module foundations.homotopies-are-natural-isomorphisms where
open import foundations.universe open import foundations.identity-type open import foundations.groupoid-laws open import foundations.identity-type-reasoning open import foundations.functions-are-functors open import foundations.homotopy open import foundations.dependent-map open import foundations.transport open import foundations.function
fからgへのホモトピーは関手間の自然同型と見なせる。
private variable
ℓ : Level
A B : Type ℓ
f g : A → B
naturalityHtpy : ∀ (H : f ~ g)
→ ∀ {x y : A} (p : x ＝ y)
→ H x ∙ ap g p ＝ ap f p ∙ H y
naturalityHtpy H refl = runitId (H _) ∙ sym (lunitId (H _))
その特殊な場合：
htpyToId : ∀ (H : f ~ idFunction A)
→ ∀ (x : A)
→ H (f x) ＝ ap f (H x)
htpyToId {f = f} H x = rcancelId (H (f x)) (ap f (H x)) (H x) b
where
a : H (f x) ∙ ap (idFunction _) (H x) ＝ ap f (H x) ∙ H x
a = naturalityHtpy H (H x)
b : H (f x) ∙ H x ＝ ap f (H x) ∙ H x
b = ap (H (f x) ∙_) (sym (apId (H x))) ∙ a
依存積バージョン：
private variable
P : A → Type ℓ
f′ g′ : (a : A) → P a
naturalityHtpyD : ∀ (H : f′ ~ g′)
→ ∀ {x y : A} (p : x ＝ y)
→ ap (subst P p) (H x) ∙ apd g′ p ＝ apd f′ p ∙ H y
naturalityHtpyD {P = P} H {x = x} refl =
(runitId _ ∙ apId (H x)) ∙ sym (lunitId (H _))