Martin Escardo

This file needs reorganization and clean-up.

\begin{code}

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

module UF.Base where

open import MLTT.Spartan

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⁻¹ : {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⁻¹ (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

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

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

Idtofun⁻¹ : {X Y : 𝓤 ̇ }  X  Y  Y  X
Idtofun⁻¹ = transport⁻¹ id

forth-and-back-transport : {X : 𝓤 ̇ } {A : X  𝓥 ̇ }
                           {x y : X} (p : x  y) {a : A x}
                          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 (transport⁻¹ A p a)  a
back-and-forth-transport refl = 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

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

transportd : {X : 𝓤 ̇ } (A : X  𝓥 ̇ ) (B : (x : X)  A x  𝓦 ̇ )
             {x : X}  (a : A x) {y : X} (p : x  y)
            B x a
            B y (transport A p a)
transportd A B a refl = id

transport-Σ : {X : 𝓤 ̇ } (A : X  𝓥 ̇ ) (B : (x : X)  A x  𝓦 ̇ )
              {x : X} (y : X) (p : x  y) (a : A x) {b : B x a}
             transport  -  Σ a  A - , B - a) p (a , b)
             transport A p a , transportd A B a p b
transport-Σ A B {x} x refl a = 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-left-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  transport⁻¹ Y r b
transport-left-rel _≺_ a a b v refl = id

transport-right-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
                     transport⁻¹ Y p v  b
transport-right-rel _≺_ a a b v refl = id

transport⁻¹-right-rel : {X : 𝓤 ̇ } {Y : X  𝓥 ̇ } (_≺_ : {x : X}  Y x  Y x  𝓦 ̇ )
                       (a x : X) (b : Y a) (v : Y x) (r : x  a)
                       v  transport⁻¹ Y r b
                       transport Y r v  b
transport⁻¹-right-rel _≺_ a a b v refl = id

transport⁻¹-left-rel : {X : 𝓤 ̇ } {Y : X  𝓥 ̇ } (_≺_ : {x : X}  Y x  Y x  𝓦 ̇ )
                      (a x : X) (b : Y a) (v : Y x) (p : a  x)
                      transport⁻¹ Y p v  b
                      v  transport Y p b
transport⁻¹-left-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 refl = refl

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

\end{code}

Added by Ettore Aldrovandi, Sun Sep 24 00:35:12 UTC 2023

\begin{code}

ap₂-refl-left : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ } (f : X  Y  Z) {x : X} {y₀ y₁ : Y}
                (q : y₀  y₁)
               ap₂ f refl q  ap (f x) q
ap₂-refl-left f refl = refl

ap₂-refl-right : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ } (f : X  Y  Z) {x₀ x₁ : X} {y : Y}
                (p : x₀  x₁)
               ap₂ f p refl  ap  v  f v y) p
ap₂-refl-right f refl = refl

ap₂-∙ : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ } (f : X  Y  Z) {x₀ x₁ x₂ : X} {y₀ y₁ y₂ : Y}
        (p₀ : x₀  x₁) (p₁ : x₁  x₂)
        (q₀ : y₀  y₁) (q₁ :  y₁  y₂)
       ap₂ f (p₀  p₁) (q₀  q₁)  ap₂ f p₀ q₀  ap₂ f p₁ q₁
ap₂-∙ f refl refl refl refl = refl

\end{code}


\begin{code}

ap₃ : {W : 𝓣 ̇} {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ }
      (f : W  X  Y  Z) {w₀ w₁ : W} {x₀ x₁ : X} {y₀ y₁ : Y}
     w₀  w₁  x₀  x₁  y₀  y₁  f w₀ x₀ y₀  f w₁ x₁ y₁
ap₃ f refl refl refl = refl

\end{code}

Added by Ettore Aldrovandi, Sun Sep 24 00:35:12 UTC 2023

\begin{code}

ap₃-∙ : {W : 𝓣 ̇} {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ }
        (f : W  X  Y  Z) {w₀ w₁ w₂ : W} {x₀ x₁ x₂ : X} {y₀ y₁ y₂ : Y}
        (r₀ : w₀  w₁) (r₁ : w₁  w₂)
        (p₀ : x₀  x₁) (p₁ : x₁  x₂)
        (q₀ : y₀  y₁) (q₁ :  y₁  y₂)
       ap₃ f (r₀  r₁) (p₀  p₁) (q₀  q₁)  ap₃ f r₀ p₀ q₀  ap₃ f r₁ p₁ q₁
ap₃-∙ f refl refl refl refl refl refl = refl

ap₃-refl-left : {W : 𝓣 ̇} {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ }
                (f : W  X  Y  Z) {w : W} {x₀ x₁ : X} {y₀ y₁ : Y}
                (p : x₀  x₁) (q : y₀  y₁)
               ap₃ f refl p q  ap₂ (f w) p q
ap₃-refl-left f refl refl = refl

ap₃-refl-mid : {W : 𝓣 ̇} {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ }
               (f : W  X  Y  Z) {w₀ w₁ : W} {x : X} {y₀ y₁ : Y}
               (r : w₀  w₁) (q : y₀  y₁)
               ap₃ f r refl q  ap₂  w y  f w x y) r q
ap₃-refl-mid f refl refl = refl

ap₃-refl-right : {W : 𝓣 ̇} {X : 𝓤 ̇ } {Y : 𝓥 ̇ } {Z : 𝓦 ̇ }
               (f : W  X  Y  Z) {w₀ w₁ : W} {x₀ x₁ : X} {y : Y}
               (r : w₀  w₁) (p : x₀  x₁)
               ap₃ f r p refl  ap₂  w x  f w x y) r p
ap₃-refl-right f refl refl = refl

\end{code}

\begin{code}

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 refl = 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-right
 : {X : 𝓤 ̇ } {x y z : X}
  (p : x  y) (q : x  y) (r : y  z)
  p  r  q  r
  p  q
cancel-right refl refl refl 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}

End of addition.

\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} refl = refl

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}

Added by Ettore Aldrovandi
September 19, 2022:

\begin{code}

ap-refl : {X : 𝓤 ̇ } {Y : 𝓥 ̇ } (f : X  Y) {x : X}
         ap f (𝓻𝓮𝒻𝓵 x)  𝓻𝓮𝒻𝓵 (f x)
ap-refl f = refl
\end{code}