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 βŠ™ 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 βŠ™ 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 βŠ™ 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 βŠ™ lower)

  lower-lub
    : βˆ€ {β„“α΅’ β„“α΅’'} {I : Type β„“α΅’} {F : I β†’ Ob}
    β†’ Lub P (F βŠ™ 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 =
        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 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)