```-- {-# OPTIONS --without-K #-}
module Prelude.Equality where

-- Functions and lemmas related to equality

open import Function
open import Data.Product

open import Relation.Binary.PropositionalEquality public hiding ([_])

{----- Postulating function extensionality -------------------}

happly : ∀ {a b} -> {A : Set a}{B : A -> Set b} ->
{f g : (x : A) -> B x} -> f ≡ g -> (x : A) -> f x ≡ g x
happly p a = cong (λ z → z a) p

postulate
ext : ∀ {a b} → Extensionality a b
ext-β : ∀ {a b} -> {A : Set a}{B : A -> Set b} ->
{f g : (x : A) -> B x} ->
(p : (x : A) -> f x ≡ g x) -> (a : A) ->
happly (ext p) a ≡ p a
ext-η : ∀ {a b} -> {A : Set a}{B : A -> Set b} ->
{f g : (x : A) -> B x} ->
(p : f ≡ g) -> ext (happly p) ≡ p

{-------------------------------------------------------------}

{---- Equality at sigma types --------------------------------}

Σ-≡ : ∀ {aa bb} -> {A : Set aa}{B : A -> Set bb} ->
{a a' : A}{b : B a}{b' : B a'} ->
(p : a ≡ a') -> subst B p b ≡ b' ->
(a , b) ≡ (a' , b')
Σ-≡ refl refl = refl

proj₁-≡ : ∀ {a b} -> {A : Set a}{B : A -> Set b} ->
{a a' : A}{b : B a}{b' : B a'} ->
(a , b) ≡ (a' , b') -> a ≡ a'
proj₁-≡ p = cong proj₁ p

proj₂-≡ : ∀ {a b} -> {A : Set a}{B : A -> Set b} ->
{a a' : A}{b : B a}{b' : B a'} ->
(p : (a , b) ≡ (a' , b')) -> subst B (proj₁-≡ p) b ≡ b'
proj₂-≡ refl = refl

{-------------------------------------------------------------}

{----- Congruence functions ----------------------------------}

-- Note: ordinary cong defined in standard library

-- Equality is a congruence for dependent functions

congd : ∀ {a b} {A : Set a} {B : A -> Set b}
(f : (x : A) -> B x) ->
∀ {x y} -> (p : x ≡ y) ->
subst B p (f x) ≡ f y
congd f refl = refl

congd-sym : ∀ {a b} {A : Set a} {B : A -> Set b}
(f : (x : A) -> B x) ->
∀ {x y} -> (p : x ≡ y) ->
f x ≡ subst B (sym p) (f y)
congd-sym f p = sym (congd f (sym p))

-- ... and for dependent two-place functions
cong₂d : ∀ {a b c} {A : Set a} {B : A -> Set b} {C : Set c}
(f : (x : A) -> B x -> C) ->
∀ {x y u v} -> (p : x ≡ y) -> subst B p u ≡ v ->
f x u ≡ f y v
cong₂d f refl refl = refl

-- ... and three-place functions; we only need it where half of the
-- latter arguments may the depend on the first
cong₃-half-d : ∀ {a b c} {A A' : Set a}{B : A -> Set b}{C : Set c}
(f : (x : A) -> A' -> B x -> C) ->
∀ {x y z w u v} -> (p : x ≡ y) -> (p' : z ≡ w) -> subst B p u ≡ v ->
f x z u ≡ f y w v
cong₃-half-d f refl refl refl = refl

-- fully dependent version of cong₂d

congd₂ : ∀ {a b c} {A : Set a} {B : A -> Set b}
{C : (x : A) -> (y : B x) -> Set c}
(f : (x : A) -> (y : B x) -> C x y) ->
∀ {x y u v} -> (p : x ≡ y) -> (q : subst B p u ≡ v) ->
subst (λ z → C (proj₁ z) (proj₂ z)) (Σ-≡ p q) (f x u) ≡ f y v
congd₂ f refl refl = refl

-- special case of congd₂

cong₂dd : ∀ {a b c} {A : Set a} {B : A -> Set b} {C : A -> Set c}
(f : (x : A) -> B x -> C x) ->
∀ {x y u v} -> (p : x ≡ y) -> (subst B p u) ≡ v ->
subst C p (f x u) ≡ f y v
cong₂dd {C = C} f refl refl = refl

{-------------------------------------------------------------}

{---- Substitution functions ---------------------------------}

subst₂d : ∀ {a b c}{A : Set a} {A' : A -> Set b}
(B : (x : A) -> A' x -> Set c) ->
{x y : A}{u : A' x}{v : A' y} ->
(p : x ≡ y) -> subst A' p u ≡ v ->
B x u -> B y v
subst₂d B {x = x} refl q = subst (B x) q

congSubst : ∀ {a b}{A : Set a} -> {B : A -> Set b} ->
{x y : A} {p q : x ≡ y}
(r : p ≡ q) ->
{u : B x} ->
subst B p u ≡ subst B q u
congSubst {B = B} r {u} = cong (λ z → subst B z u) r

{-------------------------------------------------------------}

{----- Lemmas about the groupoid structure of ≡ --------------}

sym-sym : ∀ {a}{A : Set a}{x y : A} -> (p : y ≡ x) -> sym (sym p) ≡ p
sym-sym refl = refl

cong-id : ∀ {a}{A : Set a} -> {x y : A} -> (p : x ≡ y) -> cong id p ≡ p
cong-id refl = refl

trans-cancel : ∀ {a }{A : Set a}{x y : A} ->
(p : x ≡ y) ->
trans (sym p) p ≡ refl
trans-cancel refl = refl

trans-refl : ∀ {a }{A : Set a}{x y : A} ->
(p : x ≡ y) ->
p ≡ trans p refl
trans-refl refl = refl

trans-sym : ∀ {a }{A : Set a}{x y : A} ->
{x y z : A} (p : x ≡ y)(q : y ≡ z) ->
sym (trans p q) ≡ trans (sym q) (sym p)
trans-sym refl refl = refl

trans-assoc : ∀ {a }{A : Set a}{x y z w : A} ->
(p : x ≡ y)(q : y ≡ z)(r : z ≡ w) ->
trans p (trans q r) ≡ trans (trans p q) r
trans-assoc refl q r = refl

trans-cancel-adhoc : ∀ {a }{A : Set a}{x y z w : A} ->
(p : x ≡ y)(q : y ≡ z)(r : z ≡ w) ->
trans (sym p) (trans (trans p q) r) ≡ trans q r
trans-cancel-adhoc refl q r = refl

cong-cong : ∀ {a b c}{A : Set a}{B : Set b}{C : Set c} ->
{f : B -> C}{g : A -> B} -> {x y : A} ->
(p : x ≡ y) ->
cong (f ∘ g) p ≡ cong f (cong g p)
cong-cong refl = refl

cong-cong-cong : ∀ {a b c d}{A : Set a}{B : Set b}{C : Set c}{D : Set d} ->
{f : C -> D}{g : B -> C}{h : A -> B} -> {x y : A} ->
(p : x ≡ y) ->
cong (f ∘ g ∘ h) p ≡ cong f (cong g (cong h p))
cong-cong-cong {f = f} {g} {h} p = trans (cong-cong {f = f ∘ g} p)
(cong-cong (cong h p))

sym-cong : ∀ {a b}{A : Set a}{B : Set b} ->
{f : A -> B} -> {x y : A} ->
(p : y ≡ x) ->
cong f (sym p) ≡ sym (cong f p)
sym-cong refl = refl

trans-cong : ∀ {a b}{A : Set a}{B : Set b} ->
{f : A -> B}{x y z : A} -> (p : x ≡ y)(q : y ≡ z) ->
trans (cong f p) (cong f q) ≡ cong f (trans p q)
trans-cong refl q = refl

cong-natural : ∀ {a b} ->
{A : Set a}{B : Set b} ->
{f g : A -> B} ->
{x y : A} ->
(H : (x : A) -> f x ≡ g x) ->
(p : x ≡ y) ->
trans (cong f p) (H y) ≡ trans (H x) (cong g p)
cong-natural {x = x} H refl = trans-refl (H x)

{-------------------------------------------------------------}

subst-cod : ∀ {a a' b}{A : Set a}{A' : Set a'}{B : A -> A' -> Set b} ->
{x y : A} -> (p : x ≡ y) -> {u : (a : A') -> B x a} ->
subst (λ a → (x : A') -> B a x) p u
≡ (λ a → subst (λ z → B z a) p (u a))
subst-cod refl = refl

subst-dom : ∀ {a b c}{A : Set a}{A' : A -> Set b}{B : Set c} ->
{x y : A} -> (p : x ≡ y) -> {u : A' x -> B} ->
subst (λ a → A' a -> B) p u
≡ (λ a → u (subst A' (sym p) a))
subst-dom refl = refl

subst-dom-sym : ∀ {a b c}{A : Set a}{A' : A -> Set b}{B : Set c} ->
{x y : A} -> (p : y ≡ x) -> {u : A' x -> B} ->
subst (λ a → A' a -> B) (sym p) u
≡ (λ a → u (subst A' p a))
subst-dom-sym refl {u} = refl

subst-path-general : ∀ {a b}{A : Set a}{B : Set b} ->
{x y : A}{b : B} ->  {t : A -> B}
(p : x ≡ y) -> {u : b ≡ t x} ->
subst (λ z → b ≡ t z) p u ≡ trans u (cong t p)
subst-path-general refl {refl} = refl

subst-path : ∀ {a}{A : Set a}
{x y a : A} -> (p : x ≡ y) -> {u : a ≡ x} ->
subst (λ z → a ≡ z) p u ≡ trans u p
subst-path p {u} = trans (subst-path-general {t = id} p)
(cong (trans u) (cong-id p))

subst-natural : ∀ {a b c}{A : Set a}
{P : A -> Set b}{Q : A -> Set c} ->
(f : {y : A} -> Q y -> P y) ->
{x y : A}{u : Q x} -> (p : x ≡ y) ->
subst P p (f u) ≡ f (subst Q p u)
subst-natural f refl = refl

subst-proj₂ : ∀ {a b c}{A : Set a}{B : A -> Set b}{C : (x : A) -> B x -> Set c} ->
{x y : A}{u : B x}{v : B y} -> (p : x ≡ y) ->
{u : Σ (B x) (C x)} ->
proj₂ (subst (λ z → Σ (B z) (C z)) p u)
≡ subst (λ z → C (proj₁ z) (proj₂ z)) (Σ-≡ p (subst-natural proj₁ p)) (proj₂ u)
subst-proj₂ refl = refl

subst-cong : ∀ {a b c}{A : Set a}{A' : Set b} -> {B : A -> Set c}
{f : A' -> A} -> {x y : A'} ->
(p : x ≡ y) ->
{u : B (f x)} ->
subst (B ∘ f) p u ≡ subst B (cong f p) u
subst-cong refl = refl

subst-cong-Σ : ∀ {a a' a'' b c}{A : Set a}{A' : Set a'}{A'' : Set a''}
{B : A' -> Set b}{C : A'' -> Set c} ->
{f : A -> A'}{g : (x : A) -> B (f x) -> A''} ->
{x y : A} ->
(p : x ≡ y) ->
{u : Σ (B (f x)) (C ∘ (g x))} ->
subst (λ z → Σ (B (f z)) (C ∘ (g z))) p u
≡ (subst B (cong f p) (proj₁ u) ,
subst C (cong₂d g p (subst-cong p)) (proj₂ u))
subst-cong-Σ refl = refl

Σ-≡-cong : ∀ {a b c}{A : Set a}{B : Set b}{C : B -> Set c} -> (f : A -> B) ->
{x y : A} -> {u : C (f x)}{v : C (f y)} ->
(p : x ≡ y) -> (q : subst C (cong f p) u ≡ v) ->
Σ-≡ (cong f p) q ≡ cong (λ x → f (proj₁ x) , proj₂ x) (Σ-≡ p (trans (subst-cong p) q))
Σ-≡-cong f refl refl = refl

Σ-≡-cong-sym : ∀ {a b c}{A : Set a}{B : Set b}{C : B -> Set c} -> (f : A -> B) ->
{x y : A} -> {u : C (f x)}{v : C (f y)} ->
(p : x ≡ y) -> (q : subst (C ∘ f) p u ≡ v) ->
cong (λ x → f (proj₁ x) , proj₂ x) (Σ-≡ p q)
≡ Σ-≡ {B = C} (cong f p) (trans (sym (subst-cong p)) q)
Σ-≡-cong-sym f refl refl = refl

subst-Σ-≡-proj₁ : ∀ {a b c}{A : Set a}{B : A -> Set b}{C : A -> Set c} ->
{x y : A}{u : B x}{v : B y} -> (p : x ≡ y)(q : subst B p u ≡ v) ->
{u : C x} ->
subst C p u ≡ subst (λ (z : Σ A B) -> C (proj₁ z)) (Σ-≡ p q) u
subst-Σ-≡-proj₁ refl refl = refl

subst-Σ : ∀ {a b c}{A : Set a}{B : A -> Set b}{C : (x : A) -> B x -> Set c} ->
{x y : A} -> (p : x ≡ y) -> {u : Σ (B x) (C x)} ->
subst (λ z → Σ (B z) (C z)) p u ≡ (subst B p (proj₁ u) , subst (λ z → C (proj₁ z) (proj₂ z)) (Σ-≡ p refl) (proj₂ u))
subst-Σ refl = refl

subst-Σ-const-first : ∀ {a b c}{A : Set a}{B : Set b}{C : (x : A) -> B -> Set c} ->
{x y : A} -> (p : x ≡ y) -> {u : Σ B (C x)} ->
subst (λ z → Σ B (C z)) p u ≡ (proj₁ u , subst (λ z → C z (proj₁ u)) p (proj₂ u))
subst-Σ-const-first refl = refl

subst-sym-cong : ∀ {a b c}{A : Set a}{A' : Set b} -> {B : A -> Set c}
{f : A' -> A} -> {x y : A'} ->
(p : y ≡ x) ->
{u : B (f x)} ->
subst (B ∘ f) (sym p) u ≡ subst B (sym (cong f p)) u
subst-sym-cong {B = B} p {u = u}
= trans (subst-cong (sym p)) (cong (λ z → subst B z u) (sym-cong p))

subst-trans : ∀ {a b}{A : Set a} -> {B : A -> Set b} ->
{x y z : A} (p : x ≡ y)(q : y ≡ z) ->
{u : B x} ->
subst B (trans p q) u ≡ subst B q (subst B p u)
subst-trans refl q = refl

subst-sym-trans : ∀ {a b}{A : Set a} -> {B : A -> Set b} ->
{x y z : A} (p : x ≡ y)(q : y ≡ z) ->
{u : B z} ->
subst B (sym (trans p q)) u ≡ subst B (sym p) (subst B (sym q) u)
subst-sym-trans {B = B} {x} {y} {z} p q {u}
= trans (cong (λ z → subst B z u) (trans-sym {x = x} {y} p q))
(subst-trans (sym q) (sym p))

subst-sym-subst : ∀ {a b}{A : Set a} -> {B : A -> Set b} ->
{x y : A} (p : x ≡ y)
{u : B y} ->
subst B p (subst B (sym p) u) ≡ u
subst-sym-subst {B = B} p {u} = trans (sym (subst-trans (sym p) p))
(cong (λ z → subst B z u)
(trans-cancel p))

subst-sym'-subst : ∀ {a b}{A : Set a} -> {B : A -> Set b} ->
{x y : A} (p : x ≡ y)
{u : B x} ->
subst B (sym p) (subst B p u) ≡ u
subst-sym'-subst {B = B} p {u}
= trans (cong (λ z → subst B (sym p) (subst B z u)) (sym (sym-sym p)))
(subst-sym-subst (sym p))

subst-domcod : ∀ {a b c}{A : Set a}{A' : A -> Set b}{B : (x : A) -> A' x -> Set c} ->
{x y : A} -> (p : x ≡ y) -> {u : (a : A' x) -> B x a} ->
{-
subst (λ z → (a' : A' z) -> B z a') p u
≡ (λ a' → subst₂d (λ z w → B z w) p (subst-sym-subst p) (u (subst A' (sym p) a')))
-}
subst (λ z → (a' : A' z) -> B z a') p u
≡ (λ a' → subst (λ z → B (proj₁ z) (proj₂ z)) (Σ-≡ p (subst-sym-subst p)) (u (subst A' (sym p) a')))
subst-domcod refl = refl

subst-domcod-simple : ∀ {a b c}{A : Set a}{A' : A -> Set b}{B : A -> Set c} ->
{x y : A} -> (p : x ≡ y) -> {u : A' x -> B x} ->
subst (λ z → A' z -> B z) p u
≡ (λ a → subst B p (u (subst A' (sym p) a)))
subst-domcod-simple {B = B} refl = refl

subst-eventually-trans : ∀ {a b}{A : Set a} -> {B : A -> Set b} ->
{x y z : A} (p : x ≡ y){q : y ≡ z} ->
{r : x ≡ z} ->
r ≡ trans p q ->
{u : B x} ->
subst B r u ≡ subst B q (subst B p u)
subst-eventually-trans {B = B} p {q} rr {u}
= trans (congSubst rr) (subst-trans p q)

subst-eventually-trans' : ∀ {a b}{A : Set a} -> {B : A -> Set b} ->
{x y z : A} {p : x ≡ y}(q : y ≡ z) ->
{r : x ≡ z} ->
r ≡ trans p q ->
{u : B x} ->
subst B r u ≡ subst B q (subst B p u)
subst-eventually-trans' {B = B} {p = p} q rr {u}
= trans (congSubst rr) (subst-trans p q)

subst-sym-cancel : ∀ {a b}{A : Set a} -> {B : A -> Set b}
{x y : A} ->
(p : y ≡ x) ->
{u : B x} ->
subst B p (subst B (sym p) u) ≡ u
subst-sym-cancel {B = B} p {u = u}
= trans (sym (subst-trans (sym p) p)) (congSubst (trans-cancel p))

subst-sym-cancel' : ∀ {a b}{A : Set a} -> {B : A -> Set b}
{x y : A} ->
(p : x ≡ y) ->
{u : B x} ->
subst B (sym p) (subst B p u) ≡ u
subst-sym-cancel' {B = B} p {u = u}
= trans (cong (subst B (sym p)) (congSubst (sym (sym-sym p))))
(subst-sym-cancel (sym p))

subst-inverse : ∀ {a b}{A : Set a} -> {B : A -> Set b}
{x y : A} ->
(p : x ≡ y) ->
{u : B x}{v : B y} ->
subst B p u ≡ v ->
u ≡ subst B (sym p) v
subst-inverse refl q = q

subst-const : ∀ {a b}{A : Set a}{B : Set b} ->
{x y : A} -> (p : x ≡ y) -> {u : B} ->
subst (λ _ → B) p u ≡ u
subst-const refl = refl

subst→≡ : ∀{a a' l}{A : Set a} →
{A' : Set a'} → (h : A → A') →
(B' : A' → Set l) →
{x y : A} → (p : x ≡ y) →
∀{z z'}(e : z ≡ z') →
(subst {A = A} (B' ∘ h) p z) ≡ (subst B' (cong h p) (z'))
subst→≡ h B' p e = trans (subst-cong p) (cong (subst B' (cong h p)) e)

{-------------------------------------------------------------}

{----- Lemmas about function extensionality ------------------}

eq-extensionality : ∀ {a b}{A : Set a}{B : A -> Set b} ->
{f g : (x : A) -> B x} ->
{p q : f ≡ g} ->
((x : A) -> happly p x ≡ happly q x) -> p ≡ q
eq-extensionality {p = p} {q} r =
begin
p
≡⟨ sym (ext-η p) ⟩
ext (happly p)
≡⟨ cong ext (ext r) ⟩
ext (happly q)
≡⟨ ext-η q ⟩
q ∎ where open ≡-Reasoning

trans-ext : ∀ {a b}{A : Set a}{B : A -> Set b} -> {f g h : (x : A) -> B x} ->
(p : (x : A) -> f x ≡ g x)(q : (x : A) -> g x ≡ h x) ->
trans (ext p) (ext q) ≡ ext (λ x → trans (p x) (q x))
trans-ext p q = eq-extensionality pp
where pp : (a : _) -> _ ≡ _
pp a = begin
happly (trans (ext p) (ext q)) a
≡⟨ sym (trans-cong {f = λ z → z a} (ext p) (ext q)) ⟩
trans (happly (ext p) a) (happly (ext q) a)
≡⟨ cong₂ (λ z w → trans z w) (ext-β p a) (ext-β q a) ⟩
trans (p a) (q a)
≡⟨  sym (ext-β (λ x → trans (p x) (q x)) a) ⟩
happly (ext (λ x → trans (p x) (q x))) a
∎ where open ≡-Reasoning

{-------------------------------------------------------------}

{----- Uniqueness of Identity Proofs (for now) ---------------}

UIP : ∀ {a} → {A : Set a}{x y : A} -> (p q : x ≡ y) -> p ≡ q
UIP refl refl = refl

{-------------------------------------------------------------}
```