Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Codiagonal is fiberwise suspension #892

Merged
Changes from 19 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
77 changes: 77 additions & 0 deletions src/synthetic-homotopy-theory/codiagonals-of-maps.lagda.md
Original file line number Diff line number Diff line change
Expand Up @@ -7,13 +7,23 @@ module synthetic-homotopy-theory.codiagonals-of-maps where
<details><summary>Imports</summary>

```agda
open import foundation.contractible-maps
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.equivalences
open import foundation.fibers-of-maps
open import foundation.function-types
open import foundation.homotopies
open import foundation.propositions
open import foundation.unit-type
open import foundation.universe-levels

open import synthetic-homotopy-theory.cocones-under-spans
open import synthetic-homotopy-theory.pushouts
open import synthetic-homotopy-theory.suspension-structures
open import synthetic-homotopy-theory.suspensions-of-types
open import synthetic-homotopy-theory.universal-property-pushouts
open import synthetic-homotopy-theory.universal-property-suspensions
```

</details>
Expand Down Expand Up @@ -69,3 +79,70 @@ module _
compute-glue-codiagonal-map =
compute-glue-cogap f f cocone-codiagonal-map
```

### Properties

The codiagonal is the fiberwise suspension (as claimed at the top).
tomdjong marked this conversation as resolved.
Show resolved Hide resolved

```agda
module _
{l1 l2 : Level} {A : UU l1} {B : UU l2} (f : A → B) (b : B)
where

universal-property-suspension-cocone-fiber :
{l : Level} →
Σ ( cocone terminal-map terminal-map (fiber (codiagonal-map f) b))
( universal-property-pushout l terminal-map terminal-map)
universal-property-suspension-cocone-fiber =
universal-property-pushout-cogap-fiber-up-to-equiv f f
( cocone-codiagonal-map f)
( b)
( fiber f b)
( unit)
( unit)
( inv-equiv
( terminal-map ,
( is-equiv-terminal-map-is-contr (is-torsorial-path' b))))
( inv-equiv
( terminal-map ,
( is-equiv-terminal-map-is-contr (is-torsorial-path' b))))
( id , is-equiv-id)
tomdjong marked this conversation as resolved.
Show resolved Hide resolved
( terminal-map)
( terminal-map)
( λ _ → eq-is-prop (is-prop-is-contr (is-torsorial-path' b)))
( λ _ → eq-is-prop (is-prop-is-contr (is-torsorial-path' b)))
tomdjong marked this conversation as resolved.
Show resolved Hide resolved

suspension-cocone-fiber :
suspension-cocone (fiber f b) (fiber (codiagonal-map f) b)
suspension-cocone-fiber =
pr1 (universal-property-suspension-cocone-fiber {lzero})

universal-property-suspension-fiber :
{l : Level} →
universal-property-pushout l
( terminal-map)
( terminal-map)
( suspension-cocone-fiber)
universal-property-suspension-fiber =
pr2 universal-property-suspension-cocone-fiber

equiv-suspension-fiber-fiber-codiagonal-map :
tomdjong marked this conversation as resolved.
Show resolved Hide resolved
suspension (fiber f b) ≃ fiber (codiagonal-map f) b
pr1 equiv-suspension-fiber-fiber-codiagonal-map =
cogap terminal-map terminal-map suspension-cocone-fiber
pr2 equiv-suspension-fiber-fiber-codiagonal-map =
is-equiv-up-pushout-up-pushout
( terminal-map)
( terminal-map)
( cocone-pushout terminal-map terminal-map)
( suspension-cocone-fiber)
( cogap terminal-map terminal-map (suspension-cocone-fiber))
( htpy-cocone-map-universal-property-pushout
( terminal-map)
( terminal-map)
( cocone-pushout terminal-map terminal-map)
( up-pushout terminal-map terminal-map)
( suspension-cocone-fiber))
( up-pushout terminal-map terminal-map)
( universal-property-suspension-fiber)
tomdjong marked this conversation as resolved.
Show resolved Hide resolved
```