module Order.Diagram.Lub.Reasoning {o â} (P : Poset o â) where
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