open import Cat.Displayed.Univalence.Thin
open import Cat.Displayed.Total
open import Cat.Prelude

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

module Order.Instances.Discrete where

open Functor
open Poset
open _β£_
open _=>_


# Discrete ordersπ

Every set can be turned into a poset by defining to be

Disc : β {β} β Set β β Poset β β
Disc A .Ob = β A β
Disc A ._β€_ = _β‘_
Disc A .β€-thin = A .is-tr _ _
Disc A .β€-refl = refl
Disc A .β€-trans = _β_
Disc A .β€-antisym p _ = p


We can do that same thing using the inductive identity type.

Discα΅’ : β {β} β Set β β Poset β β
Discα΅’ A .Ob = β A β
Discα΅’ A ._β€_ = _β‘α΅’_
Discα΅’ A .β€-thin = hlevel 1
Discα΅’ A .β€-refl = reflα΅’
Discα΅’ A .β€-trans = _βα΅’_
Discα΅’ A .β€-antisym reflα΅’ _ = refl


This extends to a functor from into the category of posets.

DiscF : β {β} β Functor (Sets β) (Posets β β)
DiscF .Fβ = Disc
DiscF .Fβ f .hom = f
DiscF .Fβ f .pres-β€ = ap f
DiscF .F-id = trivial!
DiscF .F-β f g = trivial!


Furthermore, this functor is a left adjoint to the forgetful functor into

DiscFβ£Forget : β {β} β DiscF {β} β£ PosetsβͺSets
DiscFβ£Forget .unit .Ξ· A x = x
DiscFβ£Forget .unit .is-natural _ _ _ = refl
DiscFβ£Forget .counit .Ξ· P .hom x  = x
DiscFβ£Forget .counit .Ξ· P .pres-β€ = Poset.β€-refl' P
DiscFβ£Forget .counit .is-natural P Q f = trivial!
DiscFβ£Forget .zig = trivial!
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)