{-# OPTIONS --universe-polymorphism #-}
module Function.Equality where
open import Function as Fun using (_on_)
open import Level
import Relation.Binary as B
import Relation.Binary.Indexed as I
record Π {f₁ f₂ t₁ t₂}
(From : B.Setoid f₁ f₂)
(To : I.Setoid (B.Setoid.Carrier From) t₁ t₂) :
Set (f₁ ⊔ f₂ ⊔ t₁ ⊔ t₂) where
open I using (_=[_]⇒_)
infixl 5 _⟨$⟩_
field
_⟨$⟩_ : (x : B.Setoid.Carrier From) → I.Setoid.Carrier To x
cong : B.Setoid._≈_ From =[ _⟨$⟩_ ]⇒ I.Setoid._≈_ To
open Π public
infixr 0 _⟶_
_⟶_ : ∀ {f₁ f₂ t₁ t₂} → B.Setoid f₁ f₂ → B.Setoid t₁ t₂ → Set _
From ⟶ To = Π From (B.Setoid.indexedSetoid To)
id : ∀ {a₁ a₂} {A : B.Setoid a₁ a₂} → A ⟶ A
id = record { _⟨$⟩_ = Fun.id; cong = Fun.id }
infixr 9 _∘_
_∘_ : ∀ {a₁ a₂} {A : B.Setoid a₁ a₂}
{b₁ b₂} {B : B.Setoid b₁ b₂}
{c₁ c₂} {C : B.Setoid c₁ c₂} →
B ⟶ C → A ⟶ B → A ⟶ C
f ∘ g = record
{ _⟨$⟩_ = Fun._∘_ (_⟨$⟩_ f) (_⟨$⟩_ g)
; cong = Fun._∘_ (cong f) (cong g)
}
const : ∀ {a₁ a₂} {A : B.Setoid a₁ a₂}
{b₁ b₂} {B : B.Setoid b₁ b₂} →
B.Setoid.Carrier B → A ⟶ B
const {B = B} b = record
{ _⟨$⟩_ = Fun.const b
; cong = Fun.const (B.Setoid.refl B)
}
setoid : ∀ {f₁ f₂ t₁ t₂}
(From : B.Setoid f₁ f₂) →
I.Setoid (B.Setoid.Carrier From) t₁ t₂ →
B.Setoid _ _
setoid From To = record
{ Carrier = Π From To
; _≈_ = λ f g → ∀ {x y} → x ≈₁ y → f ⟨$⟩ x ≈₂ g ⟨$⟩ y
; isEquivalence = record
{ refl = λ {f} → cong f
; sym = λ f∼g x∼y → To.sym (f∼g (From.sym x∼y))
; trans = λ f∼g g∼h x∼y → To.trans (f∼g From.refl) (g∼h x∼y)
}
}
where
open module From = B.Setoid From using () renaming (_≈_ to _≈₁_)
open module To = I.Setoid To using () renaming (_≈_ to _≈₂_)
infixr 0 _⇨_
_⇨_ : ∀ {f₁ f₂ t₁ t₂} → B.Setoid f₁ f₂ → B.Setoid t₁ t₂ → B.Setoid _ _
From ⇨ To = setoid From (B.Setoid.indexedSetoid To)
≡-setoid : ∀ {f t₁ t₂} (From : Set f) → I.Setoid From t₁ t₂ → B.Setoid _ _
≡-setoid From To = record
{ Carrier = (x : From) → Carrier x
; _≈_ = λ f g → ∀ x → f x ≈ g x
; isEquivalence = record
{ refl = λ {f} x → refl
; sym = λ f∼g x → sym (f∼g x)
; trans = λ f∼g g∼h x → trans (f∼g x) (g∼h x)
}
} where open I.Setoid To