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

Least upper bounds🔗

A lub uu (short for least upper bound) for a family of elements (ai)i:I(a_i)_{i : I} is, as the name implies, a least elemnet among the upper boudns of the aia_i. Being an upper bound means that we have aiua_i \le u for all i:Ii : I; Being the least upper bound means that if we’re given some other ll satisfying aila_i \le l (for each ii), then we have ulu \le l.

The same observation about the naming of glbs vs meets applies to lubs, with the binary name being join.

record is-lub
  {ℓᵢ} {I : Type ℓᵢ} (F : I  Ob) (lub : Ob)
  : Type (o    ℓᵢ)
  where
  no-eta-equality
  field
    fam≤lub :  i  F i  lub
    least   : (ub′ : Ob)  (∀ i  F i  ub′)  lub  ub′

record Lub {ℓᵢ} {I : Type ℓᵢ} (F : I  Ob) : Type (o    ℓᵢ) where
  no-eta-equality
  field
    lub : Ob
    has-lub : is-lub F lub
  open is-lub has-lub public

open is-lub
private unquoteDecl eqv = declare-record-iso eqv (quote is-lub)

is-lub-is-prop
  :  {ℓᵢ} {I : Type ℓᵢ} {F : I  Ob} {lub : Ob}
   is-prop (is-lub F lub)
is-lub-is-prop = Iso→is-hlevel 1 eqv (hlevel 1)

instance
  H-Level-is-lub
    :  {ℓᵢ} {I : Type ℓᵢ} {F : I  Ob} {lub : Ob} {n}
     H-Level (is-lub F lub) (suc n)
  H-Level-is-lub = prop-instance is-lub-is-prop

lub-unique
  :  {ℓᵢ} {I : Type ℓᵢ} {F : I  Ob} {x y}
   is-lub F x  is-lub F y
   x  y
lub-unique {x = x} {y = y} lub lub' = ≤-antisym
  (lub .least y (lub' .fam≤lub))
  (lub' .least x (lub .fam≤lub))

Lub-is-prop
  :  {ℓᵢ} {I : Type ℓᵢ} {F : I  Ob}
   is-prop (Lub F)
Lub-is-prop p q i .Lub.lub =
  lub-unique (Lub.has-lub p) (Lub.has-lub q) i
Lub-is-prop {F = F} p q i .Lub.has-lub =
  is-prop→pathp
     i  is-lub-is-prop {lub = lub-unique (Lub.has-lub p) (Lub.has-lub q) i})
    (Lub.has-lub p) (Lub.has-lub q) i

instance
  H-Level-Lub
    :  {ℓᵢ} {I : Type ℓᵢ} {F : I  Ob} {n}
     H-Level (Lub F) (suc n)
  H-Level-Lub = prop-instance Lub-is-prop

lift-is-lub
  :  {ℓᵢ ℓᵢ'} {I : Type ℓᵢ} {F : I  Ob} {lub}
   is-lub F lub  is-lub (F  Lift.lower { = ℓᵢ'}) lub
lift-is-lub is .fam≤lub (lift ix) = is .fam≤lub ix
lift-is-lub is .least ub′ le = is .least ub′ (le  lift)

lift-lub
  :  {ℓᵢ ℓᵢ'} {I : Type ℓᵢ} {F : I  Ob}
   Lub F  Lub (F  Lift.lower { = ℓᵢ'})
lift-lub lub .Lub.lub = Lub.lub lub
lift-lub lub .Lub.has-lub = lift-is-lub (Lub.has-lub lub)

lower-is-lub
  :  {ℓᵢ ℓᵢ'} {I : Type ℓᵢ} {F : I  Ob} {lub}
   is-lub (F  Lift.lower { = ℓᵢ'}) lub  is-lub F lub
lower-is-lub is .fam≤lub ix = is .fam≤lub (lift ix)
lower-is-lub is .least ub′ le = is .least ub′ (le  Lift.lower)

lower-lub
  :  {ℓᵢ ℓᵢ'} {I : Type ℓᵢ} {F : I  Ob}
   Lub (F  Lift.lower { = ℓᵢ'})  Lub F
lower-lub lub .Lub.lub = Lub.lub lub
lower-lub lub .Lub.has-lub = lower-is-lub (Lub.has-lub lub)

Let f:IPf : I \to P be a family. If there is some ii such that for all jj, f(j)<f(i)f(j) < f(i), then f(i)f(i) is the least upper bound of ff.

fam-bound→is-lub
  :  {ℓᵢ} {I : Type ℓᵢ} {F : I  Ob}
   (i : I)  (∀ j  F j  F i)
   is-lub F (F i)
fam-bound→is-lub i ge .fam≤lub = ge
fam-bound→is-lub i ge .least y le = le i

If xx is the least upper bound of a constant family, then xx must be equal to every member of the family.

lub-of-const-fam
  :  {ℓᵢ} {I : Type ℓᵢ} {F : I  Ob} {x}
   (∀ i j  F i  F j)
   is-lub F x
    i  F i  x
lub-of-const-fam {F = F} is-const x-lub i =
  ≤-antisym
    (fam≤lub x-lub i)
    (least x-lub (F i) λ j  path→≥ (is-const i j))

Furthermore, if f:IAf : I \to A is a constant family and II is merely inhabited, then ff has a least upper bound.

const-inhabited-fam→is-lub
  :  {ℓᵢ} {I : Type ℓᵢ} {F : I  Ob} {x}
   (∀ i  F i  x)
    I 
   is-lub F x
const-inhabited-fam→is-lub {I = I} {F = F} {x = x} is-const =
  ∥-∥-rec is-lub-is-prop mk-is-lub where
    mk-is-lub : I  is-lub F x
    mk-is-lub i .is-lub.fam≤lub j = path→≤ (is-const j)
    mk-is-lub i .is-lub.least y le =
      x   =˘⟨ is-const i 
      F i ≤⟨ le i 
      y ≤∎

const-inhabited-fam→lub
  :  {ℓᵢ} {I : Type ℓᵢ} {F : I  Ob}
   (∀ i j  F i  F j)
    I 
   Lub F
const-inhabited-fam→lub {I = I} {F = F} is-const =
  ∥-∥-rec Lub-is-prop mk-lub where
    mk-lub : I  Lub F
    mk-lub i .Lub.lub = F i
    mk-lub i .Lub.has-lub =
      const-inhabited-fam→is-lub  j  is-const j i) (inc i)

Joins🔗

In the binary case, a least upper bound is called a join. A short computation shows that being a join is precisely being the lub of a family of two elements.

record is-join (a b : Ob) (lub : Ob) : Type (o  ) where
  no-eta-equality
  field
    l≤join : a  lub
    r≤join : b  lub
    least  : (ub′ : Ob)  a  ub′  b  ub′  lub  ub′

record Join (a b : Ob) : Type (o  ) where
  no-eta-equality
  field
    lub : Ob
    has-join : is-join a b lub
  open is-join has-join public

open is-join

is-join→is-lub :  {a b lub}  is-join a b lub  is-lub (if_then a else b) lub
is-join→is-lub join .fam≤lub true = join .l≤join
is-join→is-lub join .fam≤lub false = join .r≤join
is-join→is-lub join .least ub′ x = join .least ub′ (x true) (x false)

is-lub→is-join :  {F : Bool  Ob} {lub}  is-lub F lub  is-join (F true) (F false) lub
is-lub→is-join lub .l≤join = lub .fam≤lub true
is-lub→is-join lub .r≤join = lub .fam≤lub false
is-lub→is-join lub .least ub′ a<ub′ b<ub′ = lub .least ub′ λ where
  true   a<ub′
  false  b<ub′

An important lemma about joins is that, if xyx \le y, then the least upper bound of xx and yy is just yy:

gt→is-join :  {a b}  a  b  is-join a b b
gt→is-join a≤b .l≤join = a≤b
gt→is-join a≤b .r≤join = ≤-refl
gt→is-join a≤b .least ub′ _ b≤ub′ = b≤ub′

gt-join :  {a b l}  a  b  is-join a b l  b  l
gt-join a≤b l = join-unique (gt→is-join a≤b) l

As coproducts🔗

Joins are the “thinning” of coproducts; Put another way, when we allow a set of relators, rather than insisting on a propositional relation, the concept of join needs to be refined to that of coproduct.

open is-coproduct
open Coproduct

is-join→coproduct :  {a b lub : Ob}  is-join a b lub  Coproduct (poset→category P) a b
is-join→coproduct lub .coapex = _
is-join→coproduct lub .in₀ = lub .is-join.l≤join
is-join→coproduct lub .in₁ = lub .is-join.r≤join
is-join→coproduct lub .has-is-coproduct .[_,_] a<q b<q =
  lub .is-join.least _ a<q b<q
is-join→coproduct lub .has-is-coproduct .in₀∘factor = prop!
is-join→coproduct lub .has-is-coproduct .in₁∘factor = prop!
is-join→coproduct lub .has-is-coproduct .unique _ _ _ = prop!

Bottom elements🔗

A bottom element in a partial order (P,)(P, \le) is an element :P\bot : P that is smaller than any other element of PP. This is the same as being a least upper upper bound for the empty family P\bot \to P.

is-bottom : Ob  Type _
is-bottom bot =  x  bot  x

record Bottom : Type (o  ) where
  no-eta-equality
  field
    bot : Ob
    has-bottom : is-bottom bot

  ¡ :  {x}  bot  x
  ¡ = has-bottom _

is-bottom→is-lub :  {lub}  is-bottom lub  is-lub absurd lub
is-bottom→is-lub is-bot .least x _ = is-bot x

is-lub→is-bottom :  {lub}  is-lub absurd lub  is-bottom lub
is-lub→is-bottom lub x = lub .least x λ ()

As initial objects🔗

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

is-bottom→initial :  {x}  is-bottom x  is-initial (poset→category P) x
is-bottom→initial is-bot x .centre = is-bot x
is-bottom→initial is-bot x .paths _ = ≤-thin _ _

initial→is-bottom :  {x}  is-initial (poset→category P) x  is-bottom x
initial→is-bottom initial x = initial x .centre