Pushouts
Content created by Fredrik Bakke, Jonathan Prieto-Cubides, Egbert Rijke and Raymond Baker.
Created on 2022-07-29.
Last modified on 2023-09-10.
module synthetic-homotopy-theory.pushouts where
Imports
open import foundation.action-on-identifications-functions 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.universe-levels open import synthetic-homotopy-theory.26-descent open import synthetic-homotopy-theory.cocones-under-spans open import synthetic-homotopy-theory.dependent-universal-property-pushouts open import synthetic-homotopy-theory.universal-property-pushouts
Idea
Consider a span 𝒮
of types
f g
A <--- S ---> B.
A pushout of 𝒮
is an initial type X
equipped with a
cocone structure of 𝒮
in
X
. In other words, a pushout X
of 𝒮
comes equipped with a cocone structure
(i , j , H)
where
g
S -----> B
| |
f | H | j
V V
A -----> X,
i
such that for any type Y
, the following evaluation map is an equivalence
(X → Y) → cocone 𝒮 Y.
This condition is the
universal property of the pushout
of 𝒮
.
The idea is that the pushout of 𝒮
is the universal type that contains the
elements of the types A
and B
via the 'inclusions' i : A → X
and
j : B → X
, and furthermore an identification i a = j b
for every s : S
such that f s = a
and g s = b
.
Examples of pushouts include suspensions, spheres, joins, and the smash product.
Postulates
We will assume that for any span
f g
A <--- S ---> B,
where S : UU l1
, A : UU l2
, and B : UU l3
there is a pushout in
UU (l1 ⊔ l2 ⊔ l3)
.
postulate pushout : {l1 l2 l3 : Level} {S : UU l1} {A : UU l2} {B : UU l3} (f : S → A) (g : S → B) → UU (l1 ⊔ l2 ⊔ l3) postulate inl-pushout : {l1 l2 l3 : Level} {S : UU l1} {A : UU l2} {B : UU l3} (f : S → A) (g : S → B) → A → pushout f g postulate inr-pushout : {l1 l2 l3 : Level} {S : UU l1} {A : UU l2} {B : UU l3} (f : S → A) (g : S → B) → B → pushout f g postulate glue-pushout : {l1 l2 l3 : Level} {S : UU l1} {A : UU l2} {B : UU l3} (f : S → A) (g : S → B) → ((inl-pushout f g) ∘ f) ~ ((inr-pushout f g) ∘ g) cocone-pushout : {l1 l2 l3 : Level} {S : UU l1} {A : UU l2} {B : UU l3} (f : S → A) (g : S → B) → cocone f g (pushout f g) pr1 (cocone-pushout f g) = inl-pushout f g pr1 (pr2 (cocone-pushout f g)) = inr-pushout f g pr2 (pr2 (cocone-pushout f g)) = glue-pushout f g postulate up-pushout : {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} (f : S → A) (g : S → B) → universal-property-pushout l4 f g (cocone-pushout f g) equiv-up-pushout : {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} (f : S → A) (g : S → B) (X : UU l4) → (pushout f g → X) ≃ (cocone f g X) pr1 (equiv-up-pushout f g X) = cocone-map f g (cocone-pushout f g) pr2 (equiv-up-pushout f g X) = up-pushout f g X
Definitions
The cogap map
cogap : { l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} ( f : S → A) (g : S → B) → { X : UU l4} → cocone f g X → pushout f g → X cogap f g {X} = map-inv-equiv (equiv-up-pushout f g X)
The is-pushout
predicate
is-pushout : { l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} ( f : S → A) (g : S → B) {X : UU l4} (c : cocone f g X) → UU (l1 ⊔ l2 ⊔ l3 ⊔ l4) is-pushout f g c = is-equiv (cogap f g c)
Properties
The pushout of a span has the dependent universal property
module _ {l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} where dependent-up-pushout : (f : S → A) (g : S → B) → dependent-universal-property-pushout l4 f g (cocone-pushout f g) dependent-up-pushout f g = dependent-universal-property-universal-property-pushout ( f) ( g) ( cocone-pushout f g) ( λ l → up-pushout f g) ( l4)
Computation with the cogap map
module _ { l1 l2 l3 l4 : Level} {S : UU l1} {A : UU l2} {B : UU l3} ( f : S → A) (g : S → B) { X : UU l4} (c : cocone f g X) where private htpy-cc = htpy-cocone-map-universal-property-pushout ( f) ( g) ( cocone-pushout f g) ( up-pushout f g) ( c) compute-inl-cogap : ( a : A) → cogap f g c (inl-pushout f g a) = horizontal-map-cocone f g c a compute-inl-cogap = pr1 htpy-cc compute-inr-cogap : ( b : B) → cogap f g c (inr-pushout f g b) = vertical-map-cocone f g c b compute-inr-cogap = pr1 (pr2 htpy-cc) compute-glue-cogap : ( s : S) → ( ap (cogap f g c) (glue-pushout f g s)) = ( ( compute-inl-cogap (f s) ∙ coherence-square-cocone f g c s) ∙ ( inv (compute-inr-cogap (g s)))) compute-glue-cogap s = right-transpose-eq-concat ( ap (cogap f g c) (glue-pushout f g s)) ( compute-inr-cogap (g s)) ( compute-inl-cogap (f s) ∙ coherence-square-cocone f g c s) ( pr2 (pr2 htpy-cc) s)
Recent changes
- 2023-09-10. Fredrik Bakke. Rename
inv-con
andcon-inv
toleft/right-transpose-eq-concat
(#730). - 2023-09-09. Raymond Baker and Egbert Rijke. Dependent universal property of suspensions (#718).
- 2023-06-10. Egbert Rijke. cleaning up transport and dependent identifications files (#650).
- 2023-06-10. Egbert Rijke and Fredrik Bakke. Cleaning up synthetic homotopy theory (#649).
- 2023-06-08. Fredrik Bakke. Examples of modalities and various fixes (#639).