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

open import MLTT.Spartan
open import UF.Sets
open import UF.SubtypeClassifier

Order is a binary relation ≤.

order-structure : 𝓤 ̇  → 𝓤 ⁺ ̇
order-structure {𝓤} A = A → A → Ω 𝓤

A poset A is a pair (A,  ≤ )

1. x ≤ x for all x ∈ A
2. x ≤ y and y ≤ z implies x ≤ z for all x, y, z ∈ A
3. x ≤ y and y ≤ x implies x = y for all x, y ∈ A

poset-axioms : (A : 𝓤 ̇ ) → order-structure A → 𝓤 ̇
poset-axioms A _≤_ = is-set A
                    × ((x : A) → (x ≤ x) holds)
                    × ((x y z : A) → (x ≤ y) holds → (y ≤ z) holds → (x ≤ z) holds)
                    × ((x y : A) → (x ≤ y) holds → (y ≤ x) holds → x ＝ y)

Poset-structure : 𝓤 ̇  → 𝓤 ⁺ ̇
Poset-structure A = Σ _≤_ ꞉ order-structure A , (poset-axioms A _≤_)

Poset : (𝓤 : Universe) → 𝓤 ⁺ ̇
Poset 𝓤 = Σ A ꞉ 𝓤 ̇ , Poset-structure A

We can add a helper to extract underlying set

⟨_⟩ : {S : 𝓤 ̇ → 𝓥 ̇ } → Σ S → 𝓤 ̇
⟨ X , s ⟩ = X

order-of : (P : Poset 𝓤) → ⟨ P ⟩ → ⟨ P ⟩ → Ω 𝓤
order-of (X , _≤_ , _) x y = x ≤ y

syntax order-of P x y = x ≤⟨ P ⟩ y

posets-are-sets : (P : Poset 𝓤) → is-set ⟨ P ⟩
posets-are-sets (X , _≤_ , i , rfl , trans , ir) = i

A hom from a poset to another, is a map that preserves the order

is-hom : (P : Poset 𝓤) (Q : Poset 𝓥) → (⟨ P ⟩ → ⟨ Q ⟩) → 𝓤 ⊔ 𝓥 ̇
is-hom P Q f = ∀ {x y} → (x ≤⟨ P ⟩ y) holds → (f x ≤⟨ Q ⟩ f y) holds

Identity map is a hom

id-is-hom : (P : Poset 𝓤) → is-hom P P id
id-is-hom P x≤y = x≤y

The composition of homs is a hom

∘-is-hom : (P : Poset 𝓤) (Q : Poset 𝓥) (R : Poset 𝓦)
            (f : ⟨ P ⟩ → ⟨ Q ⟩) (g : ⟨ Q ⟩ → ⟨ R ⟩)
          → is-hom P Q f → is-hom Q R g → is-hom P R (g ∘ f)
∘-is-hom P Q R f g f-is-hom g-is-hom x≤y = g-is-hom (f-is-hom x≤y)

{-# 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

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

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

In frames, meet is commutative, hence no difference between x ∧ y and y ∧ x

meet-is-comm : (F : Frame 𝓤) → (x y : ⟨ F ⟩) → 𝓤 ̇
meet-is-comm (X , _≤_ , ⊤ , _∧_ , _ ) x y = x ∧ y ＝ y ∧ x

prove-meet-is-comm : (F : Frame 𝓤) → (x y : ⟨ F ⟩) → meet-is-comm F x y
prove-meet-is-comm (X , _≤_ , ⊤ , _∧_ , ∨ , (_ , _ , _ , split) , (_ , meet , lim , _ , _) ) x y = split (x ∧ y) (y ∧ x) I II
  where
  I : ((x ∧ y) ≤ (y ∧ x)) holds
  I = lim y x (x ∧ y) (meet x y .pr₂) (meet x y .pr₁)
  II : ((y ∧ x) ≤ (x ∧ y)) holds
  II = lim x y (y ∧ x) (meet y x .pr₂) (meet y x .pr₁)