open import Algebra.Semigroup
open import Algebra.Magma

open import Cat.Prelude

open import Order.Diagram.Join
open import Order.Diagram.Glb
open import Order.Diagram.Lub
open import Order.Base

import Order.Diagram.Join.Reasoning as Joins
import Order.Diagram.Bottom
import Order.Reasoning

module Order.Diagram.Lub.Reasoning {o β„“} (P : Poset o β„“) where

open Order.Reasoning P
open Order.Diagram.Bottom P

Reasoning about least upper boundsπŸ”—

This module provides syntax and reasoning combinators for working with partial orders that have all least upper bounds.

module Lubs
  {⋃      : βˆ€ {I : Type o} (f : I β†’ Ob) β†’ Ob}
  (⋃-lubs : βˆ€ {I : Type o} (f : I β†’ Ob) β†’ is-lub P f (⋃ f))
  where

  lubs : βˆ€ {I : Type o} (f : I β†’ Ob) β†’ Lub P f
  lubs f = record { lub = ⋃ f ; has-lub = ⋃-lubs f }

  module ⋃-lubs {I} {f : I β†’ Ob} = is-lub (⋃-lubs f)
  open ⋃-lubs using () renaming (fam≀lub to ⋃-inj; least to ⋃-universal) public

Performing two nested joins over and is the same as taking a single join over 

  ⋃-twice
    : βˆ€ {I : Type o} {J : I β†’ Type o} (F : (i : I) β†’ J i β†’ Ob)
    β†’ ⋃ (Ξ» i β†’ ⋃ Ξ» j β†’ F i j)
    ≑ ⋃ {I = Ξ£ I J} (Ξ» p β†’ F (p .fst) (p .snd))
  ⋃-twice F = ≀-antisym
    (⋃-universal _ (Ξ» i β†’ ⋃-universal _ (Ξ» j β†’ ⋃-inj _)))
    (⋃-universal _ Ξ» (i , j) β†’ ≀-trans (⋃-inj j) (⋃-inj i))

Let and be a pair of families. If there is a map such that then the meet of is smaller than the meet of 

  ⋃≀⋃-over
    : βˆ€ {I J : Type o} {f : I β†’ Ob} {g : J β†’ Ob}
    β†’ (to : I β†’ J)
    β†’ (βˆ€ i β†’ f i ≀ g (to i))
    β†’ ⋃ f ≀ ⋃ g
  ⋃≀⋃-over to p = ⋃-universal _ Ξ» i β†’ ≀-trans (p i) (⋃-inj (to i))

As a corollary, if is smaller than for each then the join of is smaller than the join of 

  ⋃≀⋃
    : βˆ€ {I : Type o} {f g : I β†’ Ob}
    β†’ (βˆ€ i β†’ f i ≀ g i)
    β†’ ⋃ f ≀ ⋃ g
  ⋃≀⋃ = ⋃≀⋃-over (Ξ» i β†’ i)

Taking the join over a contractible family is equal the unique value of the family.

  ⋃-singleton
    : βˆ€ {I : Type o} {f : I β†’ Ob}
    β†’ (p : is-contr I)
    β†’ ⋃ f ≑ f (p .centre)
  ⋃-singleton {f = f} p = ≀-antisym
    (⋃-universal _ Ξ» i β†’ ≀-refl' $ sym $ ap f (p .paths i))
    (⋃-inj _)

We also provide syntax for binary joins and bottom elements.

  module _ (x y : Ob) where opaque
    private
      it : Join P x y
      it = Lub→Join (lower-lub (lubs _))

    infixr 24 _βˆͺ_
    _βˆͺ_ : Ob
    _βˆͺ_ = it .Join.lub

    βˆͺ-joins : is-join P x y _βˆͺ_
    βˆͺ-joins = it .Join.has-join

  opaque
    has-bottom : Bottom
    has-bottom = Lub→Bottom (lower-lub (lubs (λ ())))

  open Joins βˆͺ-joins public
  open Bottom has-bottom using (bot; Β‘) public

There is a distributive law relating binary and infinitary joins.

  βˆͺ-distrib-⋃-≀l
    : βˆ€ {I : Type o} {x : Ob} {f : I β†’ Ob}
    β†’ ⋃ (Ξ» i β†’ x βˆͺ f i) ≀ x βˆͺ ⋃ f
  βˆͺ-distrib-⋃-≀l =
    ⋃-universal _ Ξ» i β†’ βˆͺ-universal _ l≀βˆͺ (≀-trans (⋃-inj i) r≀βˆͺ)

If the infinitary join is taken over a non-empty family, then the previous distributive law can be extended to an equality.

  βˆͺ-distrib-nonempty-⋃-l
    : βˆ€ {I : Type o} {x : Ob} {f : I β†’ Ob}
    β†’ βˆ₯ I βˆ₯
    β†’ ⋃ (Ξ» i β†’ x βˆͺ f i) ≑ x βˆͺ ⋃ f
  βˆͺ-distrib-nonempty-⋃-l i =
    ≀-antisym
      βˆͺ-distrib-⋃-≀l
      (rec! (Ξ» i β†’ βˆͺ-universal _ (≀-trans l≀βˆͺ (⋃-inj i)) (⋃≀⋃ Ξ» _ β†’ r≀βˆͺ)) i)

  ⋃-ap
    : βˆ€ {I I' : Type o} {f : I β†’ Ob} {g : I' β†’ Ob}
    β†’ (e : I ≃ I')
    β†’ (βˆ€ i β†’ f i ≑ g (e .fst i))
    β†’ ⋃ f ≑ ⋃ g
  ⋃-ap e p = apβ‚‚ (Ξ» I f β†’ ⋃ {I = I} f) (ua e) (uaβ†’ p)

  -- raised i for "index", raised f for "family"
  ⋃-apⁱ : βˆ€ {I I' : Type o} {f : I' β†’ Ob} (e : I ≃ I') β†’ ⋃ (Ξ» i β†’ f (e .fst i)) ≑ ⋃ f
  ⋃-apαΆ  : βˆ€ {I : Type o} {f g : I β†’ Ob} β†’ (βˆ€ i β†’ f i ≑ g i) β†’ ⋃ f ≑ ⋃ g

  ⋃-apⁱ e = ⋃-ap e (Ξ» i β†’ refl)
  ⋃-apαΆ  p = ⋃-ap (_ , id-equiv) p

Large joinsπŸ”—

Let be a poset. If has all joins of size then it has all joins, regardless of size.

is-cocomplete→is-large-cocomplete
  : (lubs : βˆ€ {I : Type o} (f : I β†’ Ob) β†’ Lub P f)
  β†’ βˆ€ {β„“} {I : Type β„“} (F : I β†’ Ob) β†’ Lub P F
is-cocomplete→is-large-cocomplete lubs {I = I} F =
  cover-preserves-lub
    (Ξ©-corestriction-is-surjective F)
    (lubs fst)

We also provide some notation for large joins.

module
  Large
    {⋃ : {I : Type o} (F : I β†’ Ob) β†’ Ob}
    (⋃-lubs : βˆ€ {I} f β†’ is-lub P f (⋃ {I} f))
  where

  open Lubs ⋃-lubs using (lubs)

  opaque
    ⋃ᴸ : βˆ€ {β„“} {I : Type β„“} (F : I β†’ Ob) β†’ Ob
    ⋃ᴸ F = is-cocompleteβ†’is-large-cocomplete lubs F .Lub.lub

    ⋃ᴸ-inj : βˆ€ {β„“} {I : Type β„“} {F : I β†’ Ob} (i : I) β†’ F i ≀ ⋃ᴸ F
    ⋃ᴸ-inj = Lub.fam≀lub (is-cocompleteβ†’is-large-cocomplete lubs _)

    ⋃ᴸ-universal : βˆ€ {β„“} {I : Type β„“} {F : I β†’ Ob} (x : Ob) β†’ (βˆ€ i β†’ F i ≀ x) β†’ ⋃ᴸ F ≀ x
    ⋃ᴸ-universal = Lub.least (is-cocompleteβ†’is-large-cocomplete lubs _)

  ⋃ᴸ-ap
    : βˆ€ {β„“ β„“'} {I : Type β„“} {I' : Type β„“'} {f : I β†’ Ob} {g : I' β†’ Ob}
    β†’ (e : I ≃ I')
    β†’ (βˆ€ i β†’ f i ≑ g (e .fst i))
    β†’ ⋃ᴸ f ≑ ⋃ᴸ g
  ⋃ᴸ-ap {g = g} e p = ≀-antisym
    (⋃ᴸ-universal _ Ξ» i β†’ ≀-trans (≀-refl' (p i)) (⋃ᴸ-inj _))
    (⋃ᴸ-universal _ Ξ» i β†’ ≀-trans (≀-refl' (ap g (sym (Equiv.Ξ΅ e i)) βˆ™ sym (p (Equiv.from e _)))) (⋃ᴸ-inj _))

  -- raised i for "index", raised f for "family"
  ⋃ᴸ-apⁱ : βˆ€ {β„“ β„“'} {I : Type β„“} {I' : Type β„“'} {f : I' β†’ Ob} (e : I ≃ I') β†’ ⋃ᴸ (Ξ» i β†’ f (e .fst i)) ≑ ⋃ᴸ f
  ⋃ᴸ-apαΆ  : βˆ€ {β„“} {I : Type β„“} {f g : I β†’ Ob} β†’ (βˆ€ i β†’ f i ≑ g i) β†’ ⋃ᴸ f ≑ ⋃ᴸ g

  ⋃ᴸ-apⁱ e = ⋃ᴸ-ap e (Ξ» i β†’ refl)
  ⋃ᴸ-apαΆ  p = ⋃ᴸ-ap (_ , id-equiv) p