open import Cat.Displayed.Total
open import Cat.Prelude

open import Order.Diagram.Lub
open import Order.Base

import Order.Reasoning as Poset

module Order.Instances.Discrete where


Discrete Ordersπ

Every set $A$ can be turned into a poset by defining $x \le y$ to be $x = y$.

Disc : β {β} β Set β β Poset β β
Disc A = to-poset β£ A β£ mk-disc where
mk-disc : make-poset _ (A .β£_β£)
mk-disc .make-poset.rel = _β‘_
mk-disc .make-poset.id = refl
mk-disc .make-poset.thin = A .is-tr _ _
mk-disc .make-poset.trans = _β_
mk-disc .make-poset.antisym p _ = p


This extends to a functor from $\mathbf{Sets}$ into the category of posets.

DiscF : β {β} β Functor (Sets β) (Posets β β)
DiscF .Functor.Fβ = Disc
DiscF .Functor.Fβ f = total-hom f (Ξ» _ _ p β ap f p)
DiscF .Functor.F-id = total-hom-path _ refl refl
DiscF .Functor.F-β f g = total-hom-path _ refl refl


Furthermore, this functor is a left adjoint to the forgetful functor into $\mathbf{Sets}$.

DiscFβ£Forget : β {β} β DiscF {β} β£ ΟαΆ  _
DiscFβ£Forget ._β£_.unit ._=>_.Ξ· A x = x
DiscFβ£Forget ._β£_.unit ._=>_.is-natural _ _ _ = refl
DiscFβ£Forget ._β£_.counit ._=>_.Ξ· P =
total-hom (Ξ» x β x) (Ξ» _ _ β Poset.pathββ€ P)
DiscFβ£Forget ._β£_.counit ._=>_.is-natural P Q f =
total-hom-path _ refl
(funext Ξ» _ β funext Ξ» _ β funext Ξ» _ β Poset.β€-thin Q _ _)
DiscFβ£Forget ._β£_.zig {A = A} =
total-hom-path _ refl \$
funext Ξ» x β funext Ξ» y β funext Ξ» p β
J (Ξ» y p β transport (Ξ» i β p (~ i) β‘ y) refl β‘ p) (transport-refl _) p
DiscFβ£Forget ._β£_.zag = refl


Least Upper Boundsπ

If $f : I \to A$ has a least upper bound in the discrete poset on $A$, then $f$ must be a constant family.

disc-is-lubβconst
: β {β iβ} {Ix : Type iβ} {A : Set β}
β {f : Ix β β£ A β£} {x : β£ A β£}
β is-lub (Disc A) f x
β β i β f i β‘ x
disc-is-lubβconst x-lub i = is-lub.famβ€lub x-lub i

disc-lubβconst
: β {β iβ} {Ix : Type iβ} {A : Set β}
β {f : Ix β β£ A β£}
β Lub (Disc A) f
β β i j β f i β‘ f j
disc-lubβconst x-lub i j =
Lub.famβ€lub x-lub i β sym (Lub.famβ€lub x-lub j)