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)
ΠΣ-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}