module Order.Diagram.Meet where

MeetsšŸ”—

As mentioned before, in the binary case, we refer to glbs as meets: The meet of and is, if it exists, the greatest element satisfying and

record is-meet (P : Poset o ā„“) (a b glb : āŒž P ⌟) : Type (o āŠ” ā„“) where
  no-eta-equality
  open Poset P
  field
    meet≤l   : glb ≤ a
    meet≤r   : glb ≤ b
    greatest : (lb' : Ob) → lb' ≤ a → lb' ≤ b → lb' ≤ glb

record Meet (P : Poset o ā„“) (a b : āŒž P ⌟) : Type (o āŠ” ā„“) where
  no-eta-equality
  field
    glb : āŒž P ⌟
    has-meet : is-meet P a b glb
  open is-meet has-meet public

open is-meet

Has-meets : Poset o ā„“ → Type (o āŠ” ā„“)
Has-meets P = āˆ€ x y → Meet P x y

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 P a b glb → is-glb P (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 P F glb → is-meet P (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 then the greatest lower bound of and is just

  le→is-meet : āˆ€ {a b} → a ≤ b → is-meet P 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 P 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 has each a proposition, then products in are simply meets.

  open is-product
  open Product

  is-meet→product : āˆ€ {a b glb : Ob} → is-meet P 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 .Ļ€ā‚āˆ˜āŸØāŸ© = prop!
  is-meet→product glb .has-is-product .Ļ€ā‚‚āˆ˜āŸØāŸ© = prop!
  is-meet→product glb .has-is-product .unique _ _ = prop!