module Cat.Diagram.Pushout where


A pushout of and 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 and 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 and embed and into and the maps and determine what parts of and we ought to identify in

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

        universal : βˆ€ {Q} {i₁' : Hom Y Q} {iβ‚‚' : Hom Z Q}
                   β†’ i₁' ∘ f ≑ iβ‚‚' ∘ g β†’ Hom P Q
        iβ‚βˆ˜universal : {p : i₁' ∘ f ≑ iβ‚‚' ∘ g} β†’ universal p ∘ i₁ ≑ i₁'
        iβ‚‚βˆ˜universal : {p : i₁' ∘ f ≑ iβ‚‚' ∘ g} β†’ universal p ∘ iβ‚‚ ≑ iβ‚‚'
        unique : {p : i₁' ∘ f ≑ iβ‚‚' ∘ g} {colim' : Hom P Q}
               β†’ colim' ∘ i₁ ≑ i₁'
               β†’ colim' ∘ iβ‚‚ ≑ iβ‚‚'
               β†’ colim' ≑ universal p
        : {p : i₁' ∘ f ≑ iβ‚‚' ∘ g} {colim' colim'' : Hom P Q}
        β†’ colim' ∘ i₁ ≑ i₁' β†’ colim' ∘ iβ‚‚ ≑ iβ‚‚'
        β†’ colim'' ∘ i₁ ≑ i₁' β†’ colim'' ∘ iβ‚‚ ≑ iβ‚‚'
        β†’ colim' ≑ colim''
      uniqueβ‚‚ {p = o} p q r s = unique {p = o} p q βˆ™ sym (unique r s)

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