Dependent universal property of suspensions

Content created by Egbert Rijke, Fredrik Bakke, Raymond Baker and maybemabeline.

Created on 2023-08-28.
Last modified on 2023-09-16.

module synthetic-homotopy-theory.dependent-universal-property-suspensions where
Imports 
open import foundation.action-on-identifications-dependent-functions
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.unit-type
open import foundation.universe-levels

open import synthetic-homotopy-theory.dependent-cocones-under-spans
open import synthetic-homotopy-theory.dependent-suspension-structures
open import synthetic-homotopy-theory.suspension-structures

Idea

This is the dependent analog of the universal property of suspensions.

Definition

The dependent universal property of suspensions

dependent-ev-suspension :
  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2}
  (s : suspension-structure X Y) (B : Y → UU l3) →
  ((y : Y) → B y) →
  dependent-suspension-structure B s
pr1 (dependent-ev-suspension s B f) =
  f (north-suspension-structure s)
pr1 (pr2 (dependent-ev-suspension s B f)) =
  f (south-suspension-structure s)
pr2 (pr2 (dependent-ev-suspension s B f)) =
  (apd f) ∘ (meridian-suspension-structure s)

module _
  (l : Level) {l1 l2 : Level} {X : UU l1} {Y : UU l2}
  (s : suspension-structure X Y)
  where

  dependent-universal-property-suspension : UU (l1 ⊔ l2 ⊔ lsuc l)
  dependent-universal-property-suspension =
    (B : Y → UU l) → is-equiv (dependent-ev-suspension s B)

Coherence between dependent-ev-suspension and dependent-cocone-map

module _
  {l1 l2 l3 : Level} {X : UU l1} {Y : UU l2}
  where

  triangle-dependent-ev-suspension :
    (s : suspension-structure X Y) →
    (B : Y → UU l3) →
    ( ( map-equiv
      ( equiv-dependent-suspension-structure-suspension-cocone s B)) ∘
    ( dependent-cocone-map
      ( const X unit star)
      ( const X unit star)
      ( cocone-suspension-structure X Y s)
      ( B))) ~
    ( dependent-ev-suspension s B)
  triangle-dependent-ev-suspension s B = refl-htpy

Recent changes