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}