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

Bottom elements🔗

A bottom element in a partial order $(P, \leq)$ is an element $⊥ : P$ that is smaller than any other element of $P .$ This is the same as being a least upper upper bound for the empty family $⊥ \to P .$

is-bottom : Ob → Type _
is-bottom bot = ∀ x → bot ≤ x

record Bottom : Type (o ⊔ ℓ) where
  no-eta-equality
  field
    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