module Order.Diagram.Glb {o ℓ} (P : Poset o ℓ) where

Greatest lower bounds🔗

A glb gg (short for greatest lower bound) for a family of elements (ai)i:I(a_i)_{i : I} is, as the name implies, a greatest element among the lower bounds of the aia_i. Being a lower bound means that we have g≤aig \le a_i for all i:Ii : I; Being the greatest lower bound means that if we’re given some other mm satisfying m≤aim \le a_i (for each ii), then we have m≤um \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 aa and bb is, if it exists, the greatest element satisfying (a∩b)≤a(a \cap b) \le a and (a∩b)≤b(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
private unquoteDecl eqv' = declare-record-iso eqv' (quote is-meet)

instance
  H-Level-is-meet
    : ∀ {a b glb : Ob} {n}
    → H-Level (is-meet a b glb) (suc n)
  H-Level-is-meet = prop-instance $ Iso→is-hlevel 1 eqv' hlevel!

meet-unique : ∀ {a b x y} → is-meet a b x → is-meet a b y → x ≡ y
meet-unique x-meet y-meet =
  glb-unique (is-meet→is-glb x-meet) (is-meet→is-glb y-meet)

Meet-is-prop : ∀ {a b} → is-prop (Meet a b)
Meet-is-prop p q i .Meet.glb =
  meet-unique (Meet.has-meet p) (Meet.has-meet q) i
Meet-is-prop {a = a} {b = b} p q i .Meet.has-meet =
  is-prop→pathp {B = λ i → is-meet a b (meet-unique (Meet.has-meet p) (Meet.has-meet q) i)}
    (λ i → hlevel 1)
    (Meet.has-meet p) (Meet.has-meet q) i

instance
  H-Level-Meet
    : ∀ {a b} {n}
    → H-Level (Meet a b) (suc n)
  H-Level-Meet = prop-instance Meet-is-prop

Meet→Glb : ∀ {a b} → Meet a b → Glb (if_then a else b)
Meet→Glb meet .Glb.glb = Meet.glb meet
Meet→Glb meet .Glb.has-glb = is-meet→is-glb (Meet.has-meet meet)

Glb→Meet : ∀ {a b} → Glb (if_then a else b) → Meet a b
Glb→Meet glb .Meet.glb = Glb.glb glb
Glb→Meet glb .Meet.has-meet = is-glb→is-meet (Glb.has-glb glb)

is-meet≃is-glb : ∀ {a b glb : Ob} → is-equiv (is-meet→is-glb {a} {b} {glb})
is-meet≃is-glb = prop-ext! _ is-glb→is-meet .snd

Meet≃Glb : ∀ {a b} → is-equiv (Meet→Glb {a} {b})
Meet≃Glb = prop-ext! _ Glb→Meet .snd

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

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 C\mathcal{C} has each Hom(x,y)\mathbf{Hom}(x,y) a proposition, then products in C\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,≤)(P, \le) is an element ⊤:P\top : P that is larger than any other element in PP. This is the same as being a greatest lower bound for the empty family ⊥→P\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