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πŸ”—

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 ⊀ _∩_

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

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)

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

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

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β†©οΈŽ