Pushouts of pointed types

Content created by Egbert Rijke, Fredrik Bakke and maybemabeline.

Created on 2023-05-03.

module synthetic-homotopy-theory.pushouts-of-pointed-types where

Imports
open import foundation.action-on-identifications-functions
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.universe-levels

open import structured-types.pointed-maps
open import structured-types.pointed-types

open import synthetic-homotopy-theory.cocones-under-pointed-span-diagrams
open import synthetic-homotopy-theory.pushouts


Idea

Given a span of pointed maps, then the pushout is in fact a pushout diagram in the (wild) category of pointed types.

Definition

module _
{l1 l2 l3 : Level}
{S : Pointed-Type l1} {A : Pointed-Type l2} {B : Pointed-Type l3}
where

pushout-Pointed-Type :
(f : S →∗ A) (g : S →∗ B) → Pointed-Type (l1 ⊔ l2 ⊔ l3)
pr1 (pushout-Pointed-Type f g) =
pushout (map-pointed-map f) (map-pointed-map g)
pr2 (pushout-Pointed-Type f g) =
inl-pushout
( map-pointed-map f)
( map-pointed-map g)
( point-Pointed-Type A)


Properties

The pushout of a pointed map along a pointed map is pointed

module _
{l1 l2 l3 : Level}
{S : Pointed-Type l1} {A : Pointed-Type l2} {B : Pointed-Type l3}
where

inl-pushout-Pointed-Type :
(f : S →∗ A) (g : S →∗ B) → A →∗ pushout-Pointed-Type f g
pr1 (inl-pushout-Pointed-Type f g) =
inl-pushout (map-pointed-map f) (map-pointed-map g)
pr2 (inl-pushout-Pointed-Type f g) = refl

inr-pushout-Pointed-Type :
(f : S →∗ A) (g : S →∗ B) → B →∗ pushout-Pointed-Type f g
pr1 (inr-pushout-Pointed-Type f g) =
inr-pushout (map-pointed-map f) (map-pointed-map g)
pr2 (inr-pushout-Pointed-Type f g) =
( ( ap
( inr-pushout (map-pointed-map f) (map-pointed-map g))
( inv (preserves-point-pointed-map g))) ∙
( inv
( glue-pushout
( map-pointed-map f)
( map-pointed-map g)
( point-Pointed-Type S)))) ∙
( ap
( inl-pushout (map-pointed-map f) (map-pointed-map g))
( preserves-point-pointed-map f))


The cogap map for pushouts of pointed types

module _
{l1 l2 l3 : Level}
{S : Pointed-Type l1} {A : Pointed-Type l2} {B : Pointed-Type l3}
where

map-cogap-Pointed-Type :
{l4 : Level}
(f : S →∗ A) (g : S →∗ B) →
{X : Pointed-Type l4} →
cocone-Pointed-Type f g X →
type-Pointed-Type (pushout-Pointed-Type f g) → type-Pointed-Type X
map-cogap-Pointed-Type f g c =
cogap
( map-pointed-map f)
( map-pointed-map g)
( cocone-cocone-Pointed-Type f g c)

cogap-Pointed-Type :
{l4 : Level}
(f : S →∗ A) (g : S →∗ B) →
{X : Pointed-Type l4} →
cocone-Pointed-Type f g X → pushout-Pointed-Type f g →∗ X
pr1 (cogap-Pointed-Type f g c) = map-cogap-Pointed-Type f g c
pr2 (cogap-Pointed-Type f g {X} c) =
( compute-inl-cogap
( map-pointed-map f)
( map-pointed-map g)
( cocone-cocone-Pointed-Type f g c)
( point-Pointed-Type A)) ∙
( preserves-point-pointed-map
( horizontal-pointed-map-cocone-Pointed-Type f g c))


Computation with the cogap map for pointed types

module _
{ l1 l2 l3 l4 : Level}
{S : Pointed-Type l1} {A : Pointed-Type l2} {B : Pointed-Type l3}
( f : S →∗ A) (g : S →∗ B)
{ X : Pointed-Type l4} (c : cocone-Pointed-Type f g X)
where

compute-inl-cogap-Pointed-Type :
( x : type-Pointed-Type A) →
( map-cogap-Pointed-Type
( f)
( g)
( c)
( map-pointed-map (inl-pushout-Pointed-Type f g) x)) ＝
( horizontal-map-cocone-Pointed-Type f g c x)
compute-inl-cogap-Pointed-Type =
compute-inl-cogap
( map-pointed-map f)
( map-pointed-map g)
( cocone-cocone-Pointed-Type f g c)

compute-inr-cogap-Pointed-Type :
( y : type-Pointed-Type B) →
( map-cogap-Pointed-Type
( f)
( g)
( c)
( map-pointed-map (inr-pushout-Pointed-Type f g) y)) ＝
( vertical-map-cocone-Pointed-Type f g c y)
compute-inr-cogap-Pointed-Type =
compute-inr-cogap
( map-pointed-map f)
( map-pointed-map g)
( cocone-cocone-Pointed-Type f g c)