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