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

open import Data.Bool

open import Order.Base
open import Order.Cat

import Order.Reasoning

module Order.Diagram.Glb where

module _ {o β} (P : Poset o β) where
open Poset P


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