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
record Frame-on (A : Type β) : Type (lsuc β) where field top : A _β©_ : A β A β A β : β {I : Type (level-of A)} β (I β A) β A has-is-frame : is-frame top _β©_ β open is-frame has-is-frame public
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)
private unquoteDecl eqv = declare-record-iso eqv (quote is-frame-hom) private unquoteDecl eqvβ² = declare-record-iso eqvβ² (quote is-frame) open Thin-structure open is-frame-hom
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
Frame-str β .id-hom-unique {s = s} {t} Ξ± Ξ² i .Frame-on.has-is-frame = is-propβpathp (Ξ» i β lemma (Ξ± .pres-β€ i) (Ξ» a b β Ξ± .pres-β© a b i) (Ξ» f β Ξ± .pres-β f i)) (s .Frame-on.has-is-frame) (t .Frame-on.has-is-frame) i where lemma : β top a (b : β {I} β (I β A) β A) β is-prop (is-frame top a b) lemma {A = A} top a b x = Isoβis-hlevel 1 eqvβ² (hlevel 1) x where instance ahl : H-Level A 2 ahl = hlevel-instance (is-frame.has-is-set x) Frames : β β β Precategory _ _ Frames a = Structured-objects (Frame-str a) module Frames β = Cat.Reasoning (Frames β) Frame : (β : Level) β Type (lsuc β) Frame β = Frames.Ob β
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
open Frame-on open is-semilattice open is-frame record make-frame {β} (A : Type β) : Type (lsuc β) where no-eta-equality field has-is-set : is-set A top : A _cap_ : A β A β A cup : β {I : Type β} β (I β A) β A identity : β {a} β top cap a β‘ a idempotent : β {a} β a cap a β‘ a commutative : β {a b} β a cap b β‘ b cap a associative : β {a b c} β a cap (b cap c) β‘ (a cap b) cap c _le_ : A β A β Type _ x le y = x β‘ x cap y field universal : β {I} {x} (f : I β A) β (β i β f i le x) β cup f le x colimiting : β {I} i (f : I β A) β f i le cup f distrib : β {I} x (f : I β A) β x cap cup f β‘ cup Ξ» i β x cap f i open make-frame open is-magma to-frame-on : β {β} {A : Type β} β make-frame A β Frame-on A to-frame-on mfr ._β©_ = mfr ._cap_ to-frame-on mfr .top = mfr .top to-frame-on mfr .β = mfr .cup to-frame-on mfr .has-is-frame .has-meets = to-semilattice-on mk .Semilattice-on.has-is-semilattice where mk : make-semilattice _ mk .make-semilattice.has-is-set = mfr .has-is-set mk .make-semilattice.top = mfr .top mk .make-semilattice.op = mfr ._cap_ mk .make-semilattice.idl = mfr .identity mk .make-semilattice.associative = mfr .associative mk .make-semilattice.commutative = mfr .commutative mk .make-semilattice.idempotent = mfr .idempotent to-frame-on mfr .has-is-frame .β-universal = mfr .universal to-frame-on mfr .has-is-frame .β-colimiting = mfr .colimiting to-frame-on mfr .has-is-frame .β-distrib = mfr .distrib
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β©οΈ