open import Cat.Prelude

module Cat.Diagram.Pushout {o } (C : Precategory o ) where


A pushout Y+XZY +_X Z of f:XYf : X \to Y and g:XZg : X \to Z is the dual construction to the pullback. Much like the pullback is a subobject of the product, the pushout is a quotient object of the coproduct. The maps ff and gg tell us which parts of the coproduct to identify.

record is-pushout {P} (f : Hom X Y) (i₁ : Hom Y P) (g : Hom X Z) (i₂ : Hom Z P)
  : Type (o  ) where
      square     : i₁  f  i₂  g

The most important part of the pushout is a commutative square of the following shape:

This can be thought of as providing “gluing instructions”. The injection maps i1i_1 and i2i_2 embed YY and ZZ into PP, and the maps ff and gg determine what parts of YY and ZZ we ought to identify in PP.

The universal property ensures that we only perform the minimal number of identifications required to make the aforementioned square commute.

      colimiting :  {Q} {i₁′ : Hom Y Q} {i₂′ : Hom Z Q}
                  i₁′  f  i₂′  g  Hom P Q
      i₁∘colimiting : {p : i₁′  f  i₂′  g}  colimiting p  i₁  i₁′
      i₂∘colimiting : {p : i₁′  f  i₂′  g}  colimiting p  i₂  i₂′

      unique : {p : i₁′  f  i₂′  g} {colim′ : Hom P Q}
              colim′  i₁  i₁′
              colim′  i₂  i₂′
              colim′  colimiting p

We provide a convenient packaging of the pushout and the injection maps:

record Pushout (f : Hom X Y) (g : Hom X Z) : Type (o  ) where
    {coapex} : Ob
    i₁       : Hom Y coapex
    i₂       : Hom Z coapex
    has-is-po  : is-pushout f i₁ g i₂

  open is-pushout has-is-po public