module Order.Frame where


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
  open Poset P
    _∩_     : 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 Meets ∩-meets public
  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-meet-slat .is-meet-semilattice.∩-meets = ∩-meets
  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.∩-meets = ∩-meets
  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 β„“

  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
    meetp x y = meet-unique (p.∩-meets x y) (q.∩-meets x 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

  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
    {P : Poset o β„“} {Q : Poset o β„“'}
    (f : Monotone P Q) (P-frame : is-frame P) (Q-frame : is-frame Q)
    : Type (lsuc o βŠ” β„“') where
    ∩-≀   : βˆ€ 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.∩-≀ = ∩-≀
  has-meet-slat-hom≀ = 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 =
      (⋃-≀ k)
      (QαΆ .⋃-universal _ (Ξ» i β†’ f .pres-≀ (PαΆ .⋃-inj i)))

    : βˆ€ {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.

    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≀ =
      Q.≀-trans (⋃-≀ _) (QαΆ .⋃-universal _ (Ξ» ()))

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

open is-frame-hom

Clearly, the identity function is a frame homomorphism.

  : βˆ€ (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.

  : βˆ€ {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 β„“ = is-frame
Frame-subcat o β„“ = is-frame-hom
Frame-subcat o β„“ _ _ _ = hlevel 1
Frame-subcat o β„“ = id-frame-hom
Frame-subcat o β„“∘ = ∘-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β†©οΈŽ