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 $\ca{P}$ admits all indexed products. Then it also admits all limits, where the limit of an arbitrary $F : \ca{C} \to \ca{P}$ is taken to be the indexed product over the space of objects of $\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 $\ca{P}$ is thin, all diagrams automatically commute, and so the morphism part of the functor $F$ 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 _ _ _ _