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

open import Data.Bool

open import Order.Base
open import Order.Cat

import Order.Reasoning

module Order.Diagram.Lub where

module _ {o â} (P : Poset o â) where
open Poset P


# Least upper boundsð

A lub (short for least upper bound) for a family of elements is, as the name implies, a least elemnet among the upper boudns of the Being an upper bound means that we have for all Being the least upper bound means that if weâre given some other satisfying (for each then we have

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

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

module _ {o â} {P : Poset o â} where
open Order.Reasoning P
open is-lub

lub-unique
: â {âáµ¢} {I : Type âáµ¢} {F : I â Ob} {x y}
â is-lub P F x â is-lub P 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 P 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 â hlevel {T = is-lub _ _ (lub-unique (Lub.has-lub p) (Lub.has-lub q) i)} 1)
(Lub.has-lub p) (Lub.has-lub q) i

instance
H-Level-Lub
: â {âáµ¢} {I : Type âáµ¢} {F : I â Ob} {n}
â H-Level (Lub P F) (suc n)
H-Level-Lub = prop-instance Lub-is-prop

lift-is-lub
: â {âáµ¢ âáµ¢'} {I : Type âáµ¢} {F : I â Ob} {lub}
â is-lub P F lub â is-lub P (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 P F â Lub P (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 P (F â Lift.lower {â = âáµ¢'}) lub â is-lub P 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 P (F â Lift.lower {â = âáµ¢'}) â Lub P F
lower-lub lub .Lub.lub = Lub.lub lub
lower-lub lub .Lub.has-lub = lower-is-lub (Lub.has-lub lub)

  module _
{âáµ¢ âáµ¢'} {Ix : Type âáµ¢} {Im : Type âáµ¢'}
{f : Ix â Im}
{F : Im â Ob}
(surj : is-surjective f)
where
cover-preserves-is-lub : â {lub} â is-lub P F lub â is-lub P (F â f) lub
cover-preserves-is-lub l .famâ€lub x = l .famâ€lub (f x)
cover-preserves-is-lub l .least   ub' le = l .least ub' Î» i â â¥-â¥-out! do
(i' , p) â surj i
pure (â€-trans (â€-refl' (ap F (sym p))) (le i'))

cover-preserves-lub : Lub P F â Lub P (F â f)
cover-preserves-lub l .Lub.lub = _
cover-preserves-lub l .Lub.has-lub = cover-preserves-is-lub (l .Lub.has-lub)

cover-reflects-is-lub : â {lub} â is-lub P (F â f) lub â is-lub P F lub
cover-reflects-is-lub l .famâ€lub x = â¥-â¥-out! do
(y , p) â surj x
pure (â€-trans (â€-refl' (ap F (sym p))) (l .famâ€lub y))
cover-reflects-is-lub l .least ub' le = l .least ub' Î» i â le (f i)

cover-reflects-lub : Lub P (F â f) â Lub P F
cover-reflects-lub l .Lub.lub     = _
cover-reflects-lub l .Lub.has-lub = cover-reflects-is-lub (l .Lub.has-lub)

cast-is-lub
: â {âáµ¢ âáµ¢'} {I : Type âáµ¢} {I' : Type âáµ¢'} {F : I â Ob} {G : I' â Ob} {lub}
â (e : I â I')
â (â i â F i â¡ G (Equiv.to e i))
â is-lub P F lub
â is-lub P G lub
cast-is-lub {G = G} e p has-lub .famâ€lub i' =
â€-trans
(â€-refl' (sym (p (Equiv.from e i') â ap G (Equiv.Îµ e i'))))
(has-lub .famâ€lub (Equiv.from e i'))
cast-is-lub e p has-lub .least ub Gâ€ub =
has-lub .least ub (Î» i â â€-trans (â€-refl' (p i)) (Gâ€ub (Equiv.to e i)))

cast-is-lubá¶
: â {âáµ¢} {I : Type âáµ¢} {F G : I â Ob} {lub}
â (â i â F i â¡ G i)
â is-lub P F lub
â is-lub P G lub
cast-is-lubá¶  {lub = lub} p has-lub = cast-is-lub (_ , id-equiv) p has-lub


Let be a family. If there is some such that for all then is the least upper bound of

  fam-boundâis-lub
: â {âáµ¢} {I : Type âáµ¢} {F : I â Ob}
â (i : I) â (â j â F j â€ F i)
â is-lub P F (F i)
fam-boundâis-lub i ge .famâ€lub = ge
fam-boundâis-lub i ge .least y le = le i


If is the least upper bound of a constant family, then 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 P 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 â â€-refl' (sym (is-const i j)))


Furthermore, if is a constant family and is merely inhabited, then has a least upper bound.

  const-inhabited-famâis-lub
: â {âáµ¢} {I : Type âáµ¢} {F : I â Ob} {x}
â (â i â F i â¡ x)
â â¥ I â¥
â is-lub P F x
const-inhabited-famâis-lub {I = I} {F = F} {x = x} is-const =
rec! mk-is-lub where
mk-is-lub : I â is-lub P F x
mk-is-lub i .is-lub.famâ€lub j = â€-refl' (is-const j)
mk-is-lub i .is-lub.least y le =
F i â€âš le i â©â€
y â€â

const-inhabited-famâlub
: â {âáµ¢} {I : Type âáµ¢} {F : I â Ob}
â (â i j â F i â¡ F j)
â â¥ I â¥
â Lub P F
const-inhabited-famâlub {I = I} {F = F} is-const =
rec! mk-lub where
mk-lub : I â Lub P 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)