module Order.Instances.Discrete where
Discrete Ordersπ
Every set can be turned into a poset by defining to be .
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 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 .
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 has a least upper bound in the discrete poset on , then 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)