module Prelude.Equality  where

-- Lemmas about equality that are hard to find in the standard library


open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality


≡-pair : ∀ {a b} → {A : Set a}{B : A -> Set b} ->
         {x x' : A}{y : B x}{y' : B x'} ->
         (p : x ≡ x') -> (subst B p y ≡ y') -> (x , y) ≡ (x' , y')
≡-pair refl refl = refl

≡-pair-sym : ∀ {a b} → {A : Set a}{B : A -> Set b} ->
         {x x' : A}{y : B x}{y' : B x'} ->
         (p : x ≡ x') -> (y ≡ subst B (sym p) y') -> (x , y) ≡ (x' , y')
≡-pair-sym refl refl = refl


≡-pair-× : ∀ {a b} → {A : Set a}{B : Set b} ->
         {x x' : A}{y y' : B}
         (p : x ≡ x') -> (y ≡ y') -> (x , y) ≡ (x' , y')
≡-pair-× refl refl = refl


≡-fst : ∀ {a b} → {A : Set a}{B : A -> Set b} ->
         {x x' : A}{y : B x}{y' : B x'} ->
         (x , y) ≡ (x' , y') -> x ≡ x'
≡-fst refl = refl

≡-snd : ∀ {a b} → {A : Set a}{B : A -> Set b} ->
         {x x' : A}{y : B x}{y' : B x'} ->
         (p : (x , y) ≡ (x' , y')) -> subst B (≡-fst p) y ≡ y'
≡-snd refl = refl

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

subst-cong-lemma : ∀ {a b c} → {A : Set a}{B : Set b}(P : B -> Set c) ->
                   (f : A -> B) -> {x y : A} -> (q : x ≡ y) ->
                   (a  : P (f x)) ->
                   subst P (cong f q) a ≡ subst (P ∘ f)  q a
subst-cong-lemma P f refl a = refl                   

proj₁-subst-lemma : ∀ {b c} → {B : Set b}(P Q : B -> Set c) ->
                   {x y : B} -> (q : x ≡ y) -> (a : P x × Q x) ->
                   proj₁ (subst (λ z → P z × Q z) q a) ≡ subst P q (proj₁ a)
proj₁-subst-lemma P Q refl a = refl

proj₂-subst-lemma : ∀ {b c} → {B : Set b}(P Q : B -> Set c) ->
                   {x y : B} -> (q : x ≡ y) -> (a : P x × Q x) ->
                   proj₂ (subst (λ z → P z × Q z) q a) ≡ subst Q q (proj₂ a)
proj₂-subst-lemma P Q refl a = refl