open import Cat.Diagram.Product open import Cat.Prelude open import Data.Bool open import Order.Base open import Order.Cat import Order.Reasoning as Poset module Order.Diagram.Glb where

# Greatest lower bounds🔗

A **glb**
$g$
(short for **greatest lower bound**) for a family of
elements
$(a_i)_{i : I}$
is, as the name implies, a greatest element among the lower bounds of
the
$a_i$.
Being a lower bound means that we have
$g \le a_i$
for all
$i : I$;
Being the *greatest* lower bound means that if we’re given some
other
$m$
satisfying
$m \le a_i$
(for each
$i$),
then we have
$m \le u$.

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.

module _ {ℓ ℓ′} (P : Poset ℓ ℓ′) where private module P = Poset P record is-glb {ℓᵢ} {I : Type ℓᵢ} (F : I → P.Ob) (glb : P.Ob) : Type (ℓ ⊔ ℓ′ ⊔ ℓᵢ) where field glb≤fam : ∀ i → glb P.≤ F i greatest : (lb′ : P.Ob) → (∀ i → lb′ P.≤ F i) → lb′ P.≤ glb

As mentioned before, in the binary case, we refer to glbs as
**meets**: The meet of
$a$
and
$b$
is, if it exists, the greatest element satisfying
$(a \cap b) \le a$
and
$(a \cap b) \le b$.

record is-meet (a b : P.Ob) (glb : P.Ob) : Type (ℓ ⊔ ℓ′) where field meet≤l : glb P.≤ a meet≤r : glb P.≤ b greatest : (lb′ : P.Ob) → lb′ P.≤ a → lb′ P.≤ b → lb′ P.≤ glb open is-meet

A shuffling of terms shows that being a meet is precisely being the greatest lower bound of a family of two elements.

is-meet→is-glb : ∀ {a b glb} → is-meet a b glb → is-glb (if_then a else b) glb is-meet→is-glb meet .glb≤fam true = meet .meet≤l is-meet→is-glb meet .glb≤fam false = meet .meet≤r is-meet→is-glb meet .greatest glb′ x = meet .greatest glb′ (x true) (x false) is-glb→is-meet : ∀ {F : Bool → P.Ob} {glb} → is-glb F glb → is-meet (F true) (F false) glb is-glb→is-meet glb .meet≤l = glb .glb≤fam true is-glb→is-meet glb .meet≤r = glb .glb≤fam false is-glb→is-meet glb .greatest lb′ lb′<a lb′<b = glb .greatest lb′ λ where true → lb′<a false → lb′<b

An important lemma about meets is that, if $x \le y$, then the greatest lower bound of $x$ and $y$ is just $x$:

le→is-meet : ∀ {a b} → a P.≤ b → is-meet a b a le→is-meet a≤b .meet≤l = P.≤-refl le→is-meet a≤b .meet≤r = a≤b le→is-meet a≤b .greatest lb′ lb′≤a _ = lb′≤a le-meet : ∀ {a b l} → a P.≤ b → is-meet a b l → a ≡ l le-meet a≤b l = ap fst $ meet-unique (_ , le→is-meet a≤b) (_ , l)

## As products🔗

The categorification of meets is *products*: put another way,
if our category has propositional homs, then being given a product
diagram is the same as being given a meet.

open is-product open Product is-meet→product : ∀ {a b glb : P.Ob} → is-meet a b glb → Product (poset→category P) a b is-meet→product glb .apex = _ is-meet→product glb .π₁ = glb .is-meet.meet≤l is-meet→product glb .π₂ = glb .is-meet.meet≤r is-meet→product glb .has-is-product .⟨_,_⟩ q<a q<b = glb .is-meet.greatest _ q<a q<b is-meet→product glb .has-is-product .π₁∘factor = prop! is-meet→product glb .has-is-product .π₂∘factor = prop! is-meet→product glb .has-is-product .unique _ _ _ = prop!