# Pushouts in precategories

```agda
module category-theory.pushouts-in-precategories where
```

<details><summary>Imports</summary>

```agda
open import category-theory.precategories

open import foundation.action-on-identifications-functions
open import foundation.cartesian-product-types
open import foundation.contractible-types
open import foundation.dependent-pair-types
open import foundation.identity-types
open import foundation.iterated-dependent-product-types
open import foundation.propositions
open import foundation.unique-existence
open import foundation.universe-levels
```

</details>
## Idea

A pushout of two morphisms `f : hom x a` and `g : hom x b` in a category `C`
consists of:

- an object `w`
- morphisms `p₁ : hom y w` and `p₂ : hom z w` such that
- `p₁ ∘ f = p₂ ∘ g` together with the universal property that for every object
  `w'` and pair of morphisms `p₁' : hom y w'` and `p₂' : hom z w'` such that
  `p₁' ∘ f = p₂' ∘ g` there exists a unique morphism `h : hom w w'` such that
- `h ∘ p₁ = p₁'`
- `h ∘ p₂ = p₂'`.

We say that `C` has all pushouts if there is a choice of a pushout for each
object `x` and pair of morphisms from `x` in `C`.

## Definition

```agda
module _
  {l1 l2 : Level} (C : Precategory l1 l2)
  where

  is-pushout-Precategory :
    (x y z : obj-Precategory C) →
    (f : hom-Precategory C x y) →
    (g : hom-Precategory C x z) →
    (w : obj-Precategory C) →
    (p₁ : hom-Precategory C y w) →
    (p₂ : hom-Precategory C z w) →
    comp-hom-Precategory C p₁ f ＝ comp-hom-Precategory C p₂ g →
    UU (l1 ⊔ l2)
  is-pushout-Precategory x y z f g w p₁ p₂ _ =
    (w' : obj-Precategory C) →
    (p₁' : hom-Precategory C y w') →
    (p₂' : hom-Precategory C z w') →
    comp-hom-Precategory C p₁' f ＝ comp-hom-Precategory C p₂' g →
    ∃!
      ( hom-Precategory C w w')
      ( λ h →
        ( comp-hom-Precategory C h p₁ ＝ p₁') ×
        ( comp-hom-Precategory C h p₂ ＝ p₂'))

  pushout-Precategory :
    (x y z : obj-Precategory C) →
    hom-Precategory C x y →
    hom-Precategory C x z →
    UU (l1 ⊔ l2)
  pushout-Precategory x y z f g =
    Σ (obj-Precategory C) λ w →
    Σ (hom-Precategory C y w) λ p₁ →
    Σ (hom-Precategory C z w) λ p₂ →
    Σ (comp-hom-Precategory C p₁ f ＝ comp-hom-Precategory C p₂ g) λ α →
      is-pushout-Precategory x y z f g w p₁ p₂ α

  has-all-pushout-Precategory : UU (l1 ⊔ l2)
  has-all-pushout-Precategory =
    (x y z : obj-Precategory C) →
    (f : hom-Precategory C x y) →
    (g : hom-Precategory C x z) →
    pushout-Precategory x y z f g


{-

module _
  {l1 l2 : Level} (C : Precategory l1 l2)
  (t : has-all-pullback-Precategory C)
  (x y z : obj-Precategory C)
  (f : hom-Precategory C y x)
  (g : hom-Precategory C z x)
  where

  object-pullback-Precategory : obj-Precategory C
  object-pullback-Precategory = pr1 (t x y z f g)

  pr1-pullback-Precategory :
    hom-Precategory C object-pullback-Precategory y
  pr1-pullback-Precategory = pr1 (pr2 (t x y z f g))

  pr2-pullback-Precategory :
    hom-Precategory C object-pullback-Precategory z
  pr2-pullback-Precategory = pr1 (pr2 (pr2 (t x y z f g)))

  pullback-square-Precategory-comm :
    comp-hom-Precategory C f pr1-pullback-Precategory ＝
    comp-hom-Precategory C g pr2-pullback-Precategory
  pullback-square-Precategory-comm = pr1 (pr2 (pr2 (pr2 (t x y z f g))))

  module _
    (w' : obj-Precategory C)
    (p₁' : hom-Precategory C w' y)
    (p₂' : hom-Precategory C w' z)
    (α : comp-hom-Precategory C f p₁' ＝ comp-hom-Precategory C g p₂')
    where

    morphism-into-pullback-Precategory :
      hom-Precategory C w' object-pullback-Precategory
    morphism-into-pullback-Precategory =
      pr1 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α))

    morphism-into-pullback-comm-pr1 :
      comp-hom-Precategory C
        pr1-pullback-Precategory
        morphism-into-pullback-Precategory ＝
      p₁'
    morphism-into-pullback-comm-pr1 =
      pr1 (pr2 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α)))

    morphism-into-pullback-comm-pr2 :
      comp-hom-Precategory C
        pr2-pullback-Precategory
        morphism-into-pullback-Precategory ＝
      p₂'
    morphism-into-pullback-comm-pr2 =
      pr2 (pr2 (pr1 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α)))

    is-unique-morphism-into-pullback-Precategory :
      (h' : hom-Precategory C w' object-pullback-Precategory) →
      comp-hom-Precategory C pr1-pullback-Precategory h' ＝ p₁' →
      comp-hom-Precategory C pr2-pullback-Precategory h' ＝ p₂' →
      morphism-into-pullback-Precategory ＝ h'
    is-unique-morphism-into-pullback-Precategory h' α₁ α₂ =
      ap
        ( pr1)
        ( pr2 (pr2 (pr2 (pr2 (pr2 (t x y z f g)))) w' p₁' p₂' α) (h' , α₁ , α₂))

module _
  {l1 l2 : Level} (C : Precategory l1 l2)
  (x y z : obj-Precategory C)
  (f : hom-Precategory C y x)
  (g : hom-Precategory C z x)
  (w : obj-Precategory C)
  (p₁ : hom-Precategory C w y)
  (p₂ : hom-Precategory C w z)
  (α : comp-hom-Precategory C f p₁ ＝ comp-hom-Precategory C g p₂)
  where

  is-prop-is-pullback-Precategory :
    is-prop (is-pullback-Precategory C x y z f g w p₁ p₂ α)
  is-prop-is-pullback-Precategory =
    is-prop-iterated-Π 3
      ( λ w' p₁' p₂' → is-prop-function-type is-property-is-contr)

  is-pullback-prop-Precategory : Prop (l1 ⊔ l2)
  pr1 is-pullback-prop-Precategory =
    is-pullback-Precategory C x y z f g w p₁ p₂ α
  pr2 is-pullback-prop-Precategory =
    is-prop-is-pullback-Precategory
-}
```