open import Cat.Functor.Subcategory
open import Cat.Prelude

open import Order.Instances.Pointwise.Diagrams
open import Order.Diagram.Lub.Reasoning
open import Order.Instances.Pointwise
open import Order.Semilattice.Join
open import Order.Semilattice.Meet
open import Order.Instances.Props
open import Order.Diagram.Meet
open import Order.Diagram.Lub
open import Order.Diagram.Top
open import Order.Lattice
open import Order.Base

import Cat.Reasoning

import Order.Diagram.Meet.Reasoning as Meets
import Order.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 families, for an arbitrary type in the same universe as to have joins for arbitrary subsets of

record is-frame {o β} (P : Poset o β) : Type (lsuc o β β) where
no-eta-equality
open Poset P
field
_β©_     : Ob β Ob β Ob
β©-meets : β x y β is-meet P x y (x β© y)

has-top : Top P

β       : β {I : Type o} (k : I β Ob) β Ob
β-lubs  : β {I : Type o} (k : I β Ob) β is-lub P k (β k)

β-distribl : β {I} x (f : I β Ob) β x β© β f β‘ β Ξ» i β x β© f i


We have explicitly required that a frame be a meet-semilattice, but itβs worth explicitly pointing out that the infinitary join operation can also be used for more mundane purposes: By taking a join over the type of booleans (and over the empty type), we can show that all frames are also join-semilattices.

  infixr 25 _β©_

module is-lubs {I} {k : I β Ob} = is-lub (β-lubs k)

open Top has-top using (top; !) public
open Lubs P β-lubs public

has-meet-slat : is-meet-semilattice P
has-meet-slat .is-meet-semilattice.has-top = has-top

has-join-slat : is-join-semilattice P
has-join-slat .is-join-semilattice._βͺ_ = _βͺ_
has-join-slat .is-join-semilattice.βͺ-joins = βͺ-joins
has-join-slat .is-join-semilattice.has-bottom = has-bottom

has-lattice : is-lattice P
has-lattice .is-lattice._βͺ_ = _βͺ_
has-lattice .is-lattice.βͺ-joins = βͺ-joins
has-lattice .is-lattice.has-top = has-top
has-lattice .is-lattice.has-bottom = has-bottom

private variable
o β o' β' : Level
P Q R : Poset o β

abstract
is-frame-is-prop : is-prop (is-frame P)
is-frame-is-prop {P = P} p q = path where
open Order.Diagram.Top P using (H-Level-Top)

module p = is-frame p
module q = is-frame q
open is-frame

meetp : β x y β x p.β© y β‘ x q.β© y

lubp : β {I} (k : I β β P β) β p.β k β‘ q.β k
lubp k = lub-unique (p.β-lubs k) (q.β-lubs k)

path : p β‘ q
path i ._β©_     x y = meetp x y i
path i .β©-meets x y = is-propβpathp (Ξ» i β hlevel {T = is-meet P x y (meetp x y i)} 1) (p.β©-meets x y) (q.β©-meets x y) i
path i .has-top    = hlevel {T = Top P} 1 p.has-top q.has-top i
path i .β k        = lubp k i
path i .β-lubs k = is-propβpathp (Ξ» i β hlevel {T = is-lub P k (lubp k i)} 1) (p.β-lubs k) (q.β-lubs k) i
path i .β-distribl x f j = is-setβsquarep (Ξ» _ _ β Poset.Ob-is-set P)
(Ξ» i β meetp x (lubp f i) i)
(p.β-distribl x f) (q.β-distribl x f)
(Ξ» i β lubp (Ξ» e β meetp x (f e) i) i)
i j

instance
H-Level-is-frame : β {n} β H-Level (is-frame P) (suc n)
H-Level-is-frame = prop-instance is-frame-is-prop


Of course, a frame is not just a lattice, but a complete lattice. Since the infinite distributive law says exactly that βmeet with β preserves joins, this implies that it has a right adjoint, so frames are also complete Heyting algebras. Once again, the difference in naming reflects the morphisms we will consider these structures under: A frame homomorphism is a monotone map which preserves the finite meets and the infinitary joins, but not necessarily the infinitary meets (or the Heyting implication).

Since meets and joins are defined by a universal property, and we have assumed that homomorphisms are a priori monotone, it suffices to show the following inequalities:

• For every we have
• and finally, for every family we have
record
is-frame-hom
{P : Poset o β} {Q : Poset o β'}
(f : Monotone P Q) (P-frame : is-frame P) (Q-frame : is-frame Q)
: Type (lsuc o β β') where

  private
module P = Poset P
module PαΆ  = is-frame P-frame
module Q = Order.Reasoning Q
module QαΆ  = is-frame Q-frame
open is-lub

  field
β©-β€   : β x y β (f # x) QαΆ .β© (f # y) Q.β€ f # (x PαΆ .β© y)
top-β€ : QαΆ .top Q.β€ f # PαΆ .top
β-β€   : β {I : Type o} (k : I β β P β) β (f # PαΆ .β k) Q.β€ QαΆ .β (apply f β k)


If is a frame homomorphism, then it is also a homomorphism of meet semilattices.

  has-meet-slat-hom : is-meet-slat-hom f PαΆ .has-meet-slat QαΆ .has-meet-slat
has-meet-slat-hom .is-meet-slat-hom.top-β€ = top-β€

open is-meet-slat-hom has-meet-slat-hom hiding (β©-β€; top-β€) public


Furthermore, we can actually show from the inequality required above that preserves all joins up to equality.

  pres-β : β {I : Type o} (k : I β β P β) β (f # PαΆ .β k) β‘ QαΆ .β (apply f β k)
pres-β k =
Q.β€-antisym
(β-β€ k)
(QαΆ .β-universal _ (Ξ» i β f .pres-β€ (PαΆ .β-inj i)))

pres-lubs
: β {I : Type o} {k : I β β P β} {l}
β is-lub P k l
β is-lub Q (apply f β k) (f # l)
pres-lubs {k = k} {l = l} l-lub .famβ€lub i = f .pres-β€ (l-lub .famβ€lub i)
pres-lubs {k = k} {l = l} l-lub .least ub p =
f # l              Q.β€β¨ f .pres-β€ (l-lub .least _ PαΆ .β-inj) β©Q.β€
f # PαΆ .β k         Q.β€β¨ β-β€ k β©Q.β€
QαΆ .β (apply f β k) Q.β€β¨ QαΆ .β-universal ub p β©Q.β€
ub                 Q.β€β


As a corollary, is also a homomorphism of the underlying join semilattices.

  opaque
unfolding Lubs.βͺ-joins Lubs.has-bottom

has-join-slat-hom : is-join-slat-hom f PαΆ .has-join-slat QαΆ .has-join-slat
has-join-slat-hom .is-join-slat-hom.βͺ-β€ x y =
Q.β€-trans (β-β€ _) \$ QαΆ .β-universal _ Ξ» where
(lift true) β QαΆ .β-inj (lift true)
(lift false) β QαΆ .β-inj (lift false)
has-join-slat-hom .is-join-slat-hom.bot-β€ =
Q.β€-trans (β-β€ _) (QαΆ .β-universal _ (Ξ» ()))

open is-join-slat-hom has-join-slat-hom public

open is-frame-hom

unquoteDecl H-Level-is-frame-hom = declare-record-hlevel 1 H-Level-is-frame-hom (quote is-frame-hom)


Clearly, the identity function is a frame homomorphism.

id-frame-hom
: β (PαΆ  : is-frame P)
β is-frame-hom idβ PαΆ  PαΆ
id-frame-hom {P = P} PαΆ  .β©-β€ x y =
Poset.β€-refl P
id-frame-hom {P = P} PαΆ  .top-β€ =
Poset.β€-refl P
id-frame-hom {P = P} PαΆ  .β-β€ k =
Poset.β€-refl P


Furthermore, frame homomorphisms are closed under composition.

β-frame-hom
: β {Pβ Qβ Rβ} {f : Monotone Q R} {g : Monotone P Q}
β is-frame-hom f Qβ Rβ
β is-frame-hom g Pβ Qβ
β is-frame-hom (f ββ g) Pβ Rβ
β-frame-hom {R = R} {f = f} {g = g} f-pres g-pres .β©-β€ x y =
R .Poset.β€-trans (f-pres .β©-β€ (g # x) (g # y)) (f .pres-β€ (g-pres .β©-β€ x y))
β-frame-hom {R = R} {f = f} {g = g} f-pres g-pres .top-β€ =
R .Poset.β€-trans (f-pres .top-β€) (f .pres-β€ (g-pres .top-β€))
β-frame-hom {R = R} {f = f} {g = g} f-pres g-pres .β-β€ k =
R .Poset.β€-trans (f .pres-β€ (g-pres .β-β€ k)) (f-pres .β-β€ (Ξ» i β g # k i))


This means that we can define the category of frames as a subcategory of the category of posets.

Frame-subcat : β o β β Subcat (Posets o β) _ _
Frame-subcat o β .Subcat.is-ob = is-frame
Frame-subcat o β .Subcat.is-hom = is-frame-hom
Frame-subcat o β .Subcat.is-hom-prop _ _ _ = hlevel 1
Frame-subcat o β .Subcat.is-hom-id = id-frame-hom
Frame-subcat o β .Subcat.is-hom-β = β-frame-hom

Frames : β o β β Precategory _ _
Frames o β = Subcategory (Frame-subcat o β)

module Frames {o} {β} = Cat.Reasoning (Frames o β)

Frame : β o β β Type _
Frame o β = Frames.Ob {o} {β}


## Power sets as 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.

open is-frame
open is-meet-semilattice

Power-frame : β {β} (A : Type β) β Frame β β
Power-frame {β = β} A .fst = Subsets A
Power-frame A .snd ._β©_ P Q i = P i β§Ξ© Q i
Power-frame A .snd .β©-meets P Q =
is-meet-pointwise Ξ» _ β Props-has-meets (P _) (Q _)
Power-frame A .snd .has-top =
has-top-pointwise Ξ» _ β Props-has-top
Power-frame A .snd .β k i = βΞ© _ (Ξ» j β k j i)
Power-frame A .snd .β-lubs k = is-lub-pointwise _ _ Ξ» _ β
Props-has-lubs Ξ» i β k i _
Power-frame A .snd .β-distribl x f = funext Ξ» i β Ξ©-ua
(rec! Ξ» xi j j~i β inc (j , xi , j~i))
(rec! Ξ» j xi j~i β xi , inc (j , j~i))


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