Properties of frames [ag-000H]

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