open import Cat.Diagram.Coproduct
open import Cat.Prelude

open import Data.Bool

open import Order.Base
open import Order.Cat

import Order.Reasoning as Poset

module Order.Diagram.Lub 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.

module _ { ℓ′} (P : Poset  ℓ′) where
  private module P = Poset P

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

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 : P.Ob) (lub : P.Ob) : Type (  ℓ′) where
    field
      l≤join : a P.≤ lub
      r≤join : b P.≤ lub
      least  : (ub′ : P.Ob)  a P.≤ ub′  b P.≤ ub′  lub P.≤ ub′

  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  P.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′

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 : P.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!