open import Cat.Prelude

open import Order.Diagram.Lub.Reasoning
open import Order.Instances.Pointwise
open import Order.Instances.Lower
open import Order.Diagram.Glb
open import Order.Diagram.Lub
open import Order.Base

import Order.Reasoning

module Order.Instances.Lower.Cocompletion where


# Lower sets as cocompletionsπ

In this module we prove the universal property of the poset of lower sets of a poset is the free cocomplete poset on meaning that every map into a cocomplete poset admits a unique cocontinuous extension

As an intermediate step, we establish the posetal analogue of the coyoneda lemma, saying that every lower set is the join of all for

module βCoyoneda {o β} (P : Poset o β) (Ls : Lower-set P) where
private
module P  = Order.Reasoning P
module Pβ = Order.Reasoning (Lower-sets P)

diagram : β«β Ls β Lower-set P
diagram (i , iβP) = β P i


This result is much easier to establish in the posetal case than it is in the case of proper categories, so we do not comment on the construction too much. The curious reader is invited to load this file in Agda and play with it themselves!

  lower-set-is-lub : is-lub (Lower-sets P) diagram Ls
lower-set-is-lub .is-lub.famβ€lub (j , jβLs) i β‘iβ€j =
Ls .pres-β€ (out! β‘iβ€j) jβLs
lower-set-is-lub .is-lub.least ub' famβ€ub' i iβLs =
famβ€ub' (i , iβLs) i (inc (P.β€-refl))


A quick note on notation: The result saying that is the lub of the down-sets of its elements is called lower-set-β«. The integral symbol is because (in the categorical case) we can think of the coyoneda lemma as saying that presheaves are computed as certain coends.

  lower-set-β« : Ls β‘ Lub.lub (Lower-sets-cocomplete P diagram)
lower-set-β« = lub-unique (lower-set-is-lub)
(Lub.has-lub \$ Lower-sets-cocomplete P diagram)

module
_ {o β β'} {A : Poset o β} {B : Poset o β'}
{β : {I : Type o} (F : I β β B β) β β B β}
(β-lubs : β {I : Type o} (F : I β β B β) β is-lub B F (β F))
(f : Monotone A B)
where
private
module A  = Poset A
module DA = Poset (Lower-sets A)
module B  = Poset B
module B-cocomplete = Lubs B β-lubs


The cocontinuous extension sends a lower set to the join (in of which is expressed familially as the composition

It is readily computed that this procedure results in a monotone map.

  Lanβ : Monotone (Lower-sets A) B
Lanβ .hom S = β {I = Ξ£[ i β A ] (i β S)} (Ξ» i β f # (i .fst))
Lanβ .pres-β€ {S} {T} SβT = B-cocomplete.β-universal _ Ξ» where
(i , iβS) β B-cocomplete.β-inj (i , SβT i iβS)


A further short computation reveals that the least upper bound of all elements under is Put like that, it seems trivial, but it says that our cocontinuous extension commutes with the βunit mapβ

  Lanβ-commutes : β x β Lanβ # (β A x) β‘ f # x
Lanβ-commutes x = B.β€-antisym
(B-cocomplete.β-universal _ (Ξ» { (i , β‘iβ€x) β f .pres-β€ (out! β‘iβ€x) }))
(B-cocomplete.β-inj (x , inc A.β€-refl))


A short argument whose essence is the commutativity of joins with joins establishes that the cocontinuous extension does live up to its name:

  Lanβ-cocontinuous
: β {I : Type o} (F : I β Lower-set A)
β Lanβ # Lub.lub (Lower-sets-cocomplete A F) β‘ β (Ξ» i β Lanβ # (F i))
Lanβ-cocontinuous F = B.β€-antisym
(B-cocomplete.β-universal _ Ξ» where
(i , iββF) β
β‘-rec! (Ξ» { (j , iβFj) β
B.β€-trans (B-cocomplete.β-inj (i , iβFj)) (B-cocomplete.β-inj j)
}) iββF)
(B-cocomplete.β-universal _ Ξ» i β
B-cocomplete.β-universal _ Ξ» where
(j , jβFi) β B-cocomplete.β-inj (j , inc (i , jβFi)))


And the coyoneda lemma comes in to show that the cocontinuous extension is unique, for if is any other cocontinuous map sending to then expressing a lower set as

reveals that must agree with

  Lanβ-unique
: (f~ : β Monotone (Lower-sets A) B β)
β ( β {I : Type o} (F : I β Lower-set A)
β f~ # Lub.lub (Lower-sets-cocomplete A F) β‘ β (Ξ» i β f~ # (F i)) )
β (β x β f~ # (β A x) β‘ f # x)
β f~ β‘ Lanβ
Lanβ-unique f~ f~-cocont f~-comm = ext Ξ» i β
f~ # i                                                           β‘β¨ ap# f~ (βCoyoneda.lower-set-β« A i) β©β‘
f~ # Lub.lub (Lower-sets-cocomplete A (βCoyoneda.diagram A i))   β‘β¨ f~-cocont (βCoyoneda.diagram A i) β©β‘
β (Ξ» j β f~ # (βCoyoneda.diagram A i j))                         β‘β¨ ap β (funext Ξ» j β f~-comm (j .fst) β sym (Lanβ-commutes (j .fst))) β©β‘
β (Ξ» j β Lanβ # (β A (j .fst)))                                  β‘Λβ¨ Lanβ-cocontinuous (βCoyoneda.diagram A i) β©β‘Λ
Lanβ # Lub.lub (Lower-sets-cocomplete A (βCoyoneda.diagram A i)) β‘Λβ¨ ap# Lanβ (βCoyoneda.lower-set-β« A i) β©β‘Λ
Lanβ # i                                                         β