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 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 Ξ» ()
is-bottom-is-prop : β x β is-prop (is-bottom x) is-bottom-is-prop _ = hlevel 1 bottom-unique : β {x y} β is-bottom x β is-bottom y β x β‘ y bottom-unique p q = β€-antisym (p _) (q _) Bottom-is-prop : is-prop Bottom Bottom-is-prop p q i .Bottom.bot = bottom-unique (Bottom.has-bottom p) (Bottom.has-bottom q) i Bottom-is-prop p q i .Bottom.has-bottom = is-propβpathp (Ξ» i β is-bottom-is-prop (bottom-unique (Bottom.has-bottom p) (Bottom.has-bottom q) i)) (Bottom.has-bottom p) (Bottom.has-bottom q) i instance H-Level-Bottom : β {n} β H-Level Bottom (suc n) H-Level-Bottom = prop-instance Bottom-is-prop BottomβLub : β {f : β₯ β _} β Bottom β Lub P f BottomβLub bottom .Lub.lub = Bottom.bot bottom BottomβLub bottom .Lub.has-lub = is-bottomβis-lub (Bottom.has-bottom bottom) LubβBottom : β {f : β₯ β _} β Lub P f β Bottom LubβBottom lub .Bottom.bot = Lub.lub lub LubβBottom lub .Bottom.has-bottom = is-lubβis-bottom (Lub.has-lub lub) is-bottomβis-lub : β {lub} {f} β is-equiv (is-bottomβis-lub {lub} {f}) is-bottomβis-lub = biimp-is-equiv! _ is-lubβis-bottom BottomβLub : β {f} β is-equiv (BottomβLub {f}) BottomβLub = biimp-is-equiv! _ LubβBottom
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