Definition. Frame [ag-000G]

{-# OPTIONS --safe --without-K #-}
module ag-000G where

open import MLTT.Spartan
open import UF.SubtypeClassifier
open import ag-000F

To build frame, we must be able to talk about arbitrary subsets of underlying set X

Fam : 𝓤 ̇  → 𝓤 ⁺ ̇
Fam {𝓤} A = Σ I ꞉ 𝓤 ̇ , (I → A)

module JoinStntax {A : 𝓤 ̇ } (join : Fam A → A) where
  join-of : {I : 𝓤 ̇ } → (I → A) → A
  join-of {I} f = join (I , f)

  syntax join-of (λ i → e) = ∨⟨ i ⟩ e

index : {X : 𝓤 ̇ } → Fam X → 𝓤 ̇
index (I , _) = I

_$_ : {X : 𝓤 ̇ } → (F : Fam X) → index F → X
_$_ (_ , f) = f
infixl  _$_

_∈_ : {X : 𝓤 ̇ } → X → Fam X → 𝓤 ̇
x ∈ (_ , f) = fiber f x

Beside poset axioms, frame axioms are

1. There is a top element ⊤, every element x ≤ ⊤
2. Binary meet x ∧ y is smaller than x and y, and it is a limit
3. Each arbitrary subset U has a join ∨U, such that each element of it smaller than the join
4. Binary meets must distribute over arbitrary joins

frame-axioms : (X : 𝓤 ̇ ) → order-structure X → X → (X → X → X) → (Fam X → X) → 𝓤 ⁺ ̇
frame-axioms X _≤_ ⊤ _∧_ ∨ =
  ((x : X) → (x ≤ ⊤) holds)
  × ((x y : X) → ((x ∧ y) ≤ x) holds × ((x ∧ y) ≤ y) holds)
  × ((x y z : X) → (z ≤ x) holds → (z ≤ y) holds → (z ≤ (x ∧ y)) holds)
  × ((U : Fam X) → (x : X) → x ∈ U → (x ≤ ∨ U) holds)
  × ((U : Fam X) → (x : X) → ((y : X) → y ∈ U → (y ≤ x) holds) → (∨ U ≤ x) holds)
  × distrib
  where
  open JoinStntax ∨
  distrib = ((U : Fam X) → (x : X) → x ∧ (∨ U) ＝ ∨⟨ i ⟩ (x ∧ U $ i))

Frame-structure : 𝓤 ̇  → 𝓤 ⁺ ̇
Frame-structure X =
  Σ _≤_ ꞉ order-structure X ,
  Σ ⊤ ꞉ X ,
  Σ _∧_ ꞉ (X → X → X) ,
  Σ ∨ ꞉ (Fam X → X) ,
  (poset-axioms X _≤_) × (frame-axioms X _≤_ ⊤ _∧_ ∨)

Frame : (𝓤 : Universe) → 𝓤 ⁺ ̇
Frame 𝓤 = Σ X ꞉ 𝓤 ̇ , Frame-structure X