open import Cat.Prelude

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

PushoutsπŸ”—

A pushout Y+XZY +_X Z of f:X→Yf : X \to Y and g:X→Zg : 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
    field
      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
  field
    {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