-- {-# 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)


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

{----- Lemmas about subst ------------------------------------}

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

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