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:C→PF : \ca{C} \to \ca{P} is taken to be the indexed product over the space of objects of C\ca{C}.

  : βˆ€ {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:

  : βˆ€ {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.

  : βˆ€ {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 _ _ _ _)

  : βˆ€ {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 _ _ _ _