open import Cat.Diagram.Pullback.Properties
open import Cat.Instances.Shape.Parallel
open import Cat.Diagram.Limit.Equaliser
open import Cat.Diagram.Limit.Pullback
open import Cat.Diagram.Limit.Terminal
open import Cat.Diagram.Product.Finite
open import Cat.Instances.Shape.Cospan
open import Cat.Diagram.Limit.Product
open import Cat.Diagram.Limit.Base
open import Cat.Diagram.Limit.Cone
open import Cat.Instances.Discrete
open import Cat.Diagram.Equaliser
open import Cat.Diagram.Pullback
open import Cat.Diagram.Terminal
open import Cat.Diagram.Product
open import Cat.Instances.Lift
open import Cat.Prelude
open import Cat.Finite

open import Data.Fin.Finite
open import Data.Bool

import Cat.Reasoning as Cat

open is-finite-precategory

module Cat.Diagram.Limit.Finite where

module _ {ℓ ℓ'} (C : Precategory ℓ ℓ') where
open Cat C


# Finitely Complete Categories🔗

A category is said to be finitely complete if it admits limits for every diagram with a finite shape.

  is-finitely-complete : Typeω
is-finitely-complete = ∀ {o ℓ} {D : Precategory o ℓ} → is-finite-precategory D
→ (F : Functor D C) → Limit F


Similarly to the case with arbitrary limits, we can get away with only the following common shapes of limits:

• A terminal object (limit over the empty diagram)
• Binary products (limits over diagrams of the form $\bullet\quad\bullet$, that is, two points)
• Binary equalisers (limits over diagrams of the form $\bullet\rightrightarrows\bullet$)
• Binary pullbacks (limits over diagrams of the form $\bullet\to\bullet\leftarrow\bullet$)

In reality, the list above has some redundancy. Since we can build products out of pullbacks and a terminal object, and conversely we can build pullbacks out of products and equalisers, either of the following subsets suffices:

• A terminal object, binary products, binary equalisers;
• A terminal object and binary pullbacks.

For proving that a thin category is finitely complete, given that equalisers are trivial and pullbacks coincide with products, it suffices to give a terminal object and binary products.

  record Finitely-complete : Type (ℓ ⊔ ℓ') where
field
terminal   : Terminal C
products   : has-products C
equalisers : has-equalisers C
pullbacks  : has-pullbacks C

Eq : ∀ {A B} (f g : Hom A B) → Ob
Eq f g = equalisers f g .Equaliser.apex

Pb : ∀ {A B C} (f : Hom A C) (g : Hom B C) → Ob
Pb f g = pullbacks f g .Pullback.apex

module Products = Binary-products C products
open Products using (_⊗₀_) public

open Finitely-complete


As promised, the two definitions imply each other, assuming that $\mathcal{C}$ is a univalent category (which is required to go from binary products to finite products).

  Finitely-complete→is-finitely-complete
: is-category C
→ Finitely-complete → is-finitely-complete
Finitely-complete→is-finitely-complete cat Flim finite =
limit-as-equaliser-of-product
(Cartesian→finite-products (Flim .terminal) (Flim .products) cat (finite .has-finite-Ob))
(Cartesian→finite-products (Flim .terminal) (Flim .products) cat (finite .has-finite-Mor))
(Flim .equalisers)

is-finitely-complete→Finitely-complete
: is-finitely-complete → Finitely-complete
is-finitely-complete→Finitely-complete flim = Flim where
Flim : Finitely-complete
Flim .terminal = Limit→Terminal C (flim finite-cat _)
Flim .products a b = Limit→Product C (flim Disc-finite _)
Flim .equalisers f g = Limit→Equaliser C (flim ·⇉·-finite _)
Flim .pullbacks f g = Limit→Pullback C {lzero} {lzero} (flim ·→·←·-finite _)


## With equalisers🔗

We now prove that having products and equalisers suffices to have all pullbacks; Thus a terminal object, binary products and binary equalisers suffice for finite completeness.

The main result is as follows: Let $P$ be a (the) product of $X$ and $Y$, with its projections called $p_1$ and $p_2$. Letting $X \xrightarrow{f} Z \xleftarrow{g} Y$ be a cospan, if the composites $fp_1$ and $gp_2$ have an equaliser $e : E \to P$, then the square  is a pullback. Now, that description is almost entirely abstract-nonsensical, because (for generality) we do not use any “canonical” products $X \times Y$ or equalisers $\mathrm{equ}(f,g)$. If we work slightly more concretely, then this can be read as building the pullback $X \times_Z Y$ as the largest subobject of $X \times Y$ where $f, g$ agree. In particular, the pullback we want is the object $X \times_Z Y$ in the commutative diagram below.  product-equaliser→pullback
: ∀ {E P X Y Z} {p1 : Hom P X} {p2 : Hom P Y} {f : Hom X Z}
{g : Hom Y Z} {e : Hom E P}
→ is-product C p1 p2
→ is-equaliser C (f ∘ p1) (g ∘ p2) e
→ is-pullback C (p1 ∘ e) f (p2 ∘ e) g
product-equaliser→pullback {p1 = p1} {p2} {f} {g} {e} prod eq = pb where
open is-pullback
module eq = is-equaliser eq
module pr = is-product prod

pb : is-pullback C _ _ _ _
pb .square = assoc _ _ _ ∙ eq.equal ∙ sym (assoc _ _ _)


To show that this object really is a pullback of $f$ and $g$, note that we can factor any pair of arrows $P' \to X$ and $P' \to Y$ through the Cartesian product $X \times Y$, and use the universal property of equalisers to factor that as a unique arrow $P' \to X \times_Z Y$.  pb .universal {p₁' = p₁'} {p₂' = p₂'} p =
eq.universal {e′ = pr.⟨ p₁' , p₂' ⟩pr.} (
(f ∘ p1) ∘ pr.⟨ p₁' , p₂' ⟩pr. ≡⟨ pullr pr.π₁∘factor ⟩≡
f ∘ p₁'                     ≡⟨ p ⟩≡
g ∘ p₂'                     ≡˘⟨ pullr pr.π₂∘factor ⟩≡˘
(g ∘ p2) ∘ pr.⟨ p₁' , p₂' ⟩pr. ∎
)
pb .p₁∘universal = pullr eq.factors ∙ pr.π₁∘factor
pb .p₂∘universal = pullr eq.factors ∙ pr.π₂∘factor
pb .unique p q =
eq.unique ((pr.unique _ (assoc _ _ _ ∙ p) (assoc _ _ _ ∙ q)))


Hence, assuming that a category has a terminal object, binary products and binary equalisers means it also admits pullbacks.

  with-equalisers
: Terminal C
→ (∀ A B → Product C A B)
→ (∀ {A B} (f g : Hom A B) → Equaliser C f g)
→ Finitely-complete
with-equalisers top prod equ .terminal   = top
with-equalisers top prod equ .products   = prod
with-equalisers top prod equ .equalisers = equ
with-equalisers top prod equ .pullbacks {A} {B} {X} f g =
record { has-is-pb = product-equaliser→pullback Prod.has-is-product Equ.has-is-eq }
where
module Prod = Product (prod A B)
module Equ = Equaliser (equ (f ∘ Prod.π₁) (g ∘ Prod.π₂))


## With pullbacks🔗

We’ll now prove the converse: That a terminal object and pullbacks implies having all products, and all equalisers. We’ll start with the products, since those are simpler. Observe that we can complete a product diagram (like the one on the left) to a pullback diagram (like the one on the right) by adding in the unique arrows into the terminal object $*$.

  terminal-pullback→product
: ∀ {P X Y T} {p1 : Hom P X} {p2 : Hom P Y} {f : Hom X T} {g : Hom Y T}
→ is-terminal C T → is-pullback C p1 f p2 g → is-product C p1 p2
terminal-pullback→product {p1 = p1} {p2} {f} {g} term pb = prod where    module Pb = is-pullback pb

prod : is-product C p1 p2
prod .is-product.⟨_,_⟩ p1' p2' =
Pb.universal {p₁' = p1'} {p₂' = p2'} (is-contr→is-prop (term _) _ _)
prod .is-product.π₁∘factor = Pb.p₁∘universal
prod .is-product.π₂∘factor = Pb.p₂∘universal
prod .is-product.unique other p q = Pb.unique p q

with-pullbacks
: Terminal C
→ (∀ {A B X} (f : Hom A X) (g : Hom B X) → Pullback C f g)
→ Finitely-complete
with-pullbacks top pb = fc where
module top = Terminal top
mkprod : ∀ A B → Product C A B
mkprod A B = record { has-is-product = terminal-pullback→product top.has⊤ pb′ }
where pb′ = pb (top.has⊤ A .centre) (top.has⊤ B .centre) .Pullback.has-is-pb

mkeq : ∀ {A B} (f g : Hom A B) → Equaliser C f g
mkeq {A = A} {B} f g = eq where


For equalisers, the situation is a bit more complicated. Recall that, by analogy with the case in Set, we can consider the equaliser to be the solution set of $f(x) = g(x)$, for some $f, g : A \to B$. We can consider the two sides of this equation as a single map $\langle f, g \rangle : A \to B \times B$; The equation is solved where this pairing map equals some $(x,x)$. We can thus build equalisers by pulling back along the diagonal map:  module Bb = Product (mkprod B B)
⟨id,id⟩ : Hom B Bb.apex
⟨id,id⟩ = Bb.⟨ id , id ⟩Bb.

⟨f,g⟩ : Hom A Bb.apex
⟨f,g⟩ = Bb.⟨ f , g ⟩Bb.

module Pb = Pullback (pb ⟨id,id⟩ ⟨f,g⟩)

open is-equaliser
open Equaliser


The actual equaliser map is the top, horizontal face (what the code calls Pb.p₂), so we must show that, composed with this map, $f$ and $g$ become equal. Here’s where we use the fact that pullback squares, well, commute: We know that $f$ is $\pi_1 \circ \langle f , g \rangle$, and that $\langle f , g \rangle \circ \mathrm{equ} = \langle \operatorname{id}_{}, \operatorname{id}_{} \rangle$ (since the square above is a pullback).

But both projections out of $\langle \operatorname{id}_{}, \operatorname{id}_{} \rangle$ are equal, so we can apply commutativity of the square above again to conclude that $f \circ \mathrm{equ} = g \circ \mathrm{equ}$.

      eq : Equaliser C f g
eq .apex = Pb.apex
eq .equ = Pb.p₂
eq .has-is-eq .equal =
f ∘ Pb.p₂               ≡˘⟨ pulll Bb.π₁∘factor ⟩≡˘
Bb.π₁ ∘ ⟨f,g⟩ ∘ Pb.p₂   ≡⟨ ap (Bb.π₁ ∘_) (sym Pb.square) ⟩≡
Bb.π₁ ∘ ⟨id,id⟩ ∘ Pb.p₁ ≡⟨ pulll Bb.π₁∘factor ∙ sym (pulll Bb.π₂∘factor) ⟩≡
Bb.π₂ ∘ ⟨id,id⟩ ∘ Pb.p₁ ≡⟨ ap (Bb.π₂ ∘_) Pb.square ⟩≡
Bb.π₂ ∘ ⟨f,g⟩ ∘ Pb.p₂   ≡⟨ pulll Bb.π₂∘factor ⟩≡
g ∘ Pb.p₂               ∎


We must now show that if $e'$ is another map which equalises $f$ and $g$, then it fits into a commutative diagram like the one below, so that we may conclude the dashed arrow $E' \to \mathrm{eq}(f,g)$ exists and is unique.  A bit of boring limit-chasing lets us conclude that this diagram does commute, hence the dashed arrow does exist (uniquely!), so that the top face $\mathrm{equ} : \mathrm{eq}(f,g) \to A$ in our pullback diagram is indeed the equaliser of $f$ and $g$.

      eq .has-is-eq .universal {e′ = e′} p =
Pb.universal (Bb.unique₂ refl refl (sym p1) (sym p2))
where
p1 : Bb.π₁ ∘ ⟨id,id⟩ ∘ f ∘ e′ ≡ Bb.π₁ ∘ ⟨f,g⟩ ∘ e′
p1 =
Bb.π₁ ∘ ⟨id,id⟩ ∘ f ∘ e′   ≡⟨ cancell Bb.π₁∘factor ⟩≡
f ∘ e′                     ≡˘⟨ pulll Bb.π₁∘factor ⟩≡˘
Bb.π₁ ∘ ⟨f,g⟩ ∘ e′         ∎

p2 : Bb.π₂ ∘ ⟨id,id⟩ ∘ f ∘ e′ ≡ Bb.π₂ ∘ ⟨f,g⟩ ∘ e′
p2 =
Bb.π₂ ∘ ⟨id,id⟩ ∘ f ∘ e′   ≡⟨ cancell Bb.π₂∘factor ⟩≡
f ∘ e′                     ≡⟨ p ⟩≡
g ∘ e′                     ≡˘⟨ pulll Bb.π₂∘factor ⟩≡˘
Bb.π₂ ∘ ⟨f,g⟩ ∘ e′         ∎

eq .has-is-eq .factors = Pb.p₂∘universal
eq .has-is-eq .unique {F} {e′ = e′} {other = other} p₂∘l=e′ =
Pb.unique path p₂∘l=e′
where
path : Pb.p₁ ∘ other ≡ f ∘ e′
path =
Pb.p₁ ∘ other                   ≡⟨ insertl Bb.π₁∘factor ⟩≡
Bb.π₁ ∘ ⟨id,id⟩ ∘ Pb.p₁ ∘ other ≡⟨ ap (Bb.π₁ ∘_) (extendl Pb.square) ⟩≡
Bb.π₁ ∘ ⟨f,g⟩ ∘ Pb.p₂ ∘ other   ≡⟨ ap (Bb.π₁ ∘_) (ap (⟨f,g⟩ ∘_) p₂∘l=e′) ⟩≡
Bb.π₁ ∘ ⟨f,g⟩ ∘ e′              ≡⟨ pulll Bb.π₁∘factor ⟩≡
f ∘ e′                          ∎


Putting it all together into a record we get our proof of finite completeness:

    fc : Finitely-complete
fc .terminal = top
fc .products = mkprod
fc .equalisers = mkeq
fc .pullbacks = pb

  product→terminal-pullback
: ∀ {P X Y T} {p1 : Hom P X} {p2 : Hom P Y} {f : Hom X T} {g : Hom Y T}
→ is-terminal C T → is-product C p1 p2 → is-pullback C p1 f p2 g
product→terminal-pullback t r = pb where
open is-pullback
pb : is-pullback C _ _ _ _
pb .square = is-contr→is-prop (t _) _ _
pb .universal _ = r .is-product.⟨_,_⟩ _ _
pb .p₁∘universal = r .is-product.π₁∘factor
pb .p₂∘universal = r .is-product.π₂∘factor
pb .unique p q = r .is-product.unique _ p q

is-complete→finitely
: ∀ {a b} → is-complete a b C → Finitely-complete
is-complete→finitely {a} {b} compl = with-pullbacks term′ pb
where
pb : ∀ {x y z} (f : Hom x z) (g : Hom y z) → Pullback C f g
pb f g = Limit→Pullback C (compl (cospan→cospan-diagram _ _ f g))

idx : Precategory a b
idx = Lift-cat a b (Disc ⊥ λ x → absurd x)

F : Functor idx C
F .Functor.F₀ ()
F .Functor.F₁ {()}
F .Functor.F-id {()}
F .Functor.F-∘ {()}

limF : Limit F
limF = compl F
open Terminal
open Cone-hom
open Cone

term′ : Terminal C
term′ = record { top = Limit.apex limF ; has⊤ = limiting } where
limiting : ∀ x → is-contr _
limiting x =
contr (Limit.universal limF (λ { () }) (λ { {()} })) λ h →
sym (Limit.unique limF _ _ h λ { () })


# Lex functors🔗

A functor is said to be left exact, abbreviated lex, when it preserves finite limits. These functors aren’t called “finite-limit-preserving functors” by historical accident, and for brevity. By the characterisations above, it suffices for a functor to preserve the terminal object and pullbacks.

module _ {o ℓ o′ ℓ′} {C : Precategory o ℓ} {D : Precategory o′ ℓ′} where
private module C = Cat C
private module D = Cat D

  record is-lex (F : Functor C D) : Type (o ⊔ ℓ ⊔ o′ ⊔ ℓ′) where
private module F = Functor F

field
pres-⊤ : ∀ {T} → is-terminal C T → is-terminal D (F.₀ T)
pres-pullback
: ∀ {P X Y Z} {p1 : C.Hom P X} {p2 : C.Hom P Y}
{f : C.Hom X Z} {g : C.Hom Y Z}
→ is-pullback C p1 f p2 g
→ is-pullback D (F.₁ p1) (F.₁ f) (F.₁ p2) (F.₁ g)


Since (if a terminal object exists), products $A \times B$ can be identified with pullbacks $A \times_\top B$, if $\mathcal{C}$ has a terminal object, then a lex functor $F : \mathcal{C} \to \mathcal{D}$ also preserves products.

    pres-product
: ∀ {P A B T} {p1 : C.Hom P A} {p2 : C.Hom P B}
→ is-terminal C T
→ is-product C p1 p2
→ is-product D (F.₁ p1) (F.₁ p2)
pres-product term pr = terminal-pullback→product D (pres-⊤ term)
(pres-pullback {f = term _ .centre} {g = term _ .centre}
(product→terminal-pullback C term pr))


Since $f : A \to B$ being a monomorphism is equivalent to certain squares being pullbacks, a lex functor $F : \mathcal{C} \to \mathcal{D}$ preserves monomorphisms.

    pres-monos : ∀ {A B} {f : C.Hom A B} → C.is-monic f → D.is-monic (F.₁ f)
pres-monos {f = f} mono = is-pullback→is-monic
(subst (λ x → is-pullback D x _ x _) F.F-id
(pres-pullback
(is-monic→is-pullback mono)))

module _ {o ℓ o′ ℓ′} {C : Precategory o ℓ} {D : Precategory o′ ℓ′} where
open is-lex

F∘-is-lex
: ∀ {o′′ ℓ′′} {E : Precategory o′′ ℓ′′}
{F : Functor D E} {G : Functor C D}
→ is-lex F → is-lex G → is-lex (F F∘ G)
F∘-is-lex f g .pres-⊤ = f .pres-⊤ ⊙ g .pres-⊤
F∘-is-lex f g .pres-pullback = f .pres-pullback ⊙ g .pres-pullback