Commuting triangles of maps
Content created by Fredrik Bakke, Jonathan Prieto-Cubides and Egbert Rijke.
Created on 2023-02-18.
Last modified on 2023-09-12.
module foundation.commuting-triangles-of-maps where open import foundation-core.commuting-triangles-of-maps public
Imports
open import foundation.action-on-identifications-functions open import foundation.functoriality-dependent-function-types open import foundation.homotopies open import foundation.identity-types open import foundation.universe-levels open import foundation-core.equivalences open import foundation-core.function-types
Idea
A triangle of maps
A ----> B
\ /
\ /
V V
X
is said to commute if there is a homotopy between the map on the left and the composite map.
Properties
Top map is an equivalence
If the top map is an equivalence, then there is an equivalence between the coherence triangle with the map of the equivalence as with the inverse map of the equivalence.
module _ {l1 l2 l3 : Level} {X : UU l1} {A : UU l2} {B : UU l3} (left : A → X) (right : B → X) (e : A ≃ B) where equiv-coherence-triangle-maps-inv-top : coherence-triangle-maps left right (map-equiv e) ≃ coherence-triangle-maps right left (map-inv-equiv e) equiv-coherence-triangle-maps-inv-top = ( equiv-inv-htpy ( left ∘ (map-inv-equiv e)) ( right)) ∘e ( equiv-Π ( λ b → left (map-inv-equiv e b) = right b) ( e) ( λ a → equiv-concat ( ap left (is-retraction-map-inv-equiv e a)) ( right (map-equiv e a)))) coherence-triangle-maps-inv-top : coherence-triangle-maps left right (map-equiv e) → coherence-triangle-maps right left (map-inv-equiv e) coherence-triangle-maps-inv-top = map-equiv equiv-coherence-triangle-maps-inv-top
Recent changes
- 2023-09-12. Egbert Rijke. Beyond foundation (#751).
- 2023-06-15. Egbert Rijke. Replace
isretr
withis-retraction
andissec
withis-section
(#659). - 2023-06-10. Egbert Rijke and Fredrik Bakke. Cleaning up synthetic homotopy theory (#649).
- 2023-06-08. Fredrik Bakke. Remove empty
foundation
modules and replace them by their core counterparts (#644). - 2023-06-07. Fredrik Bakke. Move public imports before "Imports" block (#642).