{-# OPTIONS --without-K --safe #-}

open import Categories.Category

module Categories.Category.Cocomplete.Finitely {o  e} (C : Category o  e) where

open import Level

open import Categories.Category.Cocartesian C
open import Categories.Diagram.Coequalizer C
open import Categories.Diagram.Pushout C
open import Categories.Diagram.Pushout.Properties C

open Category C

record FinitelyCocomplete : Set (levelOfTerm C) where
  field
    cocartesian : Cocartesian
    coequalizer :  {A B} (f g : A  B)  Coequalizer f g

  module cocartesian = Cocartesian cocartesian
  module coequalizer {A B} (f g : A  B) = Coequalizer (coequalizer f g)
  open cocartesian public

  pushout :  {X Y Z} (f : X  Y) (g : X  Z)  Pushout f g
  pushout f g = Coproduct×Coequalizer⇒Pushout coproduct (coequalizer _ _)

  module pushout {X Y Z} (f : X  Y) (g : X  Z) = Pushout (pushout f g)