open import Cat.Diagram.Limit.Base
open import Cat.Diagram.Terminal
open import Cat.Diagram.Product
open import Cat.Prelude

open import Data.Bool

open import Order.Base
open import Order.Cat

import Order.Reasoning

module Order.Diagram.Glb where

module _ {o β„“} (P : Poset o β„“) where
  open Poset P

Greatest lower boundsπŸ”—

A glb (short for greatest lower bound) for a family of elements is, as the name implies, a greatest element among the lower bounds of the Being a lower bound means that we have for all Being the greatest lower bound means that if we’re given some other satisfying (for each then we have

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

unquoteDecl H-Level-is-glb = declare-record-hlevel 1 H-Level-is-glb (quote is-glb)

module _ {o β„“} {P : Poset o β„“} where
  open Poset P
  open is-glb

  glb-unique
    : βˆ€ {β„“α΅’} {I : Type β„“α΅’} {F : I β†’ Ob} {x y}
    β†’ is-glb P F x β†’ is-glb P F y
    β†’ x ≑ y
  glb-unique is is' = ≀-antisym
    (is' .greatest _ (is .glb≀fam))
    (is .greatest _ (is' .glb≀fam))

  Glb-is-prop
    : βˆ€ {β„“α΅’} {I : Type β„“α΅’} {F : I β†’ Ob}
    β†’ is-prop (Glb P F)
  Glb-is-prop p q i .Glb.glb =
    glb-unique (Glb.has-glb p) (Glb.has-glb q) i
  Glb-is-prop {F = F} p q i .Glb.has-glb =
    is-prop→pathp {B = λ i → is-glb P F (glb-unique (Glb.has-glb p) (Glb.has-glb q) i)}
      (Ξ» i β†’ hlevel 1)
      (Glb.has-glb p) (Glb.has-glb q) i

  instance
    H-Level-Glb
      : βˆ€ {β„“α΅’} {I : Type β„“α΅’} {F : I β†’ Ob} {n}
      β†’ H-Level (Glb P F) (suc n)
    H-Level-Glb = prop-instance Glb-is-prop

  lift-is-glb
    : βˆ€ {β„“α΅’ β„“α΅’'} {I : Type β„“α΅’} {F : I β†’ Ob} {glb}
    β†’ is-glb P F glb β†’ is-glb P (F βŠ™ lower {β„“ = β„“α΅’'}) glb
  lift-is-glb is .glb≀fam (lift ix) = is .glb≀fam ix
  lift-is-glb is .greatest ub' le = is .greatest ub' (le βŠ™ lift)

  lift-glb
    : βˆ€ {β„“α΅’ β„“α΅’'} {I : Type β„“α΅’} {F : I β†’ Ob}
    β†’ Glb P F β†’ Glb P (F βŠ™ lower {β„“ = β„“α΅’'})
  lift-glb glb .Glb.glb = Glb.glb glb
  lift-glb glb .Glb.has-glb = lift-is-glb (Glb.has-glb glb)

  lower-is-glb
    : βˆ€ {β„“α΅’ β„“α΅’'} {I : Type β„“α΅’} {F : I β†’ Ob} {glb}
    β†’ is-glb P (F βŠ™ lower {β„“ = β„“α΅’'}) glb β†’ is-glb P F glb
  lower-is-glb is .glb≀fam ix = is .glb≀fam (lift ix)
  lower-is-glb is .greatest ub' le = is .greatest ub' (le βŠ™ lower)

  lower-glb
    : βˆ€ {β„“α΅’ β„“α΅’'} {I : Type β„“α΅’} {F : I β†’ Ob}
    β†’ Glb P (F βŠ™ lower {β„“ = β„“α΅’'}) β†’ Glb P F
  lower-glb glb .Glb.glb = Glb.glb glb
  lower-glb glb .Glb.has-glb = lower-is-glb (Glb.has-glb glb)

  module _
    {β„“α΅’ β„“α΅’'} {Ix : Type β„“α΅’} {Im : Type β„“α΅’'}
    {f : Ix β†’ Im}
    {F : Im β†’ Ob}
    (surj : is-surjective f)
    where
      cover-preserves-is-glb : βˆ€ {glb} β†’ is-glb P F glb β†’ is-glb P (F βŠ™ f) glb
      cover-preserves-is-glb g .glb≀fam i = g .glb≀fam (f i)
      cover-preserves-is-glb g .greatest lb' le = g .greatest lb' Ξ» i β†’ βˆ₯-βˆ₯-out! do
        (i' , p) ← surj i
        pure (≀-trans (le i') (≀-refl' (ap F p)))

      cover-preserves-glb : Glb P F β†’ Glb P (F βŠ™ f)
      cover-preserves-glb g .Glb.glb = _
      cover-preserves-glb g .Glb.has-glb = cover-preserves-is-glb (g .Glb.has-glb)

      cover-reflects-is-glb : βˆ€ {glb} β†’ is-glb P (F βŠ™ f) glb β†’ is-glb P F glb
      cover-reflects-is-glb g .glb≀fam i = βˆ₯-βˆ₯-out! do
        (y , p) ← surj i
        pure (≀-trans (g .glb≀fam y) (≀-refl' (ap F p)))
      cover-reflects-is-glb g .greatest lb' le = g .greatest lb' Ξ» i β†’ le (f i)

      cover-reflects-glb : Glb P (F βŠ™ f) β†’ Glb P F
      cover-reflects-glb g .Glb.glb = _
      cover-reflects-glb g .Glb.has-glb = cover-reflects-is-glb (g .Glb.has-glb)

As limitsπŸ”—

If a poset has all greatest lower bounds of size then it is complete when viewed as a category.

module _ {o β„“} {P : Poset o β„“} where
  open Poset P

  glbs→complete
    : βˆ€ {oΞΊ β„“ΞΊ}
    β†’ (βˆ€ {I : Type oΞΊ} (k : I β†’ Ob) β†’ Glb P k)
    → is-complete oκ ℓκ (poset→category P)
  glbs→complete glbs K = to-limit (to-is-limit lim) where
    open make-is-limit
    module K = Functor K
    open Glb (glbs K.β‚€)

    lim : make-is-limit K glb
    lim .ψ = glb≀fam
    lim .commutes _ = prop!
    lim .universal eps _ = greatest _ eps
    lim .factors _ _ = prop!
    lim .unique _ _ _ _ = prop!