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

open import Categories.Category

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

open import Level

open import Categories.Category.BinaryProducts C using (BinaryProducts)
open import Categories.Category.Cartesian C using (Cartesian)
open import Categories.Diagram.Equalizer C using (Equalizer)
open import Categories.Diagram.Pullback C using (Pullback; Product×Equalizer⇒Pullback)

open Category C

record FinitelyComplete : Set (levelOfTerm C) where
  field
    cartesian : Cartesian
    equalizer :  {A B} (f g : A  B)  Equalizer f g

  module equalizer {A B} (f g : A  B) = Equalizer (equalizer f g)
  open Cartesian cartesian using (products)

  pullback :  {X Y Z} (f : X  Z) (g : Y  Z)  Pullback f g
  pullback f g = Product×Equalizer⇒Pullback (BinaryProducts.product products) (equalizer _ _)

  module pullback {X Y Z} (f : X  Z) (g : Y  Z) = Pullback (pullback f g)