open import Cat.Displayed.Univalence.Thin
open import Cat.Displayed.Total
open import Cat.Functor.Adjoint
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)