open import Cat.Diagram.Limit.Finite
open import Cat.Diagram.Limit.Base
open import Cat.Diagram.Terminal
open import Cat.Prelude

module Cat.Instances.Sets.Complete where


# Sets is completeπ

We prove that the category of $o$-sets is $(\iota,\kappa)$-complete for any universe levels $\iota \le o$ and $\kappa \le o$. Inverting this to speak of maxima rather than ordering, to admit all $(\iota,\kappa)$-limits, we must be in at least the category of $(\iota \sqcup \kappa)$-sets, but any extra adjustment $o$ is also acceptable. So, suppose we have an indexing category $\ca{D}$ and a diagram $F : \ca{D} \to \sets$; Letβs build a limit for it!

Sets-is-complete : β {ΞΉ ΞΊ o} β is-complete ΞΉ ΞΊ (Sets (ΞΉ β ΞΊ β o))
Sets-is-complete {D = D} F = lim where
module D = Precategory D
module F = Functor F

comm-prop : β f β is-prop (β x y (g : D.Hom x y) β F.β g (f x) β‘ (f y))
comm-prop f = Ξ -is-hlevel 1 Ξ» _ β Ξ -is-hlevel 1 Ξ» _ β Ξ -is-hlevel 1 Ξ» _ β
F.β _ .is-tr _ _


Since Set is closed under (arbitrary) products, we can build the limit of an arbitrary diagram $F$ β which we will write $\lim F$ β by first taking the product $\prod_{j : \ca{D}} F(j)$ (which is a set of dependent functions), then restricting ourselves to the subset of those for which $F(g) \circ f(x) = f(y)$, i.e., those which are cones over $F$.

  f-apex : Set _
f-apex .β£_β£   = Ξ£[ f β ((j : D.Ob) β β£ F.β j β£) ]
(β x y (g : D.Hom x y) β F.β g (f x) β‘ (f y))

f-apex .is-tr = Ξ£-is-hlevel 2 (Ξ -is-hlevel 2 (Ξ» x β F.β x .is-tr))
(Ξ» f β is-propβis-set (comm-prop f))


To form a cone, given an object $x : \ca{D}$, and an inhabitant $(f,p)$ of the type underlying f-apex, we must cough up (for Ο) an object of $F(x)$; But this is exactly what $f(x)$ gives us. Similarly, since $p$ witnesses that $\psi$ commutes, we can project it directly.

  open Cone
cone : Cone F
cone .Cone.apex    = f-apex
cone .Ο x          = Ξ» { (f , p) β f x }
cone .commutes o   = funext Ξ» { (_ , p) β p _ _ o }


Given some other cone $K$, to build a cone homomorphism $K \to \lim F$, recall that $K$ comes equipped with its own function $\psi : \prod_{x : \ca{D}} K \to F(x)$, which we can simply flip around to get a function $K \to \prod_{x : \ca{D}} F(x)$; This function is in the subset carved out by $\lim F$ since $K$ is a cone, hence $F(f) \circ \psi(x) = \psi(y)$, as required.

  open Terminal
lim : Limit F
lim .top = cone
lim .hasβ€ K = contr map map-unique where
module K = Cone K
open Cone-hom
map : Cone-hom F K cone
map .hom x = (Ξ» j β K.Ο j x) , Ξ» x y f β happly (K.commutes f) _
map .commutes _ = refl

map-unique : β m β map β‘ m
map-unique m = Cone-hom-path _ (funext Ξ» x β
Ξ£-prop-path comm-prop (funext Ξ» y i β m .commutes y (~ i) x))


## Finite set-limitsπ

For expository reasons, we present the computation of the most famous shapes of finite limit (terminal objects, products, pullbacks, and equalisers) in the category of sets. All the definitions below are redundant, since finite limits are always small, and thus the category of sets of any level $\ell$ admits them.

  Sets-terminal : Terminal (Sets β)
Sets-terminal .top = Lift _  β€ , is-propβis-set (Ξ» _ _ β refl)
Sets-terminal .hasβ€ _ = fun-is-hlevel 0 (contr (lift tt) Ξ» x i β lift tt)


Products are given by product sets:

  Sets-products : (A B : Set β) β Product A B
Sets-products A B .apex = (β£ A β£ Γ β£ B β£) , Γ-is-hlevel 2 (A .is-tr) (B .is-tr)
Sets-products A B .Οβ = fst
Sets-products A B .Οβ = snd
Sets-products A B .has-is-product .β¨_,_β© f g x = f x , g x
Sets-products A B .has-is-product .Οββfactor = refl
Sets-products A B .has-is-product .Οββfactor = refl
Sets-products A B .has-is-product .unique o p q i x = p i x , q i x


Equalisers are given by carving out the subset of $A$ where $f$ and $g$ agree using $\Sigma$:

  Sets-equalisers : (f g : Hom A B) β Equaliser {A = A} {B = B} f g
Sets-equalisers {A = A} {B = B} f g = eq where
eq : Equaliser f g
eq .apex = Ξ£[ x β β£ A β£ ] (f x β‘ g x)
, Ξ£-is-hlevel 2 (A .is-tr) Ξ» _ β is-propβis-set (B .is-tr _ _)
eq .equ = fst
eq .has-is-eq .equal = funext snd
eq .has-is-eq .limiting {eβ² = eβ²} p x = eβ² x , happly p x
eq .has-is-eq .universal = refl
eq .has-is-eq .unique {p = p} q =
funext Ξ» x β Ξ£-prop-path (Ξ» _ β B .is-tr _ _) (happly (sym q) x)


Pullbacks are the same, but carving out a subset of $A \times B$.

  Sets-pullbacks : β {A B C} (f : Hom A C) (g : Hom B C)
β Pullback {X = A} {Y = B} {Z = C} f g
Sets-pullbacks {A = A} {B = B} {C = C} f g = pb where
pb : Pullback f g
pb .apex .β£_β£ = Ξ£[ x β β£ A β£ ] Ξ£[ y β β£ B β£ ] (f x β‘ g y)
pb .apex .is-tr =
Ξ£-is-hlevel 2 (A .is-tr) Ξ» _ β
Ξ£-is-hlevel 2 (B .is-tr) Ξ» _ β
is-propβis-set (C .is-tr _ _)
pb .pβ (x , _ , _) = x
pb .pβ (_ , y , _) = y
pb .has-is-pb .square = funext (snd β snd)
pb .has-is-pb .limiting {pβ' = pβ'} {pβ'} p a = pβ' a , pβ' a , happly p a
pb .has-is-pb .pββlimiting = refl
pb .has-is-pb .pββlimiting = refl
pb .has-is-pb .unique {p = p} {lim' = lim'} q r i x =
q i x , r i x ,
Ξ» j β is-setβsquarep (Ξ» i j β C .is-tr)
(Ξ» j β f (q j x)) (Ξ» j β lim' x .snd .snd j) (happly p x) (Ξ» j β g (r j x)) i j


Hence, Sets is finitely complete:

  open Finitely-complete

Sets-finitely-complete : Finitely-complete (Sets β)
Sets-finitely-complete .terminal = Sets-terminal
Sets-finitely-complete .products = Sets-products
Sets-finitely-complete .equalisers = Sets-equalisers
Sets-finitely-complete .pullbacks = Sets-pullbacks