module Order.Diagram.Glb where
Greatest lower boundsπ
A glb (short for greatest lower bound) for a family of elements is, as the name implies, a greatest element among the lower bounds of the Being a lower bound means that we have for all Being the greatest lower bound means that if weβre given some other satisfying (for each then we have
A more common word to use for βgreatest lower boundβ is
βmeetβ. But since βmeetβ is a fairly uninformative name, and βglbβ
(pronounced βglibβ) is just plain fun to say, we stick with the non-word
for the indexed concept. However, if weβre talking about the glb of a
binary family, then we use the word βmeetβ. The distinction
here is entirely artificial, and itβs just because we canβt reuse the
identifier is-glb
for these two slightly
different cases. Summing up: to us, a meet is a glb of two elements.
record is-glb {βα΅’} {I : Type βα΅’} (F : I β Ob) (glb : Ob) : Type (o β β β βα΅’) where no-eta-equality field glbβ€fam : β i β glb β€ F i greatest : (lb' : Ob) β (β i β lb' β€ F i) β lb' β€ glb record Glb {βα΅’} {I : Type βα΅’} (F : I β Ob) : Type (o β β β βα΅’) where no-eta-equality field glb : Ob has-glb : is-glb F glb open is-glb has-glb public
unquoteDecl H-Level-is-glb = declare-record-hlevel 1 H-Level-is-glb (quote is-glb) module _ {o β} {P : Poset o β} where open Poset P open is-glb glb-unique : β {βα΅’} {I : Type βα΅’} {F : I β Ob} {x y} β is-glb P F x β is-glb P F y β x β‘ y glb-unique is is' = β€-antisym (is' .greatest _ (is .glbβ€fam)) (is .greatest _ (is' .glbβ€fam)) Glb-is-prop : β {βα΅’} {I : Type βα΅’} {F : I β Ob} β is-prop (Glb P F) Glb-is-prop p q i .Glb.glb = glb-unique (Glb.has-glb p) (Glb.has-glb q) i Glb-is-prop {F = F} p q i .Glb.has-glb = is-propβpathp {B = Ξ» i β is-glb P F (glb-unique (Glb.has-glb p) (Glb.has-glb q) i)} (Ξ» i β hlevel 1) (Glb.has-glb p) (Glb.has-glb q) i instance H-Level-Glb : β {βα΅’} {I : Type βα΅’} {F : I β Ob} {n} β H-Level (Glb P F) (suc n) H-Level-Glb = prop-instance Glb-is-prop lift-is-glb : β {βα΅’ βα΅’'} {I : Type βα΅’} {F : I β Ob} {glb} β is-glb P F glb β is-glb P (F β lower {β = βα΅’'}) glb lift-is-glb is .glbβ€fam (lift ix) = is .glbβ€fam ix lift-is-glb is .greatest ub' le = is .greatest ub' (le β lift) lift-glb : β {βα΅’ βα΅’'} {I : Type βα΅’} {F : I β Ob} β Glb P F β Glb P (F β lower {β = βα΅’'}) lift-glb glb .Glb.glb = Glb.glb glb lift-glb glb .Glb.has-glb = lift-is-glb (Glb.has-glb glb) lower-is-glb : β {βα΅’ βα΅’'} {I : Type βα΅’} {F : I β Ob} {glb} β is-glb P (F β lower {β = βα΅’'}) glb β is-glb P F glb lower-is-glb is .glbβ€fam ix = is .glbβ€fam (lift ix) lower-is-glb is .greatest ub' le = is .greatest ub' (le β lower) lower-glb : β {βα΅’ βα΅’'} {I : Type βα΅’} {F : I β Ob} β Glb P (F β lower {β = βα΅’'}) β Glb P F lower-glb glb .Glb.glb = Glb.glb glb lower-glb glb .Glb.has-glb = lower-is-glb (Glb.has-glb glb)
module _ {βα΅’ βα΅’'} {Ix : Type βα΅’} {Im : Type βα΅’'} {f : Ix β Im} {F : Im β Ob} (surj : is-surjective f) where cover-preserves-is-glb : β {glb} β is-glb P F glb β is-glb P (F β f) glb cover-preserves-is-glb g .glbβ€fam i = g .glbβ€fam (f i) cover-preserves-is-glb g .greatest lb' le = g .greatest lb' Ξ» i β β₯-β₯-out! do (i' , p) β surj i pure (β€-trans (le i') (β€-refl' (ap F p))) cover-preserves-glb : Glb P F β Glb P (F β f) cover-preserves-glb g .Glb.glb = _ cover-preserves-glb g .Glb.has-glb = cover-preserves-is-glb (g .Glb.has-glb) cover-reflects-is-glb : β {glb} β is-glb P (F β f) glb β is-glb P F glb cover-reflects-is-glb g .glbβ€fam i = β₯-β₯-out! do (y , p) β surj i pure (β€-trans (g .glbβ€fam y) (β€-refl' (ap F p))) cover-reflects-is-glb g .greatest lb' le = g .greatest lb' Ξ» i β le (f i) cover-reflects-glb : Glb P (F β f) β Glb P F cover-reflects-glb g .Glb.glb = _ cover-reflects-glb g .Glb.has-glb = cover-reflects-is-glb (g .Glb.has-glb)