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 .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 _ _ _ _