Universal property of suspensions
Content created by Egbert Rijke, Fredrik Bakke and Raymond Baker.
Created on 2023-08-28.
Last modified on 2023-11-09.
module synthetic-homotopy-theory.universal-property-suspensions where
Imports
open import foundation.constant-maps open import foundation.dependent-pair-types open import foundation.equivalences open import foundation.function-types open import foundation.homotopies open import foundation.identity-types open import foundation.unit-type open import foundation.universe-levels open import foundation.whiskering-homotopies open import synthetic-homotopy-theory.cocones-under-spans open import synthetic-homotopy-theory.suspension-structures open import synthetic-homotopy-theory.universal-property-pushouts
Idea
Since suspensions are just pushouts,
they retain the expected
universal property,
which states that the map cocone-map
is a equivalence. We denote this
universal property by universal-property-suspension'
. But, due to the special
nature of the span being pushed out, the suspension of a type enjoys an
equivalent universal property, here denoted by universal-property-suspension
.
This universal property states that the map ev-suspension
is an equivalence.
Definition
The universal property of the suspension as a pushout
universal-property-suspension' : (l : Level) {l1 l2 : Level} (X : UU l1) (Y : UU l2) (s : suspension-structure X Y) → UU (lsuc l ⊔ l1 ⊔ l2) universal-property-suspension' l X Y s = universal-property-pushout l ( const X unit star) ( const X unit star) ( cocone-suspension-structure X Y s) is-suspension : (l : Level) {l1 l2 : Level} (X : UU l1) (Y : UU l2) → UU (lsuc l ⊔ l1 ⊔ l2) is-suspension l X Y = Σ (suspension-structure X Y) (universal-property-suspension' l X Y)
The universal property of the suspension reforum
ev-suspension : {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} → (s : suspension-structure X Y) → (Z : UU l3) → (Y → Z) → suspension-structure X Z ev-suspension (pair N (pair S merid)) Z h = pair (h N) (pair (h S) (h ·l merid)) universal-property-suspension : (l : Level) {l1 l2 : Level} (X : UU l1) (Y : UU l2) → suspension-structure X Y → UU (lsuc l ⊔ l1 ⊔ l2) universal-property-suspension l X Y s = (Z : UU l) → is-equiv (ev-suspension s Z)
Properties
triangle-ev-suspension : {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} → (s : suspension-structure X Y) → (Z : UU l3) → ( ( map-equiv-suspension-structure-suspension-cocone X Z) ∘ ( cocone-map ( const X unit star) ( const X unit star) ( cocone-suspension-structure X Y s))) ~ ( ev-suspension s Z) triangle-ev-suspension (pair N (pair S merid)) Z h = refl is-equiv-ev-suspension : { l1 l2 l3 : Level} {X : UU l1} {Y : UU l2} → ( s : suspension-structure X Y) → ( up-Y : universal-property-suspension' l3 X Y s) → ( Z : UU l3) → is-equiv (ev-suspension s Z) is-equiv-ev-suspension {X = X} s up-Y Z = is-equiv-left-map-triangle ( ev-suspension s Z) ( map-equiv-suspension-structure-suspension-cocone X Z) ( cocone-map ( const X unit star) ( const X unit star) ( cocone-suspension-structure X _ s)) ( inv-htpy (triangle-ev-suspension s Z)) ( up-Y Z) ( is-equiv-map-equiv-suspension-structure-suspension-cocone X Z)
Recent changes
- 2023-11-09. Egbert Rijke and Fredrik Bakke. Refactoring of retractions, sections, and equivalences, and adding the 6-for-2 property of equivalences (#903).
- 2023-09-12. Egbert Rijke. Beyond foundation (#751).
- 2023-09-12. Egbert Rijke. Factoring out whiskering (#756).
- 2023-09-11. Fredrik Bakke. Transport along and action on equivalences (#706).
- 2023-09-09. Raymond Baker and Egbert Rijke. Dependent universal property of suspensions (#718).