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βˆ©β‹ƒif(i)=⋃i(x∩f(i)). 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 AA to have joins of J\mathcal{J}-indexed families, for J\mathcal{J} an arbitrary type in the same universe as AA, to have joins for arbitrary subsets of AA.

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 AA in terms of the binary meets as x≀yx \le y iff x≑x∩yx \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 AA 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:PΞ»(A)P : \mathbb{P}_{\lambda}(A). Normally, you’d be out of luck: there is no reason for AA to admit (ΞΊβŠ”Ξ»)(\kappa \sqcup \lambda)-sized joins.

But since we’ve assumed the existence of Ξ©\Omega, we can resize (pointwise) PP to be valued in the universe ΞΊ\kappa; That way we can turn the total space ∫P\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 PP.

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

  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∩yx \cap y operation, we have a top elementβ†©οΈŽ