module Order.Diagram.Top {o ℓ} (P : Poset o ℓ) where

Top elements🔗

A top element in a partial order $(P, \leq)$ is an element $⊤ : P$ that is larger than any other element in $P .$ This is the same as being a greatest lower bound for the empty family $⊥ \to P .$

is-top : Ob → Type _
is-top top = ∀ x → x ≤ top

record Top : Type (o ⊔ ℓ) where
  field
    top : Ob
    has-top : is-top top

  ! : ∀ {x} → x ≤ top
  ! = has-top _

is-top→is-glb : ∀ {glb} {f : ⊥ → _} → is-top glb → is-glb P f glb
is-top→is-glb is-top .greatest x _ = is-top x

is-glb→is-top : ∀ {glb} {f : ⊥ → _} → is-glb P f glb → is-top glb
is-glb→is-top glb x = glb .greatest x λ ()

As terminal objects🔗

Bottoms are the decategorifcation of terminal objects; we don’t need to require the uniqueness of the universal morphism, as we’ve replaced our hom-sets with hom-props!

is-top→terminal : ∀ {x} → is-top x → is-terminal (poset→category P) x
is-top→terminal is-top x .centre = is-top x
is-top→terminal is-top x .paths _ = ≤-thin _ _

terminal→is-top : ∀ {x} → is-terminal (poset→category P) x → is-top x
terminal→is-top terminal x = terminal x .centre