open import Cat.Diagram.Terminal
open import Cat.Prelude

open import Order.Diagram.Glb
open import Order.Base
open import Order.Cat

import Order.Reasoning

module Order.Diagram.Top {o β} (P : Poset o β) where

open Order.Reasoning P

open is-glb
open Glb


# 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
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 Ξ» ()

is-top-is-prop : β x β is-prop (is-top x)
is-top-is-prop _ = hlevel 1

top-unique : β {x y} β is-top x β is-top y β x β‘ y
top-unique p q = β€-antisym (q _) (p _)

Top-is-prop : is-prop Top
Top-is-prop p q i .Top.top =
top-unique (Top.has-top p) (Top.has-top q) i
Top-is-prop p q i .Top.has-top =
is-propβpathp
(Ξ» i β is-top-is-prop (top-unique (Top.has-top p) (Top.has-top q) i))
(Top.has-top p) (Top.has-top q) i

instance
H-Level-Top
: β {n}
β H-Level Top (suc n)
H-Level-Top = prop-instance Top-is-prop

TopβGlb : β {f : β₯ β _} β Top β Glb P f
TopβGlb top .Glb.glb = Top.top top
TopβGlb top .Glb.has-glb = is-topβis-glb (Top.has-top top)

GlbβTop : β {f : β₯ β _} β Glb P f β Top
GlbβTop glb .Top.top = Glb.glb glb
GlbβTop glb .Top.has-top = is-glbβis-top (Glb.has-glb glb)

is-topβis-glb : β {glb} {f} β is-equiv (is-topβis-glb {glb} {f})
is-topβis-glb = biimp-is-equiv! _ is-glbβis-top

TopβGlb : β {f} β is-equiv (TopβGlb {f})
TopβGlb = biimp-is-equiv! _ GlbβTop


### 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