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   _≡_
infix   _≠_

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

\end{code}

Standard syntax for equality chain reasoning:

\begin{code}

infix   _∎
infixr  _≡〈_〉_

_≡〈_〉_ : {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}