module Order.Instances.Discrete where

Discrete OrdersπŸ”—

Every set AA can be turned into a poset by defining x≀yx \le y to be x=yx = 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 Sets\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 Sets\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→Af : I \to A has a least upper bound in the discrete poset on AA, then ff 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)