open import Cat.Diagram.Limit.Equaliser open import Cat.Diagram.Limit.Pullback open import Cat.Instances.Shape.Cospan open import Cat.Diagram.Limit.Product open import Cat.Diagram.Limit.Base 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.Thin open import Data.Bool import Cat.Reasoning as Cat module Cat.Diagram.Limit.Finite where

# Finitely Complete Categories🔗

A category is said to be **finitely complete** if it admits limits for every diagram with a finite shape. While this condition might sound very strong, and thus that it would be hard to come by, it turns out 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\ot\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 : ∀ A B → Product C A B equalisers : ∀ {A B} (f g : Hom A B) → Equaliser C f g pullbacks : ∀ {A B X} (f : Hom A X) (g : Hom B X) → Pullback C f g 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 Cart = Cartesian C products open Cart using (_⊗_) public open Finitely-complete

## 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 \xto{f} Z \xot{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 .limiting {p₁' = p₁'} {p₂' = p₂'} p = eq.limiting {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₁∘limiting = pullr eq.universal ∙ pr.π₁∘factor pb .p₂∘limiting = pullr eq.universal ∙ pr.π₂∘factor pb .unique p q = eq.unique (sym (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.limiting {p₁' = p1'} {p₂' = p2'} (is-contr→is-prop (term _) _ _) prod .is-product.π₁∘factor = Pb.p₁∘limiting prod .is-product.π₂∘factor = Pb.p₂∘limiting 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:

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 \id{equ} = \langle \id{id}, \id{id} \rangle$ (since the square above is a pullback).

But both projections out of $\langle \id{id}, \id{id} \rangle$ are equal, so we can apply commutativity of the square above *again* to conclude that $f \circ \id{equ} = g \circ \id{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 \id{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 $\id{equ} : \id{eq}(f,g) \to A$ in our pullback diagram is indeed the equaliser of $f$ and $g$.

eq .has-is-eq .limiting {e′ = e′} p = Pb.limiting (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 .universal = Pb.p₂∘limiting eq .has-is-eq .unique {F} {e′ = e′} {lim' = lim'} e′=p₂∘l = Pb.unique path (sym e′=p₂∘l) where path : Pb.p₁ ∘ lim' ≡ f ∘ e′ path = Pb.p₁ ∘ lim' ≡⟨ insertl Bb.π₁∘factor ⟩≡ Bb.π₁ ∘ ⟨id,id⟩ ∘ Pb.p₁ ∘ lim' ≡⟨ ap (Bb.π₁ ∘_) (extendl Pb.square) ⟩≡ Bb.π₁ ∘ ⟨f,g⟩ ∘ Pb.p₂ ∘ lim' ≡⟨ ap (Bb.π₁ ∘_) (ap (⟨f,g⟩ ∘_) (sym e′=p₂∘l)) ⟩≡ 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

## Thinly🔗

Assuming that $\ca{C}$ is a thin category, it suffices to give constructions of products (i.e. meets) and a terminal object (i.e. a top element). In this sense, finitely complete thin categories correspond to bounded meet semilattices.

with-top-and-meets : is-thin C → Terminal C → (∀ A B → Product C A B) → Finitely-complete with-top-and-meets thin top meets = fc where open Pullback module Thin = is-thin thin fc : Finitely-complete fc .terminal = top fc .products = meets

For equalisers, note that since any pair of parallel arrows $f, g : A \to B$ was assumed to be equal (since the category is thin), we can take the domain of the equaliser to be $A$ and the equalising arrow to be $\id{id}$.

fc .equalisers {A} {B} f g = equalise where open Equaliser open is-equaliser equalise : Equaliser C _ _ equalise .apex = A equalise .equ = id equalise .has-is-eq .equal = Thin.Hom-is-prop _ _ _ _ equalise .has-is-eq .limiting {e′ = e′} p = e′ equalise .has-is-eq .universal = idl _ equalise .has-is-eq .unique p = Thin.Hom-is-prop _ _ _ _

For pullbacks, we note that since the maps into the object $C$ are trivial, they do not factor into the definition. The square automatically commutes independently of them, because, again, the category is thin. Therefore, we can simply take $(A \times_C B) = (A \times B)$ as the definition of pullback.

fc .pullbacks {A} {B} f g = pb where open Pullback open is-pullback module P = Product (meets A B) pb : Pullback C _ _ pb .apex = P.apex pb .p₁ = P.π₁ pb .p₂ = P.π₂ pb .has-is-pb .square = Thin.Hom-is-prop _ _ _ _ pb .has-is-pb .limiting {p₁' = p₁′} {p₂' = p₂′} p = P.⟨ p₁′ , p₂′ ⟩P. pb .has-is-pb .p₁∘limiting = P.π₁∘factor pb .has-is-pb .p₂∘limiting = P.π₂∘factor pb .has-is-pb .unique _ _ = Thin.Hom-is-prop _ _ _ _

# 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.

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 $\ca{C}$ has a terminal object, then a lex functor $F : \ca{C} \to \ca{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))