Pushouts of pointed types

Content created by Egbert Rijke, Fredrik Bakke and maybemabeline.

Created on 2023-05-03.
Last modified on 2024-03-13.

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)

Recent changes