open import Cat.Diagram.Limit.Finite
open import Cat.Diagram.Limit.Base
open import Cat.Diagram.Equaliser
open import Cat.Diagram.Pullback
open import Cat.Diagram.Terminal
open import Cat.Diagram.Product
open import Cat.Prelude

module Cat.Instances.Sets.Complete where


# Sets is completeπ

We prove that the category of is for any universe levels and Inverting this to speak of maxima rather than ordering, to admit all we must be in at least the category of but any extra adjustment is also acceptable. So, suppose we have an indexing category and a diagram Letβs build a limit for it!

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


Since Set is closed under (arbitrary) products, we can build the limit of an arbitrary diagram β which we will write β by first taking the product (which is a set of dependent functions), then restricting ourselves to the subset of those for which i.e., those which are cones over

  apex : Set _
apex = el! $Ξ£[ f β ((j : D.Ob) β β£ F.β j β£) ] (β x y (g : D.Hom x y) β F.β g (f x) β‘ (f y))  To form a cone, given an object and an inhabitant of the type underlying f-apex, we must cough up (for Ο) an object of But this is exactly what gives us. Similarly, since witnesses that commutes, we can project it directly. Given some other cone to build a cone homomorphism recall that comes equipped with its own function which we can simply flip around to get a function This function is in the subset carved out by since is a cone, hence as required.  -- open Terminal lim : make-is-limit F apex lim .Ο x (f , p) = f x lim .commutes f = funext Ξ» where (_ , p) β p _ _ f lim .universal eta p x = (Ξ» j β eta j x) , Ξ» x y f β p f$β _
lim .factors _ _ = refl
lim .unique eta p other q = funext Ξ» x β
Ξ£-prop-path! (funext Ξ» j β q j $β x)  module _ {β} where open Precategory (Sets β) private variable A B : Set β f g : β A β β β B β open Terminal open is-product open Product open is-pullback open Pullback open is-equaliser open Equaliser  ## 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 admits them.  Sets-terminal : Terminal (Sets β) Sets-terminal .top = el! (Lift _ β€) Sets-terminal .hasβ€ _ = hlevel 0  Products are given by product sets:  Sets-products : (A B : Set β) β Product (Sets β) A B Sets-products A B .apex = el! (β£ A β£ Γ β£ B β£) 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 .Οβββ¨β© = refl Sets-products A B .has-is-product .Οβββ¨β© = refl Sets-products A B .has-is-product .unique p q i x = p i x , q i x  Equalisers are given by carving out the subset of where and agree using  Sets-equalisers : (f g : Hom A B) β Equaliser (Sets β) {A = A} {B = B} f g Sets-equalisers {A = A} {B = B} f g = eq where eq : Equaliser (Sets β) f g eq .apex .β£_β£ = Ξ£[ x β A ] (f x β‘ g x) eq .apex .is-tr = hlevel 2 eq .equ = fst eq .has-is-eq .equal = funext snd eq .has-is-eq .universal {e' = e'} p x = e' x , p$β x
eq .has-is-eq .factors = refl
eq .has-is-eq .unique {p = p} q =
funext Ξ» x β Ξ£-prop-path! (happly q x)


Pullbacks are the same, but carving out a subset of

  Sets-pullbacks : β {A B C} (f : Hom A C) (g : Hom B C)
β Pullback (Sets β) {X = A} {Y = B} {Z = C} f g
Sets-pullbacks {A = A} {B = B} {C = C} f g = pb where
pb : Pullback (Sets β) f g
pb .apex .β£_β£   = Ξ£[ x β A ] Ξ£[ y β B ] (f x β‘ g y)
pb .apex .is-tr = hlevel 2
pb .pβ (x , _ , _) = x
pb .pβ (_ , y , _) = y
pb .has-is-pb .square = funext (snd β snd)
pb .has-is-pb .universal {pβ' = pβ'} {pβ'} p a = pβ' a , pβ' a , happly p a
pb .has-is-pb .pββuniversal = refl
pb .has-is-pb .pββuniversal = 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