open import Cat.Diagram.Coproduct.Indexed
open import Cat.Diagram.Product.Indexed
open import Cat.Diagram.Colimit.Base
open import Cat.Diagram.Limit.Base
open import Cat.Diagram.Terminal
open import Cat.Diagram.Initial
open import Cat.Prelude
open import Cat.Thin

module Cat.Thin.Limits {o } {P : Proset o } where

Limits in prosets🔗

Suppose a proset P\ca{P} admits all indexed products. Then it also admits all limits, where the limit of an arbitrary F:CPF : \ca{C} \to \ca{P} is taken to be the indexed product over the space of objects of C\ca{C}.

has-indexed-products→proset-is-complete
  :  {o' ℓ'}  has-indexed-products P.underlying o'
   is-complete o' ℓ' P.underlying
has-indexed-products→proset-is-complete has-ips {D} F = lim where
  module F = Functor F

  ip : Indexed-product P.underlying F.₀
  ip = has-ips _

  module Π = Indexed-product ip

Since the category P\ca{P} is thin, all diagrams automatically commute, and so the morphism part of the functor FF does not contribute to the limit at all:

  lim : Limit F
  lim .top .apex = Π.ΠF
  lim .top .ψ = Π.π
  lim .top .commutes _ = P.Hom-is-prop _ _ _ _
  lim .has⊤ x .centre .hom = Π.⟨ x .ψ Π.
  lim .has⊤ x .centre .commutes o = P.Hom-is-prop _ _ _ _
  lim .has⊤ x .paths _ = Cone-hom-path _ (P.Hom-is-prop _ _ _ _)

Limits for less🔗

The data of an indexed product can be made a lot less verbose when dealing with a thin category, since the commutativity data is free:

indexed-meet→indexed-product
  :  {o′} {I : Type o′} {F : I  P.Ob} {P : P.Ob}
   (π :  i  P P.≤ F i)                 -- P is ≤ than all the F_is
   (∀ {B}  (∀ i  B P.≤ F i)  B P.≤ P) -- and P is largest among those..
   is-indexed-product P.underlying F π
indexed-meet→indexed-product π is-meet = is-ip where
  open is-indexed-product

  is-ip : is-indexed-product _ _ _
   is-ip          = is-meet
  is-ip .commute    = P.Hom-is-prop _ _ _ _
  is-ip .unique f x = P.Hom-is-prop _ _ _ _

Colimits in prosets🔗

Dualising the discussion above, colimits in prosets correspond to indexed coproducts. I won’t comment on this part of the code since it is entirely given by flipping arrows around and fixing names of record fields.

has-indexed-coproducts→proset-is-cocomplete
  :  {o' ℓ'}  has-indexed-coproducts P.underlying o'
   is-cocomplete o' ℓ' P.underlying
has-indexed-coproducts→proset-is-cocomplete has-ips {D} F = colim where
  module F = Functor F

  ic : Indexed-coproduct P.underlying F.₀
  ic = has-ips _

  open Indexed-coproduct ic

  colim : Colimit F
  colim .bot .coapex = ΣF
  colim .bot .ψ = ι
  colim .bot .commutes _ = P.Hom-is-prop _ _ _ _
  colim .has⊥ x .centre .hom = match (x .ψ)
  colim .has⊥ x .centre .commutes o = P.Hom-is-prop _ _ _ _
  colim .has⊥ x .paths _ = Cocone-hom-path _ (P.Hom-is-prop _ _ _ _)

indexed-join→indexed-coproduct
  :  {o′} {I : Type o′} {F : I  P.Ob} {J : P.Ob}
   (ι :  i  F i P.≤ J)                 -- All the F_is are ≤ than J
   (∀ {B}  (∀ i  F i P.≤ B)  J P.≤ B) -- and J is smallest among those
   is-indexed-coproduct P.underlying F ι
indexed-join→indexed-coproduct ι is-join = is-ic where
  open is-indexed-coproduct

  is-ic : is-indexed-coproduct _ _ _
  is-ic .match      = is-join
  is-ic .commute    = P.Hom-is-prop _ _ _ _
  is-ic .unique f x = P.Hom-is-prop _ _ _ _