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}
