module Order.Diagram.Glb {o ℓ} (P : Poset o ℓ) 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.

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

Meets🔗

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 : Ob) (glb : Ob) : Type (o ⊔ ℓ) where
  no-eta-equality
  field
    meet≤l   : glb ≤ a
    meet≤r   : glb ≤ b
    greatest : (lb' : Ob) → lb' ≤ a → lb' ≤ b → lb' ≤ glb

record Meet (a b : Ob) : Type (o ⊔ ℓ) where
  no-eta-equality
  field
    glb : Ob
    has-meet : is-meet a b glb
  open is-meet has-meet public

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 → 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 ≤ b → is-meet a b a
le→is-meet a≤b .meet≤l = ≤-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 ≤ b → is-meet a b l → a ≡ l
le-meet a≤b l = meet-unique (le→is-meet a≤b) l

As products🔗

When passing from posets to categories, meets become products: coming from the other direction, if a category $\mathcal{C}$ has each $\mathbf{Hom}(x,y)$ a proposition, then products in $\mathcal{C}$ are simply meets.

open is-product
open Product

is-meet→product : ∀ {a b glb : 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!

Top elements🔗

A top element in a partial order $(P, \le)$ is an element $\top : P$ that is larger than any other element in $P$ . This is the same as being a greatest lower bound for the empty family $\bot \to P$ .

is-top : Ob → Type _
is-top top = ∀ x → x ≤ top

record Top : Type (o ⊔ ℓ) where
  field
    top : Ob
    has-top : is-top top

is-top→is-glb : ∀ {glb} {f : ⊥ → _} → is-top glb → is-glb f glb
is-top→is-glb is-top .greatest x _ = is-top x

is-glb→is-top : ∀ {glb} {f : ⊥ → _} → is-glb f glb → is-top glb
is-glb→is-top glb x = glb .greatest x λ ()

As terminal objects🔗

Bottoms are the decategorifcation of terminal objects; we don’t need to require the uniqueness of the universal morphism, as we’ve replaced our hom-sets with hom-props!

is-top→terminal : ∀ {x} → is-top x → is-terminal (poset→category P) x
is-top→terminal is-top x .centre = is-top x
is-top→terminal is-top x .paths _ = ≤-thin _ _

terminal→is-top : ∀ {x} → is-terminal (poset→category P) x → is-top x
terminal→is-top terminal x = terminal x .centre