open import Algebra.Semigroup open import Algebra.Magma open import Cat.Displayed.Univalence.Thin open import Cat.Prelude open import Order.Semilattice import Cat.Reasoning module Order.Frame where
Framesπ
A frame is a lattice with finite meets1 and arbitrary joins satisfying the infinite distributive law
In the study of frames, for simplicity, we assume propositional resizing
: that way, it suffices for a
frame
to have joins of
-indexed
families, for
an arbitrary type in the same universe as
,
to have joins for arbitrary subsets of
.
record is-frame (β€ : A) (_β©_ : A β A β A) (β : β {I : Type (level-of A)} β (I β A) β A) : Type (lsuc (level-of A)) where field has-meets : is-semilattice β€ _β©_
As usual, we define an ordering on in terms of the binary meets as iff . The properties of the join operator are then defined in terms of this ordering, rather than being defined algebraically. Thus, we have a mixed order-theoretic and algebraic presentation of frames.
field β-universal : β {I} {x} (f : I β A) β (β i β f i β€ x) β β f β€ x β-colimiting : β {I} i (f : I β A) β f i β€ β f β-distrib : β {I} x (f : I β A) β x β© β f β‘ β Ξ» i β x β© f i
Frames are, of course, complete lattices (and thus, also Heyting algebras). The difference in naming comes from the morphisms with which frames are considered: A frame homomorphism need only preserve the binary meets and arbitrary joins, and it does not need to preserve infinitary meets (or the Heyting implication).
record is-frame-hom {A B : Type β} (f : A β B) (X : Frame-on A) (Y : Frame-on B) : Type (lsuc β) where private module X = Frame-on X module Y = Frame-on Y field pres-β€ : f X.top β‘ Y.top pres-β© : β x y β f (x X.β© y) β‘ (f x Y.β© f y) pres-β : β {I} (g : I β A) β f (X.β g) β‘ Y.β Ξ» i β f (g i)
Frame homomorphisms still look like homomorphisms of algebraic structures, though, and so our usual machinery for constructing categories of βsets-with-structureβ applies here.
Frame-str : β β β Thin-structure {β = β} _ Frame-on Frame-str β .is-hom f x y .β£_β£ = is-frame-hom f x y Frame-str β .is-hom f x y .is-tr = Isoβis-hlevel 1 eqv (hlevel 1) where instance ahl : H-Level _ 2 ahl = hlevel-instance (Frame-on.has-is-set y) Frame-str β .id-is-hom .pres-β© x y = refl Frame-str β .id-is-hom .pres-β g = refl Frame-str β .id-is-hom .pres-β€ = refl Frame-str β .β-is-hom f g Ξ± Ξ² .pres-β© x y = ap f (Ξ² .pres-β© _ _) β Ξ± .pres-β© _ _ Frame-str β .β-is-hom f g Ξ± Ξ² .pres-β€ = ap f (Ξ² .pres-β€) β Ξ± .pres-β€ Frame-str β .β-is-hom f g Ξ± Ξ² .pres-β h = ap f (Ξ² .pres-β _) β Ξ± .pres-β _ Frame-str β .id-hom-unique Ξ± Ξ² i .Frame-on.top = Ξ± .pres-β€ i Frame-str β .id-hom-unique Ξ± Ξ² i .Frame-on._β©_ a b = Ξ± .pres-β© a b i Frame-str β .id-hom-unique Ξ± Ξ² i .Frame-on.β f = Ξ± .pres-β f i
Joins of subsetsπ
Imagine you have a frame whose carrier has size , and thus has joins for -small families of elements. But imagine that you have a second universe , and you have a -small predicate . Normally, youβd be out of luck: there is no reason for to admit -sized joins.
But since weβve assumed the existence of , we can resize (pointwise) to be valued in the universe ; That way we can turn the total space into a -small type! By projecting the first component, we have a -small family of elements, which has a join. This is a good definition for the join of the subset .
module _ {β} (F : Frames.Ob β) where private module F = Frame-on (F .snd) subset-cup : β {ββ²} (P : β F β β Prop ββ²) β β F β subset-cup P = F.β {I = Ξ£[ t β β F β ] (β‘ β£ P t β£)} Ξ» { (x , _) β x } subset-cup-colimiting : β {ββ²} (P : β F β β Prop ββ²) {x} β β£ P x β£ β x F.β€ subset-cup P subset-cup-colimiting P x = F.β-colimiting (_ , inc x) Ξ» { (f , w) β f } subset-cup-universal : β {ββ²} (P : β F β β Prop ββ²) {x} β (β i β β£ P i β£ β i F.β€ x) β subset-cup P F.β€ x subset-cup-universal P f = F.β-universal fst Ξ» { (i , w) β f i (out! w) }
Keep imagining that you have a subset : Can we construct a meet for it? Yes! By taking the join of all possible upper bounds for , we get the a lower bound among upper bounds of : a meet for .
subset-cap : β {ββ²} (P : β F β β Prop ββ²) β β F β subset-cap P = subset-cup Ξ» x β el! (β a β β£ P a β£ β x F.β€ a) subset-cap-limiting : β {ββ²} (P : β F β β Prop ββ²) {x} β β£ P x β£ β subset-cap P F.β€ x subset-cap-limiting P xβP = subset-cup-universal (Ξ» x β el _ hlevel!) Ξ» i aβPβiβ€a β aβPβiβ€a _ xβP subset-cap-universal : β {β} (P : β F β β Prop β) {x} β (β i β β£ P i β£ β x F.β€ i) β x F.β€ subset-cap P subset-cap-universal P xβP = subset-cup-colimiting (Ξ» _ β el _ hlevel!) xβP
Power framesπ
A canonical source of frames are power sets: The power set of any type is a frame, because it is a complete lattice satisfying the infinite distributive law; This can be seen by some computation, as is done below.
Power-frame : β {β} (A : Type β) β Frames.Ob β Power-frame {β = β} A .fst = el (A β Ξ©) (hlevel 2) Power-frame A .snd = to-frame-on go where go : make-frame (A β Ξ©) go .has-is-set = hlevel 2 go .top x = el β€ Ξ» _ _ i β tt go ._cap_ f g x .β£_β£ = β£ f x β£ Γ β£ g x β£ go ._cap_ f g x .is-tr = hlevel! go .identity = funext Ξ» i β Ξ©-ua snd (Ξ» x β tt , x) go .cup {I} P x = elΞ© (Ξ£ I Ξ» i β β£ P i x β£) go .idempotent = funext Ξ» i β Ξ©-ua fst Ξ» x β x , x go .commutative = funext Ξ» i β Ξ©-ua (Ξ» { (x , y) β y , x }) (Ξ» { (x , y) β y , x }) go .associative = funext Ξ» i β Ξ©-ua (Ξ» { (x , y , z) β (x , y) , z }) (Ξ» { ((x , y) , z) β x , y , z }) go .universal {x = x} f W = funext Ξ» i β Ξ©-ua (Ξ» r β β‘-rec! (Ξ» (a , w) β inc (_ , w) , transport (ap β£_β£ (W a $β i)) w .snd) r) (Ξ» r β r .fst) go .colimiting i f = funext Ξ» j β Ξ©-ua (Ξ» i β i , inc (_ , i)) fst go .distrib x f = funext Ξ» i β Ξ©-ua (Ξ» (x , i) β β‘-map (Ξ» (y , z) β _ , x , z) i) (Ξ» r β β‘-rec! (Ξ» { (x , y , z) β y , inc (_ , z) }) r)
So, in addition to the operation, we have a top elementβ©οΈ