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\text{.}$ Being a lower bound means that we have $g\le a_i$ for all $i:I\text{;}$ Being the greatest lower bound means that if we’re given some other $m$ satisfying $m\le a_i$ (for each $i\text{),}$ then we have $m\le u\text{.}$

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