Martin Escardo 2011.

\begin{code}

{-# OPTIONS --without-K #-}

module Equality where

open import SetsAndFunctions
open import CurryHoward

\end{code}

Definition (Intensional equality).

\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}

Induction on ≡:

\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} refl = f x

\end{code}

We will often use pattern matching rather than J, but we'll make sure
we don't use the K rule (UIP) inadvertently. But not in the following
definition:

\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 y = y

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

≢-sym : {X : Set} → {x y : X} → x ≢ y → y ≢ x
≢-sym f r = f(sym r)

trans-sym : {X : Set} {x y : X} (r : x ≡ y) → trans (sym r) r ≡ refl
trans-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

sym-is-inverse : {X : Set} {x y : X} (p : x ≡ y) → refl ≡ trans (sym p) p
sym-is-inverse {X} = J {X} (λ x y p → refl ≡ trans (sym p) p) (λ x → refl)

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}

For the moment I put this in this module:

\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')

Σ-≡-lemma : {X : Set} → {Y : X → Set} →
∀(u v : Σ {X} Y) → ∀(r : u ≡ v) → subst {X} {Y} (cong π₀ r) (π₁ u) ≡ (π₁ v)
Σ-≡-lemma {X} {Y} u v = J A (λ u → refl) {u} {v}
where
A : ∀(u v : Σ {X} Y) → u ≡ v → Prp
A u v r = subst {X} {Y} (cong π₀ r) (π₁ u) ≡ (π₁ v)

Σ-≡-lemma' : {X : Set} → {Y : X → Set} →
∀(x : X) → (y y' : Y x) → ∀(r : (x , y) ≡ (x , y')) → subst {X} {Y} (cong π₀ r) y ≡ y'
Σ-≡-lemma' {X} {Y} x y y' = Σ-≡-lemma {X} {Y} (x , y) (x , y')

Σ-≡ : {X : Set} {Y : X → Set} (x x' : X) (y : Y x) (y' : Y x')
→ (p : x ≡ x') → subst {X} {Y} p y ≡ y' → _≡_ {Σ Y} (x , y) (x' , y')
Σ-≡ .x' x' .y y refl refl = refl

Σ-≡' : {X : Set} {Y : X → Set} (x : X) (y y' : Y x)
→ y ≡ y' → _≡_ {Σ Y} (x , y) (x , y')
Σ-≡' x y y' r = cong (λ y → (x , y)) r

\end{code}

Standard syntax for equality chain reasoning:

\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

𝟙-all-* : ∀(x : 𝟙) → x ≡ *
𝟙-all-* * = refl

\end{code}