Homotopies
Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides, Vojtěch Štěpančík and maybemabeline.
Created on 2022-02-04.
Last modified on 2024-04-17.
module foundation-core.homotopies where
Imports
open import foundation.action-on-identifications-dependent-functions open import foundation.action-on-identifications-functions open import foundation.universe-levels open import foundation-core.dependent-identifications open import foundation-core.function-types open import foundation-core.identity-types open import foundation-core.transport-along-identifications
Idea
A homotopy between dependent functions f
and g
is a pointwise equality
between them.
Definitions
The type family of identifications between values of two dependent functions
module _ {l1 l2 : Level} {X : UU l1} {P : X → UU l2} (f g : (x : X) → P x) where eq-value : X → UU l2 eq-value x = (f x = g x) {-# INLINE eq-value #-} map-compute-dependent-identification-eq-value : {x y : X} (p : x = y) (q : eq-value x) (r : eq-value y) → apd f p ∙ r = ap (tr P p) q ∙ apd g p → dependent-identification eq-value p q r map-compute-dependent-identification-eq-value refl q r = inv ∘ (concat' r (right-unit ∙ ap-id q))
The type family of identifications between values of two ordinary functions
module _ {l1 l2 : Level} {X : UU l1} {Y : UU l2} (f g : X → Y) where eq-value-function : X → UU l2 eq-value-function = eq-value f g {-# INLINE eq-value-function #-} map-compute-dependent-identification-eq-value-function : {x y : X} (p : x = y) (q : eq-value f g x) (r : eq-value f g y) → ap f p ∙ r = q ∙ ap g p → dependent-identification eq-value-function p q r map-compute-dependent-identification-eq-value-function refl q r = inv ∘ concat' r right-unit map-compute-dependent-identification-eq-value-id-id : {l1 : Level} {A : UU l1} {a b : A} (p : a = b) (q : a = a) (r : b = b) → p ∙ r = q ∙ p → dependent-identification (eq-value id id) p q r map-compute-dependent-identification-eq-value-id-id refl q r s = inv (s ∙ right-unit) map-compute-dependent-identification-eq-value-comp-id : {l1 l2 : Level} {A : UU l1} {B : UU l2} (g : B → A) (f : A → B) {a b : A} (p : a = b) (q : eq-value (g ∘ f) id a) (r : eq-value (g ∘ f) id b) → ap g (ap f p) ∙ r = q ∙ p → dependent-identification (eq-value (g ∘ f) id) p q r map-compute-dependent-identification-eq-value-comp-id g f refl q r s = inv (s ∙ right-unit)
Homotopies
module _ {l1 l2 : Level} {A : UU l1} {B : A → UU l2} where infix 6 _~_ _~_ : (f g : (x : A) → B x) → UU (l1 ⊔ l2) f ~ g = (x : A) → eq-value f g x
Properties
Reflexivity
module _ {l1 l2 : Level} {A : UU l1} {B : A → UU l2} where refl-htpy : {f : (x : A) → B x} → f ~ f refl-htpy x = refl refl-htpy' : (f : (x : A) → B x) → f ~ f refl-htpy' f = refl-htpy
Inverting homotopies
inv-htpy : {f g : (x : A) → B x} → f ~ g → g ~ f inv-htpy H x = inv (H x)
Concatenating homotopies
module _ {l1 l2 : Level} {A : UU l1} {B : A → UU l2} where infixl 15 _∙h_ _∙h_ : {f g h : (x : A) → B x} → f ~ g → g ~ h → f ~ h (H ∙h K) x = (H x) ∙ (K x) concat-htpy : {f g : (x : A) → B x} → f ~ g → (h : (x : A) → B x) → g ~ h → f ~ h concat-htpy H h K x = concat (H x) (h x) (K x) concat-htpy' : (f : (x : A) → B x) {g h : (x : A) → B x} → g ~ h → f ~ g → f ~ h concat-htpy' f K H = H ∙h K concat-inv-htpy : {f g : (x : A) → B x} → f ~ g → (h : (x : A) → B x) → f ~ h → g ~ h concat-inv-htpy = concat-htpy ∘ inv-htpy concat-inv-htpy' : (f : (x : A) → B x) {g h : (x : A) → B x} → g ~ h → f ~ h → f ~ g concat-inv-htpy' f K = concat-htpy' f (inv-htpy K)
Transposition of homotopies
module _ {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h : (x : A) → B x} (H : f ~ g) (K : g ~ h) (L : f ~ h) (M : H ∙h K ~ L) where left-transpose-htpy-concat : K ~ inv-htpy H ∙h L left-transpose-htpy-concat x = left-transpose-eq-concat (H x) (K x) (L x) (M x) inv-htpy-left-transpose-htpy-concat : inv-htpy H ∙h L ~ K inv-htpy-left-transpose-htpy-concat = inv-htpy left-transpose-htpy-concat right-transpose-htpy-concat : H ~ L ∙h inv-htpy K right-transpose-htpy-concat x = right-transpose-eq-concat (H x) (K x) (L x) (M x) inv-htpy-right-transpose-htpy-concat : L ∙h inv-htpy K ~ H inv-htpy-right-transpose-htpy-concat = inv-htpy right-transpose-htpy-concat
Associativity of concatenation of homotopies
module _ {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h k : (x : A) → B x} (H : f ~ g) (K : g ~ h) (L : h ~ k) where assoc-htpy : (H ∙h K) ∙h L ~ H ∙h (K ∙h L) assoc-htpy x = assoc (H x) (K x) (L x) inv-htpy-assoc-htpy : H ∙h (K ∙h L) ~ (H ∙h K) ∙h L inv-htpy-assoc-htpy = inv-htpy assoc-htpy
Unit laws for homotopies
module _ {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g : (x : A) → B x} {H : f ~ g} where left-unit-htpy : refl-htpy ∙h H ~ H left-unit-htpy x = left-unit inv-htpy-left-unit-htpy : H ~ refl-htpy ∙h H inv-htpy-left-unit-htpy = inv-htpy left-unit-htpy right-unit-htpy : H ∙h refl-htpy ~ H right-unit-htpy x = right-unit inv-htpy-right-unit-htpy : H ~ H ∙h refl-htpy inv-htpy-right-unit-htpy = inv-htpy right-unit-htpy
Inverse laws for homotopies
module _ {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g : (x : A) → B x} (H : f ~ g) where left-inv-htpy : inv-htpy H ∙h H ~ refl-htpy left-inv-htpy = left-inv ∘ H inv-htpy-left-inv-htpy : refl-htpy ~ inv-htpy H ∙h H inv-htpy-left-inv-htpy = inv-htpy left-inv-htpy right-inv-htpy : H ∙h inv-htpy H ~ refl-htpy right-inv-htpy = right-inv ∘ H inv-htpy-right-inv-htpy : refl-htpy ~ H ∙h inv-htpy H inv-htpy-right-inv-htpy = inv-htpy right-inv-htpy
Inverting homotopies is an involution
module _ {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g : (x : A) → B x} (H : f ~ g) where inv-inv-htpy : inv-htpy (inv-htpy H) ~ H inv-inv-htpy = inv-inv ∘ H
Distributivity of inv
over concat
for homotopies
module _ {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h : (x : A) → B x} (H : f ~ g) (K : g ~ h) where distributive-inv-concat-htpy : inv-htpy (H ∙h K) ~ inv-htpy K ∙h inv-htpy H distributive-inv-concat-htpy x = distributive-inv-concat (H x) (K x) inv-htpy-distributive-inv-concat-htpy : inv-htpy K ∙h inv-htpy H ~ inv-htpy (H ∙h K) inv-htpy-distributive-inv-concat-htpy = inv-htpy distributive-inv-concat-htpy
Naturality of homotopies with respect to identifications
Given two maps f g : A → B
and a homotopy H : f ~ g
, then for every
identification p : x = y
in A
, we have a
commuting square of identifications
ap f p
f x -------> f y
| |
H x | | H y
∨ ∨
g x -------> g y.
ap g p
nat-htpy : {l1 l2 : Level} {A : UU l1} {B : UU l2} {f g : A → B} (H : f ~ g) {x y : A} (p : x = y) → H x ∙ ap g p = ap f p ∙ H y nat-htpy H refl = right-unit inv-nat-htpy : {l1 l2 : Level} {A : UU l1} {B : UU l2} {f g : A → B} (H : f ~ g) {x y : A} (p : x = y) → ap f p ∙ H y = H x ∙ ap g p inv-nat-htpy H p = inv (nat-htpy H p) nat-refl-htpy : {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) {x y : A} (p : x = y) → nat-htpy (refl-htpy' f) p = inv right-unit nat-refl-htpy f refl = refl inv-nat-refl-htpy : {l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) {x y : A} (p : x = y) → inv-nat-htpy (refl-htpy' f) p = right-unit inv-nat-refl-htpy f refl = refl nat-htpy-id : {l : Level} {A : UU l} {f : A → A} (H : f ~ id) {x y : A} (p : x = y) → H x ∙ p = ap f p ∙ H y nat-htpy-id H refl = right-unit inv-nat-htpy-id : {l : Level} {A : UU l} {f : A → A} (H : f ~ id) {x y : A} (p : x = y) → ap f p ∙ H y = H x ∙ p inv-nat-htpy-id H p = inv (nat-htpy-id H p)
Homotopies preserve the laws of the action on identity types
module _ {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h : (x : A) → B x} where ap-concat-htpy : (H : f ~ g) {K K' : g ~ h} → K ~ K' → H ∙h K ~ H ∙h K' ap-concat-htpy H L x = ap (concat (H x) (h x)) (L x) ap-concat-htpy' : {H H' : f ~ g} (K : g ~ h) → H ~ H' → H ∙h K ~ H' ∙h K ap-concat-htpy' K L x = ap (concat' (f x) (K x)) (L x) ap-binary-concat-htpy : {H H' : f ~ g} {K K' : g ~ h} → H ~ H' → K ~ K' → H ∙h K ~ H' ∙h K' ap-binary-concat-htpy {H} {H'} {K} {K'} HH KK = ap-concat-htpy H KK ∙h ap-concat-htpy' K' HH module _ {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g : (x : A) → B x} {H H' : f ~ g} where ap-inv-htpy : H ~ H' → inv-htpy H ~ inv-htpy H' ap-inv-htpy K x = ap inv (K x)
Concatenating with an inverse homotopy is inverse to concatenating
We show that the operation K ↦ inv-htpy H ∙h K
is inverse to the operation
K ↦ H ∙h K
by constructing homotopies
inv-htpy H ∙h (H ∙h K) ~ K
H ∙h (inv H ∙h K) ~ K.
Similarly, we show that the operation H ↦ H ∙h inv-htpy K
is inverse to the
operation H ↦ H ∙h K
by constructing homotopies
(H ∙h K) ∙h inv-htpy K ~ H
(H ∙h inv-htpy K) ∙h K ~ H.
module _ {l1 l2 : Level} {A : UU l1} {B : A → UU l2} {f g h : (x : A) → B x} where is-retraction-inv-concat-htpy : (H : f ~ g) (K : g ~ h) → inv-htpy H ∙h (H ∙h K) ~ K is-retraction-inv-concat-htpy H K x = is-retraction-inv-concat (H x) (K x) is-section-inv-concat-htpy : (H : f ~ g) (L : f ~ h) → H ∙h (inv-htpy H ∙h L) ~ L is-section-inv-concat-htpy H L x = is-section-inv-concat (H x) (L x) is-retraction-inv-concat-htpy' : (K : g ~ h) (H : f ~ g) → (H ∙h K) ∙h inv-htpy K ~ H is-retraction-inv-concat-htpy' K H x = is-retraction-inv-concat' (K x) (H x) is-section-inv-concat-htpy' : (K : g ~ h) (L : f ~ h) → (L ∙h inv-htpy K) ∙h K ~ L is-section-inv-concat-htpy' K L x = is-section-inv-concat' (K x) (L x)
Reasoning with homotopies
Homotopies can be constructed by equational reasoning in the following way:
homotopy-reasoning
f ~ g by htpy-1
~ h by htpy-2
~ i by htpy-3
The homotopy obtained in this way is htpy-1 ∙h (htpy-2 ∙h htpy-3)
, i.e., it is
associated fully to the right.
infixl 1 homotopy-reasoning_ infixl 0 step-homotopy-reasoning homotopy-reasoning_ : {l1 l2 : Level} {X : UU l1} {Y : X → UU l2} (f : (x : X) → Y x) → f ~ f homotopy-reasoning f = refl-htpy step-homotopy-reasoning : {l1 l2 : Level} {X : UU l1} {Y : X → UU l2} {f g : (x : X) → Y x} → f ~ g → (h : (x : X) → Y x) → g ~ h → f ~ h step-homotopy-reasoning p h q = p ∙h q syntax step-homotopy-reasoning p h q = p ~ h by q
See also
- We postulate that homotopies characterize identifications of (dependent)
functions in the file
foundation.function-extensionality
. - Multivariable homotopies.
- The whiskering operations on homotopies.
Recent changes
- 2024-04-17. Fredrik Bakke. Splitting idempotents (#1105).
- 2024-03-13. Egbert Rijke. Refactoring pointed types (#1056).
- 2024-02-19. Fredrik Bakke. Additions for coherently invertible maps (#1024).
- 2024-02-06. Egbert Rijke and Fredrik Bakke. Refactor files about identity types and homotopies (#1014).
- 2024-01-14. Fredrik Bakke. Exponentiating retracts of maps (#989).