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 oo-sets is (ΞΉ,ΞΊ)(\iota,\kappa)-complete for any universe levels ι≀o\iota \le o and κ≀o\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 oo is also acceptable. So, suppose we have an indexing category D\ca{D} and a diagram F:Dβ†’SetsF : \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 FF β€” which we will write lim⁑F\lim F β€” by first taking the product ∏j:DF(j)\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)∘f(x)=f(y)F(g) \circ f(x) = f(y), i.e., those which are cones over FF.

  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:Dx : \ca{D}, and an inhabitant (f,p)(f,p) of the type underlying f-apex, we must cough up (for ψ) an object of F(x)F(x); But this is exactly what f(x)f(x) gives us. Similarly, since pp 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 KK, to build a cone homomorphism Kβ†’lim⁑FK \to \lim F, recall that KK comes equipped with its own function ψ:∏x:DKβ†’F(x)\psi : \prod_{x : \ca{D}} K \to F(x), which we can simply flip around to get a function Kβ†’βˆx:DF(x)K \to \prod_{x : \ca{D}} F(x); This function is in the subset carved out by lim⁑F\lim F since KK is a cone, hence F(f)∘ψ(x)=ψ(y)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 AA where ff and gg 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Γ—BA \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