module Order.Diagram.Top {o β„“} (P : Poset o β„“) where

Top elementsπŸ”—

A top element in a partial order is an element that is larger than any other element in This is the same as being a greatest lower bound for the empty family

is-top : Ob β†’ Type _
is-top top = βˆ€ x β†’ x ≀ top

record Top : Type (o βŠ” β„“) where
    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