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π

private variable
β ββ² : Level
A B : Type β


A frame is a lattice with finite meets1 and arbitrary joins satisfying the infinite distributive law

$x \cap \bigcup_i f(i) = \bigcup_i (x \cap f(i))\text{.}$

In the study of frames, for simplicity, we assume propositional resizing: that way, it suffices for a frame $A$ to have joins of $\mathcal{J}$-indexed families, for $\mathcal{J}$ an arbitrary type in the same universe as $A$, to have joins for arbitrary subsets of $A$.

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 β€ _β©_

  open is-semilattice has-meets public
_β€_ : A β A β Type _
x β€ y = x β‘ x β© y


As usual, we define an ordering on $A$ in terms of the binary meets as $x \le y$ iff $x \equiv x \cap y$. 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 $A$ whose carrier has size $\kappa$, and thus has joins for $\kappa$-small families of elements. But imagine that you have a second universe $\lambda$, and you have a $\lambda$-small predicate $P : \mathbb{P}_{\lambda}(A)$. Normally, youβd be out of luck: there is no reason for $A$ to admit $(\kappa \sqcup \lambda)$-sized joins.

But since weβve assumed the existence of $\Omega$, we can resize (pointwise) $P$ to be valued in the universe $\kappa$; That way we can turn the total space $\int P$ into a $\kappa$-small type! By projecting the first component, we have a $\kappa$-small family of elements, which has a join. This is a good definition for the join of the subset $P$.

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 $P \sube A$: Can we construct a meet for it? Yes! By taking the join of all possible upper bounds for $P$, we get the a lower bound among upper bounds of $P$: a meet for $P$.

  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)


1. So, in addition to the $x \cap y$ operation, we have a top elementβ©οΈ