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

\end{code}

We will use pattern matching rather than J, but we'll make sure we
don't use the K rule (UIP) inadvertently.

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

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)

\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

\end{code}