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

Bottom elementsπŸ”—

A bottom element in a partial order is an element that is smaller than any other element of This is the same as being a least upper upper bound for the empty family

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

record Bottom : Type (o βŠ” β„“) where
    bot : Ob
    has-bottom : is-bottom bot

  Β‘ : βˆ€ {x} β†’ bot ≀ x
  Β‘ = has-bottom _

is-bottomβ†’is-lub : βˆ€ {lub} {f : βŠ₯ β†’ _} β†’ is-bottom lub β†’ is-lub P f lub
is-bottom→is-lub is-bot .least x _ = is-bot x

is-lubβ†’is-bottom : βˆ€ {lub} {f : βŠ₯ β†’ _} β†’ is-lub P f lub β†’ is-bottom lub
is-lub→is-bottom lub x = lub .least x λ ()

As initial objectsπŸ”—

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

is-bottomβ†’initial : βˆ€ {x} β†’ is-bottom x β†’ is-initial (posetβ†’category P) x
is-bottom→initial is-bot x .centre = is-bot x
is-bottomβ†’initial is-bot x .paths _ = ≀-thin _ _

initialβ†’is-bottom : βˆ€ {x} β†’ is-initial (posetβ†’category P) x β†’ is-bottom x
initial→is-bottom initial x = initial x .centre