\begin{code}
{-# OPTIONS --without-K #-}
module Equality where
open import SetsAndFunctions
open import CurryHoward
\end{code}
\begin{code}
infix 30 _≡_
infix 30 _≠_
data _≡_ {X : Set} : X → X → Prp where
refl : {x : X} → x ≡ x
_≠_ : {X : Set} → (x y : X) → Prp
x ≠ y = x ≡ y → ⊥
\end{code}
\begin{code}
J : {X : Set} → (A : ∀(x x' : X) → x ≡ x' → Prp)
→ (∀(x : X) → A x x refl)
→ ∀{x x' : X} → ∀(r : x ≡ x') → A x x' r
J A f {x} {.x} refl = f x
\end{code}
\begin{code}
pseudo-uip : {X : Set} →
∀{x x' : X} → ∀(r : x ≡ x') → (x , refl) ≡ (x' , r)
pseudo-uip {X} = J {X} A (λ x → refl)
where A : ∀(x x' : X) → x ≡ x' → Prp
A x x' r = _≡_ {Σ \(x' : X) → x ≡ x'} (x , refl) (x' , r)
subst : {X : Set}{Y : X → Set}{x x' : X} → x ≡ x' → Y x → Y x'
subst refl x = x
trans : {X : Set} → {x y z : X} → x ≡ y → y ≡ z → x ≡ z
trans refl refl = refl
sym : {X : Set} → {x y : X} → x ≡ y → y ≡ x
sym refl = refl
cong : {X Y : Set} →
∀(f : X → Y) → {x₀ x₁ : X} → x₀ ≡ x₁ → f x₀ ≡ f x₁
cong f refl = refl
Lemma-cong-cong : {X Y Z : Set} →
∀(f : X → Y) → ∀(g : Y → Z) → ∀{x x' : X} → ∀(r : x ≡ x') → cong g (cong f r) ≡ cong (g ∘ f) r
Lemma-cong-cong {X} {Y} {Z} f g = J A (λ x → refl)
where
A : ∀(x x' : X) → x ≡ x' → Prp
A x x' r = cong g (cong f r) ≡ cong (g ∘ f) r
cong₂ : {X Y Z : Set} →
∀(f : X → Y → Z) → {x₀ x₁ : X} → {y₀ y₁ : Y} →
x₀ ≡ x₁ → y₀ ≡ y₁ → f x₀ y₀ ≡ f x₁ y₁
cong₂ f refl refl = refl
fun-cong : {X Y : Set} →
∀{f g : X → Y} → f ≡ g → ∀(x : X) → f x ≡ g x
fun-cong {X} {Y} {f} {g} r x = cong (λ h → h x) r
Lemma[x≡y→y≡z→y≡z] : {X : Set} → ∀{x y z : X} → x ≡ y → x ≡ z → y ≡ z
Lemma[x≡y→y≡z→y≡z] refl refl = refl
Lemma[x≡y→x≡z→z≡y] : {X : Set} → ∀{x y z : X} → x ≡ y → x ≡ z → z ≡ y
Lemma[x≡y→x≡z→z≡y] refl refl = refl
Lemma[x≡y→x≡z→y≡z] : {X : Set} → ∀{x y z : X} → x ≡ y → x ≡ z → y ≡ z
Lemma[x≡y→x≡z→y≡z] refl refl = refl
Lemma[x≡z→y≡z→x≡y] : {X : Set} → ∀{x y z : X} → x ≡ z → y ≡ z → x ≡ y
Lemma[x≡z→y≡z→x≡y] refl refl = refl
Lemma[fx≡y→x≡x'→fx'≡y] : {X Y : Set} →
(f : X → Y) → {x x' : X} → {y : Y} → f x ≡ y → x ≡ x' → f x' ≡ y
Lemma[fx≡y→x≡x'→fx'≡y] f {x} {x'} {y} r s = Lemma[x≡y→x≡z→z≡y] r (cong f s)
\end{code}
\begin{code}
equality-cases : {X₀ X₁ : Set} → {A : Set} →
∀(y : X₀ + X₁) → (∀ x₀ → y ≡ in₀ x₀ → A) → (∀ x₁ → y ≡ in₁ x₁ → A) → A
equality-cases (in₀ x₀) f₀ f₁ = f₀ x₀ refl
equality-cases (in₁ x₁) f₀ f₁ = f₁ x₁ refl
∃! : {X : Set} → (A : X → Prp) → Prp
∃! {X} A = (∃ \(x : X) → A x) ∧ (∀(x x' : X) → A x → A x' → x ≡ x')
\end{code}
\begin{code}
infix 2 _∎
infixr 2 _≡〈_〉_
_≡〈_〉_ : {X : Set} → ∀(x : X) → ∀{y z : X} → x ≡ y → y ≡ z → x ≡ z
_ ≡〈 r 〉 s = trans r s
_∎ : {X : Set} → (x : X) → x ≡ x
_∎ _ = refl
\end{code}