This file needs reorganization and clean-up.

\begin{code}

{-# OPTIONS --without-K --exact-split --safe #-}

module UF-Base where

open import SpartanMLTT

Nat : {X : 𝓀 Μ‡ } β†’ (X β†’ π“₯ Μ‡ ) β†’ (X β†’ 𝓦 Μ‡ ) β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 Μ‡
Nat A B = βˆ€ x β†’ A x β†’ B x

Nats-are-natural : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (B : X β†’ 𝓦 Μ‡ )
                   (Ο„ : Nat A B) {x y : X} (p : x ≑ y)
                 β†’ Ο„ y ∘ transport A p ≑ transport B p ∘ Ο„ x
Nats-are-natural A B Ο„ refl = refl

Nats-are-natural-∼ : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (B : X β†’ 𝓦 Μ‡ )
                     (Ο„ : Nat A B) {x y : X} (p : x ≑ y)
                   β†’ Ο„ y ∘ transport A p ∼ transport B p ∘ Ο„ x
Nats-are-natural-∼ A B Ο„ refl a = refl

NatΞ£ : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {B : X β†’ 𝓦 Μ‡ } β†’ Nat A B β†’ Ξ£ A β†’ Ξ£ B
NatΞ£ ΞΆ (x , a) = (x , ΞΆ x a)

NatΞ  : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {B : X β†’ 𝓦 Μ‡ } β†’ Nat A B β†’ Ξ  A β†’ Ξ  B
NatΞ  f g x = f x (g x) -- (S combinator from combinatory logic!)

Ξ Ξ£-distr : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {P : (x : X) β†’ A x β†’ 𝓦 Μ‡ }
         β†’ (Ξ  x κž‰ X , Ξ£ a κž‰ A x , P x a)
         β†’ Ξ£ f κž‰ Ξ  A , Ξ  x κž‰ X , P x (f x)
Ξ Ξ£-distr Ο† = (Ξ» x β†’ pr₁ (Ο† x)) , Ξ» x β†’ prβ‚‚ (Ο† x)

Ξ Ξ£-distr-back : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {P : (x : X) β†’ A x β†’ 𝓦 Μ‡ }
              β†’ (Ξ£ f κž‰ Ξ  A , Ξ  x κž‰ X , P x (f x))
              β†’ Ξ  x κž‰ X , Ξ£ a κž‰ A x , P x a
Ξ Ξ£-distr-back (f , Ο†) x = f x , Ο† x

_β‰ˆ_ : {X : 𝓀 Μ‡ } {x : X} {A : X β†’ π“₯ Μ‡ } β†’ Nat (Id x) A β†’ Nat (Id x) A β†’ 𝓀 βŠ” π“₯ Μ‡
Ξ· β‰ˆ ΞΈ = βˆ€ y β†’ Ξ· y ∼ ΞΈ y

ap-const : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (y : Y) {x x' : X} (p : x ≑ x')
         β†’ ap (Ξ» _ β†’ y) p ≑ refl
ap-const y refl = refl

transport-fiber : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
                  (x x' : X) (y : Y) (p : x ≑ x') (q : f x ≑ y)
                β†’ transport (Ξ» - β†’ f - ≑ y) p q ≑ ap f (p ⁻¹) βˆ™ q
transport-fiber f x x' y refl refl = refl

transportβ‚‚ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (A : X β†’ Y β†’ 𝓦 Μ‡ )
             {x x' : X} {y y' : Y}
             β†’ x ≑ x' β†’ y ≑ y' β†’ A x y β†’ A x' y'
transportβ‚‚ A refl refl = id

transport₃ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ } (A : X β†’ Y β†’ Z β†’ 𝓣 Μ‡ )
             {x x' : X} {y y' : Y} {z z' : Z}
           β†’ x ≑ x' β†’ y ≑ y' β†’ z ≑ z' β†’ A x y z β†’ A x' y' z'
transport₃ A refl refl refl = id

back-transportβ‚‚ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (A : X β†’ Y β†’ 𝓦 Μ‡ )
                  {x x' : X} {y y' : Y}
                β†’ x ≑ x' β†’ y ≑ y' β†’ A x' y' β†’ A x y
back-transportβ‚‚ A refl refl = id

Idtofun : {X Y : 𝓀 Μ‡ } β†’ X ≑ Y β†’ X β†’ Y
Idtofun = transport id

Idtofun-retraction : {X Y : 𝓀 Μ‡ } (p : X ≑ Y) β†’ Idtofun p ∘ Idtofun (p ⁻¹) ∼ id
Idtofun-retraction refl _ = refl

Idtofun-section : {X Y : 𝓀 Μ‡ } (p : X ≑ Y) β†’ Idtofun (p ⁻¹) ∘ Idtofun p ∼ id
Idtofun-section refl _ = refl

back-Idtofun : {X Y : 𝓀 Μ‡ } β†’ X ≑ Y β†’ Y β†’ X
back-Idtofun = back-transport id

forth-and-back-transport : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ }
                           {x y : X} (p : x ≑ y) {a : A x}
                         β†’ back-transport A p (transport A p a) ≑ a
forth-and-back-transport refl = refl

back-and-forth-transport : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ }
                           {x y : X} (p : y ≑ x) {a : A x}
                         β†’ transport A p (back-transport A p a) ≑ a
back-and-forth-transport refl = refl

back-transport-is-pre-comp : {X X' : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (p : X ≑ X') (g : X' β†’ Y)
                           β†’ back-transport (Ξ» - β†’ - β†’ Y) p g ≑ g ∘ Idtofun p
back-transport-is-pre-comp refl g = refl

transport-is-pre-comp : {X X' : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (p : X ≑ X') (g : X β†’ Y)
                      β†’ transport (Ξ» - β†’ - β†’ Y) p g ≑ g ∘ Idtofun (p ⁻¹)
transport-is-pre-comp refl g = refl

trans-sym : {X : 𝓀 Μ‡ } {x y : X} (r : x ≑ y) β†’ r ⁻¹ βˆ™ r ≑ refl
trans-sym refl = refl

trans-sym' : {X : 𝓀 Μ‡ } {x y : X} (r : x ≑ y) β†’ r βˆ™ r ⁻¹ ≑ refl
trans-sym' refl = refl

transport-Γ— : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (B : X β†’ 𝓦 Μ‡ )
              {x y : X} {c : A x Γ— B x} (p : x ≑ y)
            β†’ transport (Ξ» x β†’ A x Γ— B x) p c
            ≑ (transport A p (pr₁ c) , transport B p (prβ‚‚ c))
transport-Γ— A B refl = refl

transport-βˆ™ : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ )
                 {x y z : X} (q : x ≑ y) (p : y ≑ z) {a : A x}
               β†’ transport A  (q βˆ™ p) a ≑ transport A p (transport A q a)
transport-βˆ™ A refl refl = refl

transport-βˆ™' : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ )
                  {x y z : X} (q : x ≑ y) (p : y ≑ z)
                β†’ transport A  (q βˆ™ p) ≑ transport A p ∘ transport A q
transport-βˆ™' A refl refl = refl

transport-ap : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (A : Y β†’ 𝓦 Μ‡ )
               (f : X β†’ Y) {x x' : X} (p : x ≑ x') {a : A(f x)}
             β†’ transport (A ∘ f) p a ≑ transport A (ap f p) a
transport-ap A f refl = refl

transport-ap' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (A : Y β†’ 𝓦 Μ‡ )
                (f : X β†’ Y) {x x' : X} (p : x ≑ x')
              β†’ transport (A ∘ f) p ≑ transport A (ap f p)
transport-ap' A f refl = refl

nat-transport : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {B : X β†’ 𝓦 Μ‡ }
                (f : Nat A B) {x y : X} (p : x ≑ y) {a : A x}
              β†’ f y (transport A p a) ≑ transport B p (f x a)
nat-transport f refl = refl

transport-fam : {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ } (P : {x : X} β†’ Y x β†’ 𝓦 Μ‡ )
               (x : X) (y : Y x) β†’ P y β†’ (x' : X) (r : x ≑ x') β†’ P(transport Y r y)
transport-fam P x y p .x refl = p

transport-rel : {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ } (_β‰Ί_ : {x : X} β†’ Y x β†’ Y x β†’ 𝓦 Μ‡ )
              β†’ (a x : X) (b : Y a) (v : Y x) (p : a ≑ x)
              β†’  v β‰Ί transport Y p b
              β†’ back-transport Y p v β‰Ί b
transport-rel _β‰Ί_ a .a b v refl = id

transport-rel' : {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ } (_β‰Ί_ : {x : X} β†’ Y x β†’ Y x β†’ 𝓦 Μ‡ )
               β†’ (a x : X) (b : Y a) (v : Y x) (r : x ≑ a)
               β†’ transport Y r v β‰Ί b
               β†’ v β‰Ί back-transport Y r b
transport-rel' _β‰Ί_ a .a b v refl = id

transport-const : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {x x' : X} {y : Y} (p : x ≑ x')
                β†’ transport (Ξ» (_ : X) β†’ Y) p y ≑ y
transport-const refl = refl

apd' : {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ ) (f : (x : X) β†’ A x)
       {x y : X} (p : x ≑ y)
     β†’ transport A p (f x) ≑ f y
apd' A f refl = refl

apd : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } (f : (x : X) β†’ A x)
      {x y : X} (p : x ≑ y)
    β†’ transport A p (f x) ≑ f y
apd = apd' _

ap-id-is-id : {X : 𝓀 Μ‡ } {x y : X} (p : x ≑ y) β†’ ap id p ≑ p
ap-id-is-id refl = refl

ap-id-is-id' : {X : 𝓀 Μ‡ } {x y : X} (p : x ≑ y) β†’ p ≑ ap id p
ap-id-is-id' refl = refl

ap-βˆ™ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y) {x y z : X} (p : x ≑ y) (q : y ≑ z)
     β†’ ap f (p βˆ™ q) ≑ ap f p βˆ™ ap f q
ap-βˆ™ f refl refl = refl

ap-βˆ™' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y) {x y : X} (p : x ≑ y)
      β†’ ap f (p ⁻¹) βˆ™ ap f p ≑ refl
ap-βˆ™' f refl = refl

ap-sym : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y) {x y : X} (p : x ≑ y)
       β†’ (ap f p) ⁻¹ ≑ ap f (p ⁻¹)
ap-sym f refl = refl

ap-ap : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ } (f : X β†’ Y) (g : Y β†’ Z)
        {x x' : X} (r : x ≑ x')
      β†’ ap g (ap f r) ≑ ap (g ∘ f) r
ap-ap {𝓀} {π“₯} {𝓦} {X} {Y} {Z} f g = J A (Ξ» x β†’ refl)
 where
  A : (x x' : X) β†’ x ≑ x' β†’ 𝓦 Μ‡
  A x x' r = ap g (ap f r) ≑ ap (g ∘ f) r

apβ‚‚ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ } (f : X β†’ Y β†’ Z) {xβ‚€ x₁ : X} {yβ‚€ y₁ : Y}
    β†’ xβ‚€ ≑ x₁ β†’ yβ‚€ ≑ y₁ β†’ f xβ‚€ yβ‚€ ≑ f x₁ y₁
apβ‚‚ f refl refl = refl

refl-left-neutral : {X : 𝓀 Μ‡ } {x y : X} {p : x ≑ y} β†’ refl βˆ™ p ≑ p
refl-left-neutral {𝓀} {X} {x} {_} {refl} = refl

refl-right-neutral : {X : 𝓀 Μ‡ } {x y : X} (p : x ≑ y) β†’ p ≑ p βˆ™ refl
refl-right-neutral p = refl

βˆ™assoc : {X : 𝓀 Μ‡ } {x y z t : X} (p : x ≑ y) (q : y ≑ z) (r : z ≑ t)
       β†’ (p βˆ™ q) βˆ™ r ≑ p βˆ™ (q βˆ™ r)
βˆ™assoc refl refl refl = refl

happly' : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } (f g : Ξ  A) β†’ f ≑ g β†’ f ∼ g
happly' f g p x = ap (Ξ» - β†’ - x) p

happly : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {f g : Ξ  A} β†’ f ≑ g β†’ f ∼ g
happly = happly' _ _

sym-is-inverse : {X : 𝓀 Μ‡ } {x y : X} (p : x ≑ y)
               β†’ refl ≑ p ⁻¹ βˆ™ p
sym-is-inverse = J (Ξ» x y p β†’ refl ≑ p ⁻¹ βˆ™ p) (Ξ» x β†’ refl)

sym-is-inverse' : {X : 𝓀 Μ‡ } {x y : X} (p : x ≑ y)
                β†’ refl ≑ p βˆ™ p ⁻¹
sym-is-inverse' refl = refl

⁻¹-involutive : {X : 𝓀 Μ‡ } {x y : X} (p : x ≑ y) β†’ (p ⁻¹)⁻¹ ≑ p
⁻¹-involutive refl = refl

⁻¹-contravariant : {X : 𝓀 Μ‡ } {x y : X} (p : x ≑ y) {z : X} (q : y ≑ z)
                 β†’ q ⁻¹ βˆ™ p ⁻¹ ≑ (p βˆ™ q)⁻¹
⁻¹-contravariant refl refl = refl

left-inverse : {X : 𝓀 Μ‡ } {x y : X} (p : x ≑ y) β†’ p ⁻¹ βˆ™ p ≑ refl
left-inverse {𝓀} {X} {x} {y} refl = refl

right-inverse : {X : 𝓀 Μ‡ } {x y : X} (p : x ≑ y) β†’ refl ≑ p βˆ™ p ⁻¹
right-inverse {𝓀} {X} {x} {y} refl = refl

cancel-left : {X : 𝓀 Μ‡ } {x y z : X} {p : x ≑ y} {q r : y ≑ z}
            β†’ p βˆ™ q ≑ p βˆ™ r β†’ q ≑ r
cancel-left {𝓀} {X} {x} {y} {z} {p} {q} {r} s =
       q              β‰‘βŸ¨ refl-left-neutral ⁻¹ ⟩
       refl βˆ™ q       β‰‘βŸ¨ ap (Ξ» - β†’ - βˆ™ q) ((left-inverse p)⁻¹) ⟩
       (p ⁻¹ βˆ™ p) βˆ™ q β‰‘βŸ¨ βˆ™assoc (p ⁻¹) p q ⟩
       p ⁻¹ βˆ™ (p βˆ™ q) β‰‘βŸ¨ ap (Ξ» - β†’ p ⁻¹ βˆ™ -) s ⟩
       p ⁻¹ βˆ™ (p βˆ™ r) β‰‘βŸ¨ (βˆ™assoc (p ⁻¹) p r)⁻¹ ⟩
       (p ⁻¹ βˆ™ p) βˆ™ r β‰‘βŸ¨ ap (Ξ» - β†’ - βˆ™ r) (left-inverse p) ⟩
       refl βˆ™ r       β‰‘βŸ¨ refl-left-neutral ⟩
       r              ∎

\end{code}

It is shorter to prove the above using pattern matching on refl, of course.

\begin{code}

cancelβ‚„ : {X : 𝓀 Μ‡ } {x y z : X} (p : x ≑ y) (q : z ≑ y)
        β†’ (p βˆ™ q ⁻¹) βˆ™ (q βˆ™ p ⁻¹) ≑ refl
cancelβ‚„ refl refl = refl

\end{code}

Added 24 February 2020 by Tom de Jong.

\begin{code}

cancel-left-≑ : {X : 𝓀 Μ‡ } {x y z : X} {p : x ≑ y} {q r : y ≑ z}
              β†’ (p βˆ™ q ≑ p βˆ™ r) ≑ (q ≑ r)
cancel-left-≑ {𝓀} {X} {x} {y} {z} {refl} {q} {r} =
 apβ‚‚ (Ξ» u v β†’ u ≑ v) refl-left-neutral refl-left-neutral

\end{code}

\begin{code}

homotopies-are-natural' : {X : 𝓀 Μ‡ } {A : π“₯ Μ‡ } (f g : X β†’ A) (H : f ∼ g) {x y : X} {p : x ≑ y}
                        β†’ H x βˆ™ ap g p βˆ™ (H y)⁻¹ ≑ ap f p
homotopies-are-natural' f g H {x} {_} {refl} = trans-sym' (H x)

homotopies-are-natural'' : {X : 𝓀 Μ‡ } {A : π“₯ Μ‡ } (f g : X β†’ A) (H : f ∼ g) {x y : X} {p : x ≑ y}
                         β†’ (H x) ⁻¹ βˆ™ ap f p βˆ™ H y ≑ ap g p
homotopies-are-natural'' f g H {x} {_} {refl} = trans-sym (H x)

homotopies-are-natural : {X : 𝓀 Μ‡ } {A : π“₯ Μ‡ } (f g : X β†’ A) (H : f ∼ g) {x y : X} {p : x ≑ y}
                       β†’ H x βˆ™ ap g p ≑ ap f p βˆ™ H y
homotopies-are-natural f g H {x} {_} {refl} = refl-left-neutral ⁻¹

to-Γ—-≑ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {x x' : X} {y y' : Y}
       β†’ x ≑ x' β†’ y ≑ y' β†’ (x , y) ≑ (x' , y')
to-Γ—-≑ refl refl = refl

to-Γ—-≑' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {z z' : X Γ— Y}
        β†’ (pr₁ z ≑ pr₁ z') Γ— (prβ‚‚ z ≑ prβ‚‚ z') β†’ z ≑ z'
to-Γ—-≑' (refl , refl) = refl

from-Γ—-≑' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {z z' : X Γ— Y}
          β†’ z ≑ z'
          β†’ (pr₁ z ≑ pr₁ z') Γ— (prβ‚‚ z ≑ prβ‚‚ z' )
from-Γ—-≑' refl = (refl , refl)

tofrom-Γ—-≑ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
             {z z' : X Γ— Y} (p : z ≑ z')
           β†’ p ≑ to-Γ—-≑ (pr₁ (from-Γ—-≑' p)) (prβ‚‚ (from-Γ—-≑' p))
tofrom-Γ—-≑ refl = refl

from-Ξ£-≑' : {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ } {u v : Ξ£ Y} (r : u ≑ v)
          β†’ transport Y (ap pr₁ r) (prβ‚‚ u) ≑ (prβ‚‚ v)
from-Ξ£-≑' {𝓀} {π“₯} {X} {Y} {u} {v} = J A (Ξ» u β†’ refl) {u} {v}
 where
  A : (u v : Ξ£ Y) β†’ u ≑ v β†’ π“₯ Μ‡
  A u v r = transport Y (ap pr₁ r) (prβ‚‚ u) ≑ (prβ‚‚ v)

from-Ξ£-≑ : {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ } {Οƒ Ο„ : Ξ£ Y} (r : Οƒ ≑ Ο„)
         β†’ Ξ£ p κž‰ pr₁ Οƒ ≑ pr₁ Ο„ , transport Y p (prβ‚‚ Οƒ) ≑ (prβ‚‚ Ο„)
from-Ξ£-≑ r = (ap pr₁ r , from-Ξ£-≑' r)

to-Ξ£-≑ : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {Οƒ Ο„ : Ξ£ A}
       β†’ (Ξ£ p κž‰ pr₁ Οƒ ≑ pr₁ Ο„ , transport A p (prβ‚‚ Οƒ) ≑ prβ‚‚ Ο„)
       β†’ Οƒ ≑ Ο„
to-Ξ£-≑ (refl , refl) = refl

ap-pr₁-to-Ξ£-≑ : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {Οƒ Ο„ : Ξ£ A}
                (w : Ξ£ p κž‰ pr₁ Οƒ ≑ pr₁ Ο„ , transport A p (prβ‚‚ Οƒ) ≑ prβ‚‚ Ο„)
              β†’ ap pr₁ (to-Ξ£-≑ w) ≑ pr₁ w
ap-pr₁-to-Ξ£-≑ (refl , refl) = refl

to-Ξ£-≑' : {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡ } {x : X} {y y' : Y x}
        β†’ y ≑ y'
        β†’ (x , y) ≑[ Ξ£ Y ] (x , y')
to-Ξ£-≑' {𝓀} {π“₯} {X} {Y} {x} = ap (Ξ» - β†’ (x , -))

fromto-Ξ£-≑ : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ }
             {Οƒ Ο„ : Ξ£ A}
             (w : Ξ£ p κž‰ pr₁ Οƒ ≑ pr₁ Ο„ , transport A p (prβ‚‚ Οƒ) ≑ prβ‚‚ Ο„)
           β†’ from-Ξ£-≑ (to-Ξ£-≑ w) ≑ w
fromto-Ξ£-≑ (refl , refl) = refl

tofrom-Ξ£-≑ : {X : 𝓀 Μ‡ } {A : X β†’ π“₯ Μ‡ } {Οƒ Ο„ : Ξ£ A} (r : Οƒ ≑ Ο„)
           β†’ to-Ξ£-≑ (from-Ξ£-≑ r) ≑ r
tofrom-Ξ£-≑ refl = refl

ap-pr₁-to-Γ—-≑ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {z t : X Γ— Y}
              β†’ (p₁ : pr₁ z ≑ pr₁ t)
              β†’ (pβ‚‚ : prβ‚‚ z ≑ prβ‚‚ t)
              β†’ ap pr₁ (to-Γ—-≑ p₁ pβ‚‚) ≑ p₁
ap-pr₁-to-Γ—-≑ refl refl = refl

ap-prβ‚‚-to-Γ—-≑ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {z t : X Γ— Y}
              β†’ (p₁ : pr₁ z ≑ pr₁ t)
              β†’ (pβ‚‚ : prβ‚‚ z ≑ prβ‚‚ t)
              β†’ ap prβ‚‚ (to-Γ—-≑ p₁ pβ‚‚) ≑ pβ‚‚
ap-prβ‚‚-to-Γ—-≑ refl refl = refl

\end{code}

Added by Tom de Jong
22 March 2021:

\begin{code}

ap-pr₁-refl-lemma : {X : 𝓀 Μ‡ } (Y : X β†’ π“₯ Μ‡ )
                    {x : X} {y y' : Y x}
                    (w : (x , y) ≑[ Ξ£ Y ] (x , y'))
                  β†’ ap pr₁ w ≑ refl
                  β†’ y ≑ y'
ap-pr₁-refl-lemma Y {x} {y} {y'} w p = Ξ³ (ap pr₁ w) p βˆ™ h
 where
  Ξ³ : (r : x ≑ x) β†’ (r ≑ refl) β†’ y ≑ transport Y r y
  Ξ³ r refl = refl
  h : transport Y (ap pr₁ w) y ≑ y'
  h = from-Ξ£-≑' w

transport-along-≑ : {X : 𝓀 Μ‡ } {x y : X} (q : x ≑ y) (p : x ≑ x)
                  β†’ transport (Ξ» - β†’ - ≑ -) q p ≑ q ⁻¹ βˆ™ p βˆ™ q
transport-along-≑ refl p = (refl ⁻¹ βˆ™ (p βˆ™ refl) β‰‘βŸ¨ refl              ⟩
                            refl ⁻¹ βˆ™ p          β‰‘βŸ¨ refl-left-neutral ⟩
                            p                    ∎                     ) ⁻¹

transport-along-β†’ : {X : 𝓀 Μ‡ } (Y : X β†’ π“₯ Μ‡ ) (Z : X β†’ 𝓦 Μ‡ )
                    {x y : X}
                    (p : x ≑ y) (f : Y x β†’ Z x)
                  β†’ transport (Ξ» - β†’ (Y - β†’ Z -)) p f
                  ≑ transport Z p ∘ f ∘ transport Y (p ⁻¹)
transport-along-β†’ Y Z refl f = refl

\end{code}