```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

```