Ayberk Tosun, 8 March 2021.

Ported from `ayberkt/formal-topology-in-UF`.

 * Frames.
 * Frame homomorphisms.
 * Frame bases.

\begin{code}[hide]

{-# OPTIONS --safe --without-K #-}

open import MLTT.Spartan hiding (𝟚; β‚€; ₁)
open import UF.Base
open import UF.FunExt
open import UF.PropTrunc
open import MLTT.List hiding ([_])

module Locales.Frame
        (pt : propositional-truncations-exist)
        (fe : Fun-Ext)
       where

open import Slice.Family
open import UF.Hedberg
open import UF.Logic
open import UF.Sets
open import UF.Sets-Properties
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.Subsingletons-Properties
open import UF.SubtypeClassifier
open import UF.SubtypeClassifier-Properties

open AllCombinators pt fe

\end{code}

\section{Preliminaries}

\begin{code}

private
  variable
    𝓀′ π“₯β€² 𝓦′ 𝓀′′ π“₯β€²β€² : Universe

\end{code}

We define some order-theoretic notions that are also defined in the
`Dcpo` module. Ideally, this should be factored out into a standalone
module to be imported by both this module and the `Dcpo` module.

\begin{code}

is-reflexive : {A : 𝓀 Μ‡ } β†’ (A β†’ A β†’ Ξ© π“₯) β†’ Ξ© (𝓀 βŠ” π“₯)
is-reflexive {A = A} _≀_ = β±― x κž‰ A , x ≀ x

is-transitive : {A : 𝓀 Μ‡ } β†’ (A β†’ A β†’ Ξ© π“₯) β†’ Ξ© (𝓀 βŠ” π“₯)
is-transitive {A = A} _≀_ =
 β±― x κž‰ A , β±― y κž‰ A , β±― z κž‰ A , x ≀ y β‡’ y ≀ z β‡’ x ≀ z

is-preorder : {A : 𝓀 Μ‡ } β†’ (A β†’ A β†’ Ξ© π“₯) β†’ Ξ© (𝓀 βŠ” π“₯)
is-preorder {A = A} _≀_ = is-reflexive _≀_ ∧ is-transitive _≀_

\end{code}

Antisymmetry is not propositional unless A is a set. We will always
work with sets but the fact they are sets will be a corollary of their
equipment with an antisymmetric order so they are not sets a priori.

\begin{code}

is-antisymmetric : {A : 𝓀 Μ‡ } β†’ (A β†’ A β†’ Ξ© π“₯) β†’ (𝓀 βŠ” π“₯) Μ‡
is-antisymmetric {A = A} _≀_ = {x y : A} β†’ (x ≀ y) holds β†’ (y ≀ x) holds β†’ x ＝ y

being-antisymmetric-is-prop : {A : 𝓀 Μ‡ } (_≀_ : A β†’ A β†’ Ξ© π“₯)
                            β†’ is-set A
                            β†’ is-prop (is-antisymmetric _≀_)
being-antisymmetric-is-prop {𝓀} {A} _≀_ A-is-set =
 Ξ -is-prop' fe (Ξ» x β†’ Ξ -is-prop' fe (Ξ» y β†’ Ξ β‚‚-is-prop fe (Ξ» _ _ β†’ A-is-set {x} {y})))

is-partial-order : (A : 𝓀 Μ‡ )β†’ (A β†’ A β†’ Ξ© π“₯) β†’ 𝓀 βŠ” π“₯ Μ‡
is-partial-order A _≀_ = is-preorder _≀_ holds Γ—  is-antisymmetric _≀_

being-partial-order-is-prop : (A : 𝓀 Μ‡ )(_≀_ : A β†’ A β†’ Ξ© π“₯)
                            β†’ is-prop (is-partial-order A _≀_)
being-partial-order-is-prop A _≀_ = prop-criterion Ξ³
 where
  Ξ³ : is-partial-order A _≀_ β†’ is-prop (is-partial-order A _≀_)
  Ξ³ (p , a) = Γ—-is-prop
               (holds-is-prop (is-preorder _≀_))
               (being-antisymmetric-is-prop _≀_ i)
   where
    i : is-set A
    i = type-with-prop-valued-refl-antisym-rel-is-set
         (Ξ» x y β†’ (x ≀ y) holds)
         (Ξ» x y β†’ holds-is-prop (x ≀ y))
         (pr₁ p)
         (Ξ» x y β†’ a {x} {y})

\end{code}

\section{Definition of poset}

A (𝓀, π“₯)-poset is a poset whose

  - carrier lives in universe 𝓀, and
  - whose relation lives in universe π“₯.

\begin{code}

poset-structure : (π“₯ : Universe) β†’ 𝓀 Μ‡ β†’ 𝓀 βŠ” π“₯ ⁺ Μ‡
poset-structure π“₯ A =
 Ξ£ _≀_ κž‰ (A β†’ A β†’ Ξ© π“₯) , (is-partial-order A _≀_)

Poset : (𝓀 π“₯ : Universe) β†’ 𝓀 ⁺ βŠ” π“₯ ⁺ Μ‡
Poset 𝓀 π“₯ = Ξ£ A κž‰ 𝓀 Μ‡ , poset-structure π“₯ A

∣_βˆ£β‚š : Poset 𝓀 π“₯ β†’ 𝓀 Μ‡
∣ A , _ βˆ£β‚š = A

rel-syntax : (P : Poset 𝓀 π“₯)  β†’ ∣ P βˆ£β‚š β†’ ∣ P βˆ£β‚š β†’ Ξ© π“₯
rel-syntax (_ , _≀_ , _) = _≀_

infix 5 rel-syntax

syntax rel-syntax P x y = x ≀[ P ] y

poset-eq-syntax : (P : Poset 𝓀 π“₯) β†’ ∣ P βˆ£β‚š β†’ ∣ P βˆ£β‚š β†’ Ξ© π“₯
poset-eq-syntax P x y = x ≀[ P ] y ∧ y ≀[ P ] x

syntax poset-eq-syntax P x y = x ≣[ P ] y

≀-is-reflexive : (P : Poset 𝓀 π“₯)
               β†’ is-reflexive (Ξ» x y β†’ x ≀[ P ] x) holds
≀-is-reflexive (_ , _ , ((r , _) , _)) = r

≣-is-reflexive : (P : Poset 𝓀 π“₯) β†’ is-reflexive (Ξ» x y β†’ x ≣[ P ] x) holds
≣-is-reflexive P x = ≀-is-reflexive P x , ≀-is-reflexive P x

reflexivity+ : (P : Poset 𝓀 π“₯)
             β†’ {x y : pr₁ P} β†’ x ＝ y β†’ (x ≀[ P ] y) holds
reflexivity+ P {x} {y} p =
 transport (Ξ» - β†’ (x ≀[ P ] -) holds) p (≀-is-reflexive P x)

≀-is-transitive : (P : Poset 𝓀 π“₯)
                β†’ is-transitive (Ξ» x y β†’ x ≀[ P ] y) holds
≀-is-transitive (_ , _ , ((_ , t) , _)) = t

≀-is-antisymmetric : (P : Poset 𝓀 π“₯)
                   β†’ is-antisymmetric (Ξ» x y β†’ x ≀[ P ] y)
≀-is-antisymmetric (_ , _ , (_ , a)) = a

carrier-of-[_]-is-set : (P : Poset 𝓀 π“₯) β†’ is-set ∣ P βˆ£β‚š
carrier-of-[_]-is-set P@ (A , _)=
 type-with-prop-valued-refl-antisym-rel-is-set
  (Ξ» x y β†’ (x ≀[ P ] y) holds)
  (Ξ» x y β†’ holds-is-prop (x ≀[ P ] y))
  (≀-is-reflexive P)
  (Ξ» x y β†’ ≀-is-antisymmetric P {x} {y})

\end{code}

Some convenient syntax for reasoning with posets.

\begin{code}

module PosetNotation (P : Poset 𝓀 π“₯) where

 _≀_ : ∣ P βˆ£β‚š β†’ ∣ P βˆ£β‚š β†’ Ξ© π“₯
 x ≀ y = x ≀[ P ] y

 infix 4 _≀_

 _≣_ : ∣ P βˆ£β‚š β†’ ∣ P βˆ£β‚š β†’ Ξ© π“₯
 x ≣ y = x ≣[ P ] y

module PosetReasoning (P : Poset 𝓀 π“₯) where

 open PosetNotation P using (_≀_)

 _β‰€βŸ¨_⟩_ : (x : ∣ P βˆ£β‚š) {y z : ∣ P βˆ£β‚š}
        β†’ (x ≀ y) holds β†’ (y ≀ z) holds β†’ (x ≀ z) holds
 x β‰€βŸ¨ p ⟩ q = ≀-is-transitive P _ _ _ p q

 _＝⟨_βŸ©β‚š_ : (x : ∣ P βˆ£β‚š) {y z : ∣ P βˆ£β‚š}
         β†’ x ＝ y β†’ (y ≀ z) holds β†’ (x ≀ z) holds
 x ＝⟨ p βŸ©β‚š q = transport (Ξ» - β†’ (- ≀ _) holds) (p ⁻¹) q

 _β–  : (x : ∣ P βˆ£β‚š) β†’ (x ≀ x) holds
 _β–  = ≀-is-reflexive P

 infixr 0 _β‰€βŸ¨_⟩_
 infixr 0 _＝⟨_βŸ©β‚š_
 infix  1 _β– 

infix 1 _＝[_]＝_

_＝[_]＝_ : {A : 𝓀 Μ‡ } β†’ A β†’ is-set A β†’ A β†’ Ξ© 𝓀
x ＝[ iss ]＝ y = (x ＝ y) , iss

\end{code}

\section{Meets}

\begin{code}

module Meets {A : 𝓀 Μ‡ } (_≀_ : A β†’ A β†’ Ξ© π“₯) where

 is-top : A β†’ Ξ© (𝓀 βŠ” π“₯)
 is-top t = β±― x κž‰ A , (x ≀ t)

 _is-a-lower-bound-of_ : A β†’ A Γ— A β†’ Ξ© π“₯
 l is-a-lower-bound-of (x , y) = (l ≀ x) ∧ (l ≀ y)

 lower-bound : A Γ— A β†’ 𝓀 βŠ” π“₯ Μ‡
 lower-bound (x , y) =
   Ξ£ l κž‰ A , (l is-a-lower-bound-of (x , y)) holds

 _is-glb-of_ : A β†’ A Γ— A β†’ Ξ© (𝓀 βŠ” π“₯)
 l is-glb-of (x , y) = l is-a-lower-bound-of (x , y)
                     ∧ (β±― (lβ€² , _) κž‰ lower-bound (x , y) , (lβ€² ≀ l))

 glb-is-an-upper-bound₁ : {x y z : A} β†’ (z is-glb-of (x , y) β‡’ z ≀ x) holds
 glb-is-an-upper-bound₁ ((p₁ , _) , _) = p₁

 glb-is-an-upper-boundβ‚‚ : {x y z : A} β†’ (z is-glb-of (x , y) β‡’ z ≀ y) holds
 glb-is-an-upper-boundβ‚‚ ((_ , pβ‚‚) , _) = pβ‚‚

 glb-is-greatest : {x y z w : A}
                 β†’ (z is-glb-of (x , y)) holds
                 β†’ (w is-a-lower-bound-of (x , y) β‡’ w ≀ z) holds
 glb-is-greatest {_} {_} {_} {w} (_ , q) Ο… = q (w , Ο…)

\end{code}

\section{Joins}

\begin{code}

module Joins {A : 𝓀 Μ‡ } (_≀_ : A β†’ A β†’ Ξ© π“₯) where

 is-least : A β†’ Ξ© (𝓀 βŠ” π“₯)
 is-least x = β±― y κž‰ A , x ≀ y

 _is-an-upper-bound-of_ : A β†’ Fam 𝓦 A β†’ Ξ© (π“₯ βŠ” 𝓦)
 u is-an-upper-bound-of U = β±― i κž‰ index U , (U [ i ]) ≀ u

 _is-an-upper-bound-ofβ‚‚_ : A β†’ A Γ— A β†’ Ξ© π“₯
 u is-an-upper-bound-ofβ‚‚ (v , w) = (v ≀ u) ∧ (w ≀ u)

 upper-bound : Fam 𝓦 A β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 Μ‡
 upper-bound U = Ξ£ u κž‰ A , (u is-an-upper-bound-of U) holds

 upper-boundβ‚‚ : A Γ— A β†’ 𝓀 βŠ” π“₯  Μ‡
 upper-boundβ‚‚ (x , y) = Ξ£ u κž‰ A , (u is-an-upper-bound-ofβ‚‚ (x , y)) holds

 _is-lub-of_ : A β†’ Fam 𝓦 A β†’ Ξ© (𝓀 βŠ” π“₯ βŠ” 𝓦)
 u is-lub-of U = (u is-an-upper-bound-of U)
               ∧ (β±― (uβ€² , _) κž‰ upper-bound U , (u ≀ uβ€²))

 _is-lub-ofβ‚‚_ : A β†’ A Γ— A β†’ Ξ© (𝓀 βŠ” π“₯)
 u is-lub-ofβ‚‚ (v , w) = (u is-an-upper-bound-ofβ‚‚ (v , w))
                      ∧ (β±― (uβ€² , _) κž‰ upper-boundβ‚‚ (v , w) , (u ≀ uβ€²))

 lubβ‚‚-is-an-upper-bound₁ : {x y z : A} β†’ (z is-lub-ofβ‚‚ (x , y) β‡’ x ≀ z) holds
 lubβ‚‚-is-an-upper-bound₁ ((p₁ , _) , _) = p₁

 lubβ‚‚-is-an-upper-boundβ‚‚ : {x y z : A} β†’ (z is-lub-ofβ‚‚ (x , y) β‡’ y ≀ z) holds
 lubβ‚‚-is-an-upper-boundβ‚‚ ((_ , pβ‚‚) , _) = pβ‚‚

 lubβ‚‚-is-least : {x y z w : A}
               β†’ (z is-lub-ofβ‚‚ (x , y)) holds
               β†’ (w is-an-upper-bound-ofβ‚‚ (x , y) β‡’ z ≀ w) holds
 lubβ‚‚-is-least {_} {_} {_} {w} (_ , q) Ο… = q (w , Ο…)

module JoinNotation {A : 𝓀 Μ‡ } (⋁_ : Fam 𝓦 A β†’ A) where

 join-syntax : (I : 𝓦 Μ‡ )β†’ (I β†’ A) β†’ A
 join-syntax I f = ⋁ (I , f)

 β‹βŸ¨βŸ©-syntax : {I : 𝓦 Μ‡ } β†’ (I β†’ A) β†’ A
 β‹βŸ¨βŸ©-syntax {I = I} f = join-syntax I f

 infix 2 join-syntax
 infix 2 β‹βŸ¨βŸ©-syntax

 syntax join-syntax I (Ξ» i β†’ e) = β‹βŸ¨ i ∢ I ⟩ e
 syntax β‹βŸ¨βŸ©-syntax    (Ξ» i β†’ e) = β‹βŸ¨ i ⟩ e

\end{code}

\section{Definition of frame}

A (𝓀, π“₯, 𝓦)-frame is a frame whose

  - carrier lives in universe 𝓀,
  - order lives in universe π“₯, and
  - index types live in universe 𝓦.

\begin{code}

frame-data : (π“₯ 𝓦 : Universe) β†’ 𝓀 Μ‡ β†’ 𝓀 βŠ” π“₯ ⁺ βŠ” 𝓦 ⁺ Μ‡
frame-data π“₯ 𝓦 A = (A β†’ A β†’ Ξ© π“₯)   -- order
                 Γ— A               -- top element
                 Γ— (A β†’ A β†’ A)     -- binary meets
                 Γ— (Fam 𝓦 A β†’ A)   -- arbitrary joins

satisfies-frame-laws : {A : 𝓀 Μ‡ } β†’ frame-data π“₯ 𝓦 A β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 ⁺ Μ‡
satisfies-frame-laws {𝓀 = 𝓀} {π“₯} {𝓦} {A = A}  (_≀_ , 𝟏 , _βŠ“_ , βŠ”_) =
 Ξ£ p κž‰ is-partial-order A _≀_ , rest p holds
 where
  open Meets _≀_
  open Joins _≀_
  open JoinNotation βŠ”_

  rest : is-partial-order A _≀_ β†’ Ξ© (𝓀 βŠ” π“₯ βŠ” 𝓦 ⁺)
  rest p = β ∧ γ ∧ δ ∧ Ρ
   where
    P : Poset 𝓀 π“₯
    P = A , _≀_ , p

    iss : is-set A
    iss = carrier-of-[ P ]-is-set

    β = is-top 𝟏
    Ξ³ = β±― (x , y) κž‰ (A Γ— A) , ((x βŠ“ y) is-glb-of (x , y))
    Ξ΄ = β±― U κž‰ Fam 𝓦 A , (βŠ” U) is-lub-of U
    Ξ΅ = β±― (x , U) κž‰ A Γ— Fam 𝓦 A ,
        (x βŠ“ (β‹βŸ¨ i ⟩ U [ i ]) ＝[ iss ]＝ β‹βŸ¨ i ⟩ x βŠ“ (U [ i ]))

\end{code}

The proof `satisfying-frame-laws-is-prop` has been added on 2024-04-15.

\begin{code}

satisfying-frame-laws-is-prop : {A : 𝓀  Μ‡} (d : frame-data π“₯ 𝓦 A)
                              β†’ is-prop (satisfies-frame-laws d)
satisfying-frame-laws-is-prop {𝓀} {π“₯} {𝓦} {A} d@(_≀_ , 𝟏 , _βŠ“_ , βŠ”_) =
 Ξ£-is-prop (being-partial-order-is-prop A _≀_) †
  where
   open Meets _≀_
   open Joins _≀_
   open JoinNotation βŠ”_

   β = is-top 𝟏
   Ξ³ = β±― (x , y) κž‰ (A Γ— A) , ((x βŠ“ y) is-glb-of (x , y))
   Ξ΄ = β±― U κž‰ Fam 𝓦 A , (βŠ” U) is-lub-of U

   Ξ΅ : is-set A β†’ Ξ© (𝓀 βŠ” 𝓦 ⁺)
   Ξ΅ Οƒ = β±― (x , U) κž‰ A Γ— Fam 𝓦 A ,
          (x βŠ“ (β‹βŸ¨ i ⟩ U [ i ]) ＝[ Οƒ ]＝ β‹βŸ¨ i ⟩ x βŠ“ (U [ i ]))

   ‑ : (p : is-partial-order A _≀_) (Οƒ : is-set A)
     β†’ is-prop ((Ξ² ∧ Ξ³ ∧ Ξ΄ ∧ Ξ΅ Οƒ) holds)
   ‑ p Οƒ = holds-is-prop (Ξ² ∧ Ξ³ ∧ Ξ΄ ∧ Ξ΅ Οƒ)

   Ο‡ : is-partial-order A _≀_ β†’ is-set A
   Ο‡ p = carrier-of-[ (A , _≀_ , p) ]-is-set

   † : (p : is-partial-order A _≀_) β†’ is-prop ((Ξ² ∧ Ξ³ ∧ Ξ΄ ∧ Ξ΅ (Ο‡ p)) holds)
   † p = ‑ p (Ο‡ p)

frame-structure : (π“₯ 𝓦 : Universe) β†’ 𝓀 Μ‡ β†’ 𝓀 βŠ” π“₯ ⁺ βŠ” 𝓦 ⁺ Μ‡
frame-structure π“₯ 𝓦 A = Ξ£ d κž‰ frame-data π“₯ 𝓦 A , satisfies-frame-laws d

\end{code}

The type of (𝓀, π“₯, 𝓦)-frames is then defined as:

\begin{code}

Frame : (𝓀 π“₯ 𝓦 : Universe) β†’ 𝓀 ⁺ βŠ” π“₯ ⁺ βŠ” 𝓦 ⁺ Μ‡
Frame 𝓀 π“₯ 𝓦 = Ξ£ A κž‰ (𝓀 Μ‡ ), frame-structure π“₯ 𝓦 A

\end{code}

The underlying poset of a frame:

\begin{code}

poset-of : Frame 𝓀 π“₯ 𝓦 β†’ Poset 𝓀 π“₯
poset-of (A , (_≀_ , _ , _ , _) , p , _) = A , _≀_ , p

\end{code}

Some projections.

\begin{code}

⟨_⟩ : Frame 𝓀 π“₯ 𝓦 β†’ 𝓀 Μ‡
⟨ (A , (_≀_ , _ , _ , _) , p , _) ⟩ = A

𝟏[_] : (F : Frame 𝓀 π“₯ 𝓦) β†’  ⟨ F ⟩
𝟏[ (A , (_ , 𝟏 , _ , _) , p , _) ] = 𝟏

is-top : (F : Frame 𝓀 π“₯ 𝓦) β†’ ⟨ F ⟩ β†’ Ξ© (𝓀 βŠ” π“₯)
is-top F t = β±― x κž‰ ⟨ F ⟩ , x ≀[ poset-of F ] t

𝟏-is-top : (F : Frame 𝓀 π“₯ 𝓦) β†’ (is-top F 𝟏[ F ]) holds
𝟏-is-top (A , _ , _ , p , _) = p

𝟏-is-unique : (F : Frame 𝓀 π“₯ 𝓦) β†’ (t : ⟨ F ⟩) β†’ is-top F t holds β†’ t ＝ 𝟏[ F ]
𝟏-is-unique F t t-top = ≀-is-antisymmetric (poset-of F) Ξ² Ξ³
 where
  Ξ² : (t ≀[ poset-of F ] 𝟏[ F ]) holds
  β = 𝟏-is-top F t

  Ξ³ : (𝟏[ F ] ≀[ poset-of F ] t) holds
  γ = t-top 𝟏[ F ]

only-𝟏-is-above-𝟏 : (F : Frame 𝓀 π“₯ 𝓦) (x : ⟨ F ⟩)
                  β†’ (𝟏[ F ] ≀[ poset-of F ] x) holds β†’ x ＝ 𝟏[ F ]
only-𝟏-is-above-𝟏 F x p =
 𝟏-is-unique F x Ξ» y β†’ y β‰€βŸ¨ 𝟏-is-top F y ⟩ 𝟏[ F ] β‰€βŸ¨ p ⟩ x β– 
  where
   open PosetReasoning (poset-of F)

meet-of : (F : Frame 𝓀 π“₯ 𝓦) β†’ ⟨ F ⟩ β†’ ⟨ F ⟩ β†’ ⟨ F ⟩
meet-of (_ , (_ , _ , _∧_ , _) , _ , _) x y = x ∧ y

infixl 4 meet-of

syntax meet-of F x y = x ∧[ F ] y

join-of : (F : Frame 𝓀 π“₯ 𝓦) β†’ Fam 𝓦 ⟨ F ⟩ β†’ ⟨ F ⟩
join-of (_ , (_ , _ , _ , ⋁_) , _ , _) = ⋁_

infix 4 join-of

syntax join-of F U = ⋁[ F ] U

\end{code}

\begin{code}

∧[_]-is-glb : (A : Frame 𝓀 π“₯ 𝓦) (x y : ⟨ A ⟩)
            β†’ let
               open Meets (Ξ» x y β†’ x ≀[ poset-of A ] y)
              in
               ((x ∧[ A ] y) is-glb-of (x , y)) holds
∧[_]-is-glb (A , _ , _ , (_ , γ , _ , _)) x y = γ (x , y)

∧[_]-is-glb⋆ : (A : Frame 𝓀 π“₯ 𝓦) {x y z : ⟨ A ⟩}
             β†’ let
                open Meets (Ξ» x y β†’ x ≀[ poset-of A ] y)
               in
                z ＝ x ∧[ A ] y β†’ (z is-glb-of (x , y)) holds
∧[_]-is-glb⋆ L@(A , _ , _ , (_ , Ξ³ , _ , _)) {x} {y} {z} p =
 transport (Ξ» - β†’ (- is-glb-of (x , y)) holds) (p ⁻¹) (∧[ L ]-is-glb x y)
  where
   open Meets (Ξ» x y β†’ x ≀[ poset-of L ] y)

∧[_]-lower₁ : (A : Frame 𝓀 π“₯ 𝓦) (x y : ⟨ A ⟩)
            β†’ ((x ∧[ A ] y) ≀[ poset-of A ] x) holds
∧[_]-lower₁ (A , _ , _ , (_ , Ξ³ , _ , _)) x y = pr₁ (pr₁ (Ξ³ (x , y)))

∧[_]-lowerβ‚‚ : (A : Frame 𝓀 π“₯ 𝓦) (x y : ⟨ A ⟩)
            β†’ ((x ∧[ A ] y) ≀[ poset-of A ] y) holds
∧[_]-lowerβ‚‚ (A , _ , _ , (_ , Ξ³ , _ , _)) x y = prβ‚‚ (pr₁ (Ξ³ (x , y)))

∧[_]-greatest : (A : Frame 𝓀 π“₯ 𝓦) (x y : ⟨ A ⟩)
              β†’ (z : ⟨ A ⟩)
              β†’ (z ≀[ poset-of A ] x) holds
              β†’ (z ≀[ poset-of A ] y) holds
              β†’ (z ≀[ poset-of A ] (x ∧[ A ] y)) holds
∧[_]-greatest (A , _ , _ , (_ , γ , _ , _)) x y z p q =
  prβ‚‚ (Ξ³ (x , y)) (z , p , q)

\end{code}

\begin{code}

𝟏-right-unit-of-∧ : (F : Frame 𝓀 π“₯ 𝓦)
                  β†’ (x : ⟨ F ⟩) β†’ x ∧[ F ] 𝟏[ F ] ＝ x
𝟏-right-unit-of-∧ F x = ≀-is-antisymmetric (poset-of F) Ξ² Ξ³
 where
  Ξ² : ((x ∧[ F ] 𝟏[ F ]) ≀[ poset-of F ] x) holds
  Ξ² = ∧[ F ]-lower₁ x 𝟏[ F ]

  Ξ³ : (x ≀[ poset-of F ] (x ∧[ F ] 𝟏[ F ])) holds
  Ξ³ = ∧[ F ]-greatest x 𝟏[ F ] x (≀-is-reflexive (poset-of F) x) (𝟏-is-top F x)

\end{code}

\begin{code}

⋁[_]-upper : (A : Frame 𝓀 π“₯ 𝓦) (U : Fam 𝓦 ⟨ A ⟩) (i : index U)
        β†’ ((U [ i ]) ≀[ poset-of A ] (⋁[ A ] U)) holds
⋁[_]-upper (A , _ , _ , (_ , _ , c , _)) U i = pr₁ (c U) i

⋁[_]-least : (A : Frame 𝓀 π“₯ 𝓦) β†’ (U : Fam 𝓦 ⟨ A ⟩)
           β†’ let open Joins (Ξ» x y β†’ x ≀[ poset-of A ] y)
             in ((u , _) : upper-bound U) β†’ ((⋁[ A ] U) ≀[ poset-of A ] u) holds
⋁[_]-least (A , _ , _ , (_ , _ , c , _)) U = prβ‚‚ (c U)

\end{code}

\begin{code}

𝟚 : (𝓀 : Universe) β†’ 𝓀 Μ‡
𝟚 𝓀 = πŸ™ {𝓀} + πŸ™ {𝓀}

pattern β‚€ = inl ⋆
pattern ₁ = inr ⋆

andβ‚‚ : {𝓀 : Universe} β†’ 𝟚 𝓀 β†’ 𝟚 𝓀 β†’ 𝟚 𝓀
andβ‚‚ (inl ⋆) _ = inl ⋆
andβ‚‚ (inr ⋆) y = y

binary-family : {A : 𝓀 Μ‡ } β†’ (𝓦 : Universe) β†’ A β†’ A β†’ Fam 𝓦 A
binary-family {A = A} 𝓦 x y = 𝟚 𝓦  , Ξ±
 where
  Ξ± : 𝟚 𝓦 β†’ A
  Ξ± (inl *) = x
  Ξ± (inr *) = y

binary-family-syntax : {A : 𝓀 Μ‡ } {𝓦 : Universe} β†’ A β†’ A β†’ Fam 𝓦 A
binary-family-syntax {𝓦 = 𝓦} x y = binary-family 𝓦 x y

syntax binary-family-syntax x y = ⁅ x , y ⁆

fmap-binary-family : {A : 𝓀 Μ‡ } {B : π“₯ Μ‡ }
                   β†’ (𝓦 : Universe)
                   β†’ (f : A β†’ B)
                   β†’ (x y : A)
                   β†’ ⁅ f z ∣ z Ξ΅ (binary-family 𝓦 x y) ⁆
                   ＝ binary-family 𝓦 (f x) (f y)
fmap-binary-family 𝓦 f x y = ap (Ξ» - β†’ 𝟚 𝓦 , -) (dfunext fe Ξ³)
 where
  Ξ³ : ⁅ f z ∣ z Ξ΅ binary-family 𝓦 x y ⁆ [_] ∼ binary-family 𝓦 (f x) (f y) [_]
  Ξ³ (inl *) = refl
  Ξ³ (inr *) = refl


binary-join : (F : Frame 𝓀 π“₯ 𝓦) β†’ ⟨ F ⟩ β†’ ⟨ F ⟩ β†’ ⟨ F ⟩
binary-join {𝓦 = 𝓦} F x y = ⋁[ F ] binary-family 𝓦 x y

infix 3 binary-join
syntax binary-join F x y = x ∨[ F ] y

∨[_]-least : (F : Frame 𝓀 π“₯ 𝓦)
           β†’ let open Joins (Ξ» x y β†’ x ≀[ poset-of F ] y) in
             {x y z : ⟨ F ⟩}
           β†’ (x ≀[ poset-of F ] z) holds
           β†’ (y ≀[ poset-of F ] z) holds
           β†’ ((x ∨[ F ] y) ≀[ poset-of F ] z) holds
∨[_]-least {𝓦 = 𝓦} F {x} {y} {z} x≀z y≀z =
 ⋁[ F ]-least (binary-family 𝓦 x y) (z , Ξ³)
  where
   Ξ³ : _
   Ξ³ (inl *) = x≀z
   Ξ³ (inr *) = y≀z

∨[_]-upper₁ : (F : Frame 𝓀 π“₯ 𝓦)
            β†’ let open Joins (Ξ» x y β†’ x ≀[ poset-of F ] y) in
              (x y : ⟨ F ⟩) β†’ (x ≀[ poset-of F ] (x ∨[ F ] y)) holds
∨[_]-upper₁ {𝓦 = 𝓦} F x y = ⋁[ F ]-upper (binary-family 𝓦 x y) (inl ⋆)

∨[_]-upperβ‚‚ : (F : Frame 𝓀 π“₯ 𝓦)
            β†’ let open Joins (Ξ» x y β†’ x ≀[ poset-of F ] y) in
              (x y : ⟨ F ⟩) β†’ (y ≀[ poset-of F ] (x ∨[ F ] y)) holds
∨[_]-upperβ‚‚ {𝓦 = 𝓦} F x y = ⋁[ F ]-upper (binary-family 𝓦 x y) (inr ⋆)

∨[_]-is-commutative : (F : Frame 𝓀 π“₯ 𝓦)
                    β†’ (x y : ⟨ F ⟩)
                    β†’ (x ∨[ F ] y) ＝ (y ∨[ F ] x)
∨[_]-is-commutative F x y =
 ≀-is-antisymmetric (poset-of F) Ξ² Ξ³
  where
   open PosetNotation  (poset-of F)
   open PosetReasoning (poset-of F)

   Ξ² : ((x ∨[ F ] y) ≀ (y ∨[ F ] x)) holds
   Ξ² = ∨[ F ]-least (∨[ F ]-upperβ‚‚ y x) (∨[ F ]-upper₁ y x)

   Ξ³ : ((y ∨[ F ] x) ≀ (x ∨[ F ] y)) holds
   Ξ³ = ∨[ F ]-least (∨[ F ]-upperβ‚‚ x y) (∨[ F ]-upper₁ x y)

∨[_]-assoc : (F : Frame 𝓀 π“₯ 𝓦)
           β†’ (x y z : ⟨ F ⟩)
           β†’ (x ∨[ F ] y) ∨[ F ] z ＝ x ∨[ F ] (y ∨[ F ] z)
∨[_]-assoc F x y z =
 ≀-is-antisymmetric (poset-of F) (∨[ F ]-least Ξ² Ξ³) (∨[ F ]-least Ξ΄ Ξ΅)
 where
  open PosetNotation  (poset-of F)
  open PosetReasoning (poset-of F)

  Ξ· : (y ≀ ((x ∨[ F ] y) ∨[ F ] z)) holds
  Ξ· = y                     β‰€βŸ¨ ∨[ F ]-upperβ‚‚ x y            ⟩
      x ∨[ F ] y            β‰€βŸ¨ ∨[ F ]-upper₁ (x ∨[ F ] y) z ⟩
      (x ∨[ F ] y) ∨[ F ] z β– 

  ΞΈ : (y ≀ (x ∨[ F ] (y ∨[ F ] z))) holds
  ΞΈ = y                     β‰€βŸ¨ ∨[ F ]-upper₁ y z            ⟩
      y ∨[ F ] z            β‰€βŸ¨ ∨[ F ]-upperβ‚‚ x (y ∨[ F ] z) ⟩
      x ∨[ F ] (y ∨[ F ] z) β– 

  Ξ΄ : (x ≀ ((x ∨[ F ] y) ∨[ F ] z)) holds
  Ξ΄ = x                     β‰€βŸ¨ ∨[ F ]-upper₁ x y            ⟩
      x ∨[ F ] y            β‰€βŸ¨ ∨[ F ]-upper₁ (x ∨[ F ] y) z ⟩
      (x ∨[ F ] y) ∨[ F ] z β– 

  Ξ΅ : ((y ∨[ F ] z) ≀ ((x ∨[ F ] y) ∨[ F ] z)) holds
  Ξ΅ = ∨[ F ]-least Ξ· (∨[ F ]-upperβ‚‚ (x ∨[ F ] y) z)

  Ξ² : ((x ∨[ F ] y) ≀ (x ∨[ F ] (y ∨[ F ] z))) holds
  Ξ² = ∨[ F ]-least (∨[ F ]-upper₁ x (y ∨[ F ] z)) ΞΈ

  Ξ³ : (z ≀ (x ∨[ F ] (y ∨[ F ] z))) holds
  Ξ³ = z                      β‰€βŸ¨ ∨[ F ]-upperβ‚‚ y z            ⟩
      y ∨[ F ] z             β‰€βŸ¨ ∨[ F ]-upperβ‚‚ x (y ∨[ F ] z) ⟩
      x ∨[ F ] (y ∨[ F ] z)  β– 

\end{code}

By fixing the left or right argument of `_∨_` to anything, we get a monotonic
map.

\begin{code}

∨[_]-left-monotone : (F : Frame 𝓀 π“₯ 𝓦)
               β†’ {x y z : ⟨ F ⟩}
               β†’ (x ≀[ poset-of F ] y) holds
               β†’ ((x ∨[ F ] z) ≀[ poset-of F ] (y ∨[ F ] z)) holds
∨[_]-left-monotone F {x = x} {y} {z} p = ∨[ F ]-least Ξ³ (∨[ F ]-upperβ‚‚ y z)
 where
  open PosetNotation  (poset-of F) using (_≀_)
  open PosetReasoning (poset-of F)

  Ξ³ : (x ≀ (y ∨[ F ] z)) holds
  Ξ³ = x β‰€βŸ¨ p ⟩ y β‰€βŸ¨ ∨[ F ]-upper₁ y z ⟩ y ∨[ F ] z β– 

∨[_]-right-monotone : (F : Frame 𝓀 π“₯ 𝓦)
                β†’ {x y z : ⟨ F ⟩}
                β†’ (x ≀[ poset-of F ] y) holds
                β†’ ((z ∨[ F ] x) ≀[ poset-of F ] (z ∨[ F ] y)) holds
∨[_]-right-monotone F {x} {y} {z} p =
 z ∨[ F ] x  ＝⟨ ∨[ F ]-is-commutative z x βŸ©β‚š
 x ∨[ F ] z  β‰€βŸ¨ ∨[ F ]-left-monotone p    ⟩
 y ∨[ F ] z  ＝⟨ ∨[ F ]-is-commutative y z βŸ©β‚š
 z ∨[ F ] y  β– 
  where
   open PosetReasoning (poset-of F)

\end{code}

\begin{code}

βˆ… : {A : 𝓀  Μ‡ } β†’ (𝓦 : Universe) β†’ Fam 𝓦 A
βˆ… 𝓦 = 𝟘 {𝓦} , Ξ» ()

𝟎[_] : (F : Frame 𝓀 π“₯ 𝓦) β†’ ⟨ F ⟩
𝟎[ F ] = ⋁[ F ] (βˆ… _)

is-bottom : (F : Frame 𝓀 π“₯ 𝓦) β†’ ⟨ F ⟩ β†’ Ξ© (𝓀 βŠ” π“₯)
is-bottom F b = β±― x κž‰ ⟨ F ⟩ , (b ≀[ poset-of F ] x)

𝟎-is-bottom : (F : Frame 𝓀 π“₯ 𝓦)
            β†’ (x : ⟨ F ⟩) β†’ (𝟎[ F ] ≀[ poset-of F ] x) holds
𝟎-is-bottom F x = ⋁[ F ]-least (𝟘 , Ξ» ()) (x , Ξ» ())

only-𝟎-is-below-𝟎 : (F : Frame 𝓀 π“₯ 𝓦) (x : ⟨ F ⟩)
                  β†’ (x ≀[ poset-of F ] 𝟎[ F ]) holds β†’ x ＝ 𝟎[ F ]
only-𝟎-is-below-𝟎 F x p =
 ≀-is-antisymmetric (poset-of F) p (𝟎-is-bottom F x)

𝟎-is-unique : (F : Frame 𝓀 π“₯ 𝓦) (b : ⟨ F ⟩)
            β†’ ((x : ⟨ F ⟩) β†’ (b ≀[ poset-of F ] x) holds) β†’ b ＝ 𝟎[ F ]
𝟎-is-unique F b Ο† = only-𝟎-is-below-𝟎 F b (Ο† 𝟎[ F ])

𝟎-right-unit-of-∨ : (F : Frame 𝓀 π“₯ 𝓦) (x : ⟨ F ⟩) β†’ 𝟎[ F ] ∨[ F ] x ＝ x
𝟎-right-unit-of-∨ {𝓦 = 𝓦} F x = ≀-is-antisymmetric (poset-of F) Ξ² Ξ³
 where
  open PosetNotation (poset-of F)

  Ξ² : ((𝟎[ F ] ∨[ F ] x) ≀ x) holds
  Ξ² = ∨[ F ]-least (𝟎-is-bottom F x) (≀-is-reflexive (poset-of F) x)

  Ξ³ : (x ≀ (𝟎[ F ] ∨[ F ] x)) holds
  Ξ³ = ⋁[ F ]-upper (binary-family 𝓦 𝟎[ F ] x) (inr ⋆)

𝟎-left-unit-of-∨ : (F : Frame 𝓀 π“₯ 𝓦) (x : ⟨ F ⟩) β†’ x ∨[ F ] 𝟎[ F ] ＝ x
𝟎-left-unit-of-∨ {𝓦 = 𝓦} F x =
 x ∨[ F ] 𝟎[ F ]  ＝⟨ ∨[ F ]-is-commutative x 𝟎[ F ] ⟩
 𝟎[ F ] ∨[ F ] x  ＝⟨ 𝟎-right-unit-of-∨ F x          ⟩
 x                ∎
\end{code}

\begin{code}

distributivity : (F : Frame 𝓀 π“₯ 𝓦)
               β†’ (x : ⟨ F ⟩)
               β†’ (U : Fam 𝓦 ⟨ F ⟩)
               β†’ let open JoinNotation (Ξ» - β†’ ⋁[ F ] -) in
                 x ∧[ F ] (β‹βŸ¨ i ⟩ (U [ i ]))
               ＝ β‹βŸ¨ i ⟩ (x ∧[ F ] (U [ i ]))
distributivity (_ , _ , _ , (_ , _ , _ , d)) x U = d (x , U)

\end{code}

\section{Scott-continuity}

\begin{code}

is-directed : (F : Frame 𝓀 π“₯ 𝓦) β†’ Fam 𝓦 ⟨ F ⟩ β†’ Ξ© (π“₯ βŠ” 𝓦)
is-directed F (I , Ξ²) =
   βˆ₯ I βˆ₯Ξ©
 ∧ (β±― i κž‰ I , β±― j κž‰ I , (Ǝ k κž‰ I , ((Ξ² i ≀ Ξ² k) ∧ (Ξ² j ≀ Ξ² k)) holds))
  where open PosetNotation (poset-of F)

directedness-entails-inhabitation : (F : Frame 𝓀 π“₯ 𝓦) (S : Fam 𝓦 ⟨ F ⟩)
                                  β†’ (is-directed F S β‡’ βˆ₯ index S βˆ₯Ξ©) holds
directedness-entails-inhabitation F S = pr₁

is-scott-continuous : (F : Frame 𝓀  π“₯  𝓦)
                    β†’ (G : Frame 𝓀′ π“₯β€² 𝓦)
                    β†’ (f : ⟨ F ⟩ β†’ ⟨ G ⟩)
                    β†’ Ξ© (𝓀 βŠ” π“₯ βŠ” 𝓦 ⁺ βŠ” 𝓀′ βŠ” π“₯β€²)
is-scott-continuous {𝓦 = 𝓦} F G f =
 β±― S κž‰ Fam 𝓦 ⟨ F ⟩ , is-directed F S β‡’ f (⋁[ F ] S) is-lub-of ⁅ f s ∣ s Ξ΅ S ⁆
  where
   open Joins (Ξ» x y β†’ x ≀[ poset-of G ] y) using (_is-lub-of_)

id-is-scott-continuous : (F : Frame 𝓀 π“₯ 𝓦) β†’ is-scott-continuous F F id holds
id-is-scott-continuous F S Ξ΄ = ⋁[ F ]-upper S , ⋁[ F ]-least S
 where
  open Joins (Ξ» x y β†’ x ≀[ poset-of F ] y)

\end{code}

\section{Frame homomorphisms}

\begin{code}

is-monotonic : (P : Poset 𝓀 π“₯) (Q : Poset 𝓀′ π“₯β€²)
             β†’ (pr₁ P β†’ pr₁ Q) β†’ Ξ© (𝓀 βŠ” π“₯ βŠ” π“₯β€²)
is-monotonic P Q f =
 β±― (x , y) κž‰ (pr₁ P Γ— pr₁ P) , ((x ≀[ P ] y) β‡’ f x ≀[ Q ] f y)

_─mβ†’_ : (P : Poset 𝓀 π“₯) (Q : Poset 𝓀′ π“₯β€²) β†’ 𝓀 βŠ” π“₯ βŠ” 𝓀′ βŠ” π“₯β€² Μ‡
P ─mβ†’ Q = Ξ£ f κž‰ (∣ P βˆ£β‚š β†’ ∣ Q βˆ£β‚š) , (is-monotonic P Q f) holds

monotone-image-on-directed-family-is-directed : (F : Frame 𝓀  π“₯  𝓦)
                                              β†’ (G : Frame 𝓀′ π“₯β€² 𝓦)
                                              β†’ (S : Fam 𝓦 ⟨ F ⟩)
                                              β†’ is-directed F S holds
                                              β†’ (f : ⟨ F ⟩ β†’ ⟨ G ⟩)
                                              β†’ is-monotonic (poset-of F) (poset-of G) f holds
                                              β†’ is-directed G ⁅ f s ∣ s Ξ΅ S ⁆ holds
monotone-image-on-directed-family-is-directed F G S (ΞΉ , Ο…) f ΞΌ = ΞΉ , Ξ³
 where
  open PropositionalTruncation pt

  I = index S

  Ξ³ : (β±― i κž‰ I , β±― j κž‰ I ,
        (Ǝ k κž‰ I ,
          ((f (S [ i ]) ≀[ poset-of G ] f (S [ k ]))
         ∧ (f (S [ j ]) ≀[ poset-of G ] f (S [ k ]))) holds)) holds
  Ξ³ i j = βˆ₯βˆ₯-rec βˆ₯βˆ₯-is-prop Ξ² (Ο… i j)
   where
    Ξ² : (Ξ£ k κž‰ I , (((S [ i ]) ≀[ poset-of F ] (S [ k ]))
                  ∧ ((S [ j ]) ≀[ poset-of F ] (S [ k ]))) holds)
      β†’ (βˆƒ k κž‰ I , ((f (S [ i ]) ≀[ poset-of G ] f (S [ k ]))
                  ∧ (f (S [ j ]) ≀[ poset-of G ] f (S [ k ]))) holds)
    β (k , p , q) = ∣ k , μ (S [ i ] , S [ k ]) p , μ (S [ j ] , S [ k ]) q ∣



is-join-preserving : (F : Frame 𝓀 π“₯ 𝓦) (G : Frame 𝓀' π“₯' 𝓦)
                   β†’ (⟨ F ⟩ β†’ ⟨ G ⟩) β†’ Ξ© (𝓀 βŠ” 𝓀' βŠ” 𝓦 ⁺)
is-join-preserving {𝓦 = 𝓦} F G f =
 β±― S κž‰ Fam 𝓦 ⟨ F ⟩ , f (⋁[ F ] S) ＝[ iss ]＝ ⋁[ G ] ⁅ f s ∣ s Ξ΅ S ⁆
  where
   iss = carrier-of-[ poset-of G ]-is-set

join-preserving-implies-scott-continuous : (F : Frame 𝓀 π“₯ 𝓦) (G : Frame 𝓀' π“₯' 𝓦)
                                         β†’ (f : ⟨ F ⟩ β†’ ⟨ G ⟩)
                                         β†’ is-join-preserving F G f holds
                                         β†’ is-scott-continuous F G f holds
join-preserving-implies-scott-continuous F G f Ο† S _ = Ξ³
 where
  open Joins (Ξ» x y β†’ x ≀[ poset-of G ] y)

  Ξ³ : (f (⋁[ F ] S) is-lub-of ⁅ f s ∣ s Ξ΅ S ⁆) holds
  Ξ³ = transport
       (Ξ» - β†’ (- is-lub-of (fmap-syntax (Ξ» s β†’ f s)) S) holds)
       (Ο† S ⁻¹)
       (⋁[ G ]-upper ⁅ f s ∣ s Ξ΅ S ⁆ , ⋁[ G ]-least ⁅ f s ∣ s Ξ΅ S ⁆)

\end{code}

\section{Some properties of frames}

\begin{code}

∧[_]-unique : (F : Frame 𝓀 π“₯ 𝓦) {x y z : ⟨ F ⟩}
            β†’ let open Meets (Ξ» x y β†’ x ≀[ poset-of F ] y) in
              (z is-glb-of (x , y)) holds β†’ z ＝ (x ∧[ F ] y)
∧[ F ]-unique {x} {y} {z} (p , q) = ≀-is-antisymmetric (poset-of F) Ξ² Ξ³
 where
  Ξ² : (z ≀[ poset-of F ] (x ∧[ F ] y)) holds
  Ξ² = ∧[ F ]-greatest x y z (pr₁ p) (prβ‚‚ p)

  Ξ³ : ((x ∧[ F ] y) ≀[ poset-of F ] z) holds
  Ξ³ = q ((x ∧[ F ] y) , ∧[ F ]-lower₁ x y , ∧[ F ]-lowerβ‚‚ x y)

\end{code}

\begin{code}

⋁[_]-unique : (F : Frame 𝓀 π“₯ 𝓦) (U : Fam 𝓦 ⟨ F ⟩) (u : ⟨ F ⟩)
         β†’ let open Joins (Ξ» x y β†’ x ≀[ poset-of F ] y) in
           (u is-lub-of U) holds β†’ u ＝ ⋁[ F ] U
⋁[_]-unique F U u (p , q) = ≀-is-antisymmetric (poset-of F) Ξ³ Ξ²
 where
  open PosetNotation (poset-of F)

  Ξ³ : (u ≀ (⋁[ F ] U)) holds
  Ξ³ = q ((⋁[ F ] U) , ⋁[ F ]-upper U)

  Ξ² : ((⋁[ F ] U) ≀ u) holds
  Ξ² = ⋁[ F ]-least U (u , p)

connecting-lemma₁ : (F : Frame 𝓀 π“₯ 𝓦) {x y : ⟨ F ⟩}
                  β†’ (x ≀[ poset-of F ] y) holds
                  β†’ x ＝ x ∧[ F ] y
connecting-lemma₁ F {x} {y} p = ∧[ F ]-unique (Ξ² , Ξ³)
 where
  open Meets (Ξ» x y β†’ x ≀[ poset-of F ] y)

  Ξ² : (x is-a-lower-bound-of (x , y)) holds
  Ξ² = ≀-is-reflexive (poset-of F) x , p

  Ξ³ : (β±― (z , _) κž‰ lower-bound (x , y) , z ≀[ poset-of F ] x) holds
  Ξ³ (z , q , _) = q

connecting-lemmaβ‚‚ : (F : Frame 𝓀 π“₯ 𝓦) {x y : ⟨ F ⟩}
                  β†’ x ＝ x ∧[ F ] y
                  β†’ (x ≀[ poset-of F ] y) holds
connecting-lemmaβ‚‚ F {x} {y} p = x ＝⟨ p βŸ©β‚š x ∧[ F ] y β‰€βŸ¨ ∧[ F ]-lowerβ‚‚ x y ⟩ y β– 
 where
  open PosetReasoning (poset-of F)

connecting-lemma₃ : (F : Frame 𝓀 π“₯ 𝓦) {x y : ⟨ F ⟩}
                  β†’ y ＝ x ∨[ F ] y
                  β†’ (x ≀[ poset-of F ] y) holds
connecting-lemma₃ F {x} {y} p =
 x β‰€βŸ¨ ∨[ F ]-upper₁ x y ⟩ x ∨[ F ] y ＝⟨ p ⁻¹ βŸ©β‚š y β– 
  where
   open PosetReasoning (poset-of F)

connecting-lemmaβ‚„ : (F : Frame 𝓀 π“₯ 𝓦) {x y : ⟨ F ⟩}
                  β†’ (x ≀[ poset-of F ] y) holds
                  β†’ y ＝ x ∨[ F ] y
connecting-lemmaβ‚„ F {x} {y} p = ≀-is-antisymmetric (poset-of F) Ξ² Ξ³
 where
  Ξ² : (y ≀[ poset-of F ] (x ∨[ F ] y)) holds
  Ξ² = ∨[ F ]-upperβ‚‚ x y

  Ξ³ : ((x ∨[ F ] y) ≀[ poset-of F ] y) holds
  Ξ³ = ∨[ F ]-least p (≀-is-reflexive (poset-of F) y)

yoneda : (F : Frame 𝓀 π“₯ 𝓦)
       β†’ (x y : ⟨ F ⟩)
       β†’ ((z : ⟨ F ⟩) β†’ ((z ≀[ poset-of F ] x) β‡’ (z ≀[ poset-of F ] y)) holds)
       β†’ (x ≀[ poset-of F ] y) holds
yoneda F x y Ο† = Ο† x (≀-is-reflexive (poset-of F) x)

scott-continuous-implies-monotone : (F : Frame 𝓀 π“₯ 𝓦) (G : Frame 𝓀′ π“₯β€² 𝓦)
                                  β†’ (f : ⟨ F ⟩ β†’ ⟨ G ⟩)
                                  β†’ is-scott-continuous F G f holds
                                  β†’ is-monotonic (poset-of F) (poset-of G) f holds
scott-continuous-implies-monotone {𝓦 = 𝓦} F G f Ο† (x , y) p =
 f x                                       β‰€βŸ¨ i   ⟩
 f x ∨[ G ] f y                            ＝⟨ ii  βŸ©β‚š
 ⋁[ G ] ⁅ f z ∣ z Ξ΅ binary-family 𝓦 x y ⁆  ＝⟨ iii βŸ©β‚š
 f (x ∨[ F ] y)                            ＝⟨ iv  βŸ©β‚š
 f y                                       β– 
  where
   open PosetReasoning (poset-of G)
   open PropositionalTruncation pt

   Ξ΄ : is-directed F (binary-family 𝓦 x y) holds
   Ξ΄ = ∣ inr ⋆ ∣ , †
        where
         rx : (x ≀[ poset-of F ] x) holds
         rx = ≀-is-reflexive (poset-of F) x

         ry : (y ≀[ poset-of F ] y) holds
         ry = ≀-is-reflexive (poset-of F) y

         † : _
         † (inl ⋆) (inl ⋆) = ∣ inl ⋆ , rx , rx ∣
         † (inl ⋆) (inr ⋆) = ∣ inr ⋆ , p  , ry ∣
         † (inr ⋆) (inl ⋆) = ∣ inr ⋆ , ry , p  ∣
         † (inr ⋆) (inr ⋆) = ∣ inr ⋆ , ry , ry ∣

   i   = ∨[ G ]-upper₁ (f x) (f y)
   ii  = ap (Ξ» - β†’ ⋁[ G ] -) (fmap-binary-family 𝓦 f x y ⁻¹)
   iii = (⋁[ G ]-unique
           ⁅ f z ∣ z Ξ΅ binary-family 𝓦 x y ⁆
           (f (⋁[ F ] ⁅ x , y ⁆))
           (Ο† ⁅ x , y ⁆ Ξ΄)) ⁻¹
   iv  = ap f (connecting-lemmaβ‚„ F p) ⁻¹


scott-continuous-join-eq : (F : Frame 𝓀  π“₯  𝓦)
                         β†’ (G : Frame 𝓀′ π“₯β€² 𝓦)
                         β†’ (f : ⟨ F ⟩ β†’ ⟨ G ⟩)
                         β†’ is-scott-continuous F G f holds
                         β†’ (S : Fam 𝓦 ⟨ F ⟩)
                         β†’ is-directed F S holds
                         β†’ f (⋁[ F ] S) ＝ ⋁[ G ] ⁅ f s ∣ s Ξ΅ S ⁆
scott-continuous-join-eq F G f ΞΆ S Ξ΄ =
 ⋁[ G ]-unique ⁅ f s ∣ s Ξ΅ S ⁆ (f (⋁[ F ] S)) (ΞΆ S Ξ΄)

∘-of-scott-cont-is-scott-cont : (F : Frame 𝓀   π“₯   𝓦)
                                (G : Frame 𝓀′  π“₯β€²  𝓦)
                                (H : Frame 𝓀′′ π“₯β€²β€² 𝓦)
                              β†’ (g : ⟨ G ⟩ β†’ ⟨ H ⟩)
                              β†’ (f : ⟨ F ⟩ β†’ ⟨ G ⟩)
                              β†’ is-scott-continuous G H g holds
                              β†’ is-scott-continuous F G f holds
                              β†’ is-scott-continuous F H (g ∘ f) holds
∘-of-scott-cont-is-scott-cont F G H g f ΢g ΢f S δ =
 Ξ² , Ξ³
  where
   open Joins (Ξ» x y β†’ x ≀[ poset-of H ] y)
   open PosetReasoning (poset-of H)

   ΞΌf : is-monotonic (poset-of F) (poset-of G) f holds
   ΞΌf = scott-continuous-implies-monotone F G f ΞΆf

   ΞΌg : is-monotonic (poset-of G) (poset-of H) g holds
   ΞΌg = scott-continuous-implies-monotone G H g ΞΆg

   † : is-directed G ⁅ f s ∣ s Ξ΅  S ⁆ holds
   † = monotone-image-on-directed-family-is-directed F G S Ξ΄ f ΞΌf

   Ξ² : (g (f (⋁[ F ] S)) is-an-upper-bound-of ⁅ g (f s) ∣ s Ξ΅ S ⁆) holds
   Ξ² k = g (f (S [ k ]))              β‰€βŸ¨ i   ⟩
         ⋁[ H ] ⁅ g (f s) ∣ s Ξ΅ S ⁆   β‰€βŸ¨ ii  ⟩
         g (⋁[ G ] ⁅ f s ∣ s Ξ΅ S ⁆)   ＝⟨ iii βŸ©β‚š
         g (f (⋁[ F ] S))             β– 
          where
           i   = ⋁[ H ]-upper ⁅ g (f s) ∣ s Ξ΅ S ⁆ k
           ii  = ⋁[ H ]-least
                  ⁅ g (f s) ∣ s Ξ΅ S ⁆
                  (g (⋁[ G ] ⁅ f s ∣ s Ξ΅ S ⁆) , pr₁ (ΞΆg ⁅ f s ∣ s Ξ΅ S ⁆ †))
           iii = ap g (scott-continuous-join-eq F G f ΢f S δ ⁻¹)

   Ξ³ : (β±― (u , _) κž‰ upper-bound ⁅ g (f s) ∣ s Ξ΅ S ⁆ ,
         (g (f (⋁[ F ] S)) ≀[ poset-of H ] u)) holds
   Ξ³ (u , p) = g (f (⋁[ F ] S))              β‰€βŸ¨ i   ⟩
               g (⋁[ G ] ⁅ f s ∣ s Ξ΅ S ⁆)    ＝⟨ ii  βŸ©β‚š
               ⋁[ H ] ⁅ g (f s) ∣ s Ξ΅ S ⁆    β‰€βŸ¨ iii ⟩
               u                             β– 
                where
                 β€» : (f (⋁[ F ] S) ≀[ poset-of G ] (⋁[ G ] ⁅ f s ∣ s Ξ΅ S ⁆)) holds
                 β€» = prβ‚‚ (ΞΆf S Ξ΄) ((⋁[ G ] ⁅ f s ∣ s Ξ΅ S ⁆)
                                  , ⋁[ G ]-upper (⁅ f s ∣ s Ξ΅ S ⁆))

                 i   = ΞΌg (f (⋁[ F ] S) , ⋁[ G ] ⁅ f s ∣ s Ξ΅ S ⁆) β€»
                 ii  = scott-continuous-join-eq G H g ΞΆg ⁅ f s ∣ s Ξ΅ S ⁆ †
                 iii = ⋁[ H ]-least ⁅ g (f s) ∣ s Ξ΅ S ⁆ (u , p)

\end{code}

\begin{code}

∧[_]-is-commutative : (F : Frame 𝓀 π“₯ 𝓦) (x y : ⟨ F ⟩)
                 β†’ x ∧[ F ] y ＝ y ∧[ F ] x
∧[ F ]-is-commutative x y = ∧[ F ]-unique (β , γ)
 where
  open Meets (Ξ» x y β†’ x ≀[ poset-of F ] y)
  open PosetNotation (poset-of F) using (_≀_)

  β : ((x ∧[ F ] y) is-a-lower-bound-of (y , x)) holds
  Ξ² = (∧[ F ]-lowerβ‚‚ x y) , (∧[ F ]-lower₁ x y)

  Ξ³ : (β±― (l , _) κž‰ lower-bound (y , x) , l ≀ (x ∧[ F ] y)) holds
  γ (l , p , q) = ∧[ F ]-greatest x y l q p

∧[_]-is-associative : (F : Frame 𝓀 π“₯ 𝓦) (x y z : ⟨ F ⟩)
                    β†’ x ∧[ F ] (y ∧[ F ] z) ＝ (x ∧[ F ] y) ∧[ F ] z
∧[ F ]-is-associative x y z = ≀-is-antisymmetric (poset-of F) Ξ² Ξ³
 where
  open PosetReasoning (poset-of F)

  abstract
   Ξ² : ((x ∧[ F ] (y ∧[ F ] z)) ≀[ poset-of F ] ((x ∧[ F ] y) ∧[ F ] z)) holds
   β = ∧[ F ]-greatest (x ∧[ F ] y) z (x ∧[ F ] (y ∧[ F ] z)) δ Ρ
    where
     Ξ΄ : ((x ∧[ F ] (y ∧[ F ] z)) ≀[ poset-of F ] (x ∧[ F ] y)) holds
     Ξ΄ = ∧[ F ]-greatest x y (x ∧[ F ] (y ∧[ F ] z)) δ₁ Ξ΄β‚‚
      where
       δ₁ : ((x ∧[ F ] (y ∧[ F ] z)) ≀[ poset-of F ] x) holds
       δ₁ = ∧[ F ]-lower₁ x (y ∧[ F ] z)

       Ξ΄β‚‚ : ((x ∧[ F ] (y ∧[ F ] z)) ≀[ poset-of F ] y) holds
       Ξ΄β‚‚ = x ∧[ F ] (y ∧[ F ] z) β‰€βŸ¨ ∧[ F ]-lowerβ‚‚ x (y ∧[ F ] z) ⟩
            y ∧[ F ] z            β‰€βŸ¨ ∧[ F ]-lower₁ y z            ⟩
            y                     β– 

     Ξ΅ : ((x ∧[ F ] (y ∧[ F ] z)) ≀[ poset-of F ] z) holds
     Ξ΅ = x ∧[ F ] (y ∧[ F ] z)  β‰€βŸ¨ ∧[ F ]-lowerβ‚‚ x (y ∧[ F ] z) ⟩
         y ∧[ F ] z             β‰€βŸ¨ ∧[ F ]-lowerβ‚‚ y z            ⟩
         z                      β– 

   Ξ³ : (((x ∧[ F ] y) ∧[ F ] z) ≀[ poset-of F ] (x ∧[ F ] (y ∧[ F ] z))) holds
   γ = ∧[ F ]-greatest x (y ∧[ F ] z) ((x ∧[ F ] y) ∧[ F ] z) ΢ η
    where
     ΞΆ : (((x ∧[ F ] y) ∧[ F ] z) ≀[ poset-of F ] x) holds
     ΞΆ = (x ∧[ F ] y) ∧[ F ] z     β‰€βŸ¨ ∧[ F ]-lower₁ (x ∧[ F ] y) z ⟩
         x ∧[ F ] y                β‰€βŸ¨ ∧[ F ]-lower₁ x y            ⟩
         x                         β– 

     Ξ· : (((x ∧[ F ] y) ∧[ F ] z) ≀[ poset-of F ] (y ∧[ F ] z)) holds
     Ξ· = ∧[ F ]-greatest y z ((x ∧[ F ] y) ∧[ F ] z) Ξ·β‚€ η₁
      where
       Ξ·β‚€ : (((x ∧[ F ] y) ∧[ F ] z) ≀[ poset-of F ] y) holds
       Ξ·β‚€ = (x ∧[ F ] y) ∧[ F ] z  β‰€βŸ¨ ∧[ F ]-lower₁ (x ∧[ F ] y) z ⟩
            x ∧[ F ] y             β‰€βŸ¨ ∧[ F ]-lowerβ‚‚ x y            ⟩
            y                      β– 

       η₁ : (((x ∧[ F ] y) ∧[ F ] z) ≀[ poset-of F ] z) holds
       η₁ = ∧[ F ]-lowerβ‚‚ (x ∧[ F ] y) z

\end{code}

\begin{code}

∧[_]-left-monotone : (F : Frame 𝓀 π“₯ 𝓦)
                   β†’ {x y z : ⟨ F ⟩}
                   β†’ (x ≀[ poset-of F ] y) holds
                   β†’ ((x ∧[ F ] z) ≀[ poset-of F ] (y ∧[ F ] z)) holds
∧[ F ]-left-monotone {x} {y} {z} p = ∧[ F ]-greatest y z (x ∧[ F ] z) β γ
 where
  open PosetReasoning (poset-of F)

  Ξ² : ((x ∧[ F ] z) ≀[ poset-of F ] y) holds
  Ξ² = x ∧[ F ] z β‰€βŸ¨ ∧[ F ]-lower₁ x z ⟩ x β‰€βŸ¨ p ⟩ y β– 

  Ξ³ : ((x ∧[ F ] z) ≀[ poset-of F ] z) holds
  Ξ³ = ∧[ F ]-lowerβ‚‚ x z

∧[_]-right-monotone : (F : Frame 𝓀 π“₯ 𝓦)
                    β†’ {x y z : ⟨ F ⟩}
                    β†’ (x ≀[ poset-of F ] y) holds
                    β†’ ((z ∧[ F ] x) ≀[ poset-of F ] (z ∧[ F ] y)) holds
∧[ F ]-right-monotone {x} {y} {z} p =
 z ∧[ F ] x  ＝⟨ ∧[ F ]-is-commutative z x βŸ©β‚š
 x ∧[ F ] z  β‰€βŸ¨ ∧[ F ]-left-monotone p    ⟩
 y ∧[ F ] z  ＝⟨ ∧[ F ]-is-commutative y z βŸ©β‚š
 z ∧[ F ] y  β– 
  where
   open PosetReasoning (poset-of F)

\end{code}

\begin{code}

𝟎-right-annihilator-for-∧ : (F : Frame 𝓀 π“₯ 𝓦) (x : ⟨ F ⟩)
                          β†’ x ∧[ F ] 𝟎[ F ] ＝ 𝟎[ F ]
𝟎-right-annihilator-for-∧ F x =
 only-𝟎-is-below-𝟎 F (x ∧[ F ] 𝟎[ F ]) (∧[ F ]-lowerβ‚‚ x 𝟎[ F ])

𝟎-left-annihilator-for-∧ : (F : Frame 𝓀 π“₯ 𝓦) (x : ⟨ F ⟩)
                         β†’ 𝟎[ F ] ∧[ F ] x ＝ 𝟎[ F ]
𝟎-left-annihilator-for-∧ F x =
 𝟎[ F ] ∧[ F ] x  ＝⟨ ∧[ F ]-is-commutative 𝟎[ F ] x ⟩
 x ∧[ F ] 𝟎[ F ]  ＝⟨ 𝟎-right-annihilator-for-∧ F x  ⟩
 𝟎[ F ]           ∎

𝟏-right-annihilator-for-∨ : (F : Frame 𝓀 π“₯ 𝓦) (x : ⟨ F ⟩)
                          β†’ x ∨[ F ] 𝟏[ F ] ＝ 𝟏[ F ]
𝟏-right-annihilator-for-∨ F x =
 only-𝟏-is-above-𝟏 F (x ∨[ F ] 𝟏[ F ]) (∨[ F ]-upperβ‚‚ x 𝟏[ F ])

𝟏-left-annihilator-for-∨ : (F : Frame 𝓀 π“₯ 𝓦) (x : ⟨ F ⟩)
                         β†’ 𝟏[ F ] ∨[ F ] x ＝ 𝟏[ F ]
𝟏-left-annihilator-for-∨ F x =
 𝟏[ F ] ∨[ F ] x  ＝⟨ ∨[ F ]-is-commutative 𝟏[ F ] x ⟩
 x ∨[ F ] 𝟏[ F ]  ＝⟨ 𝟏-right-annihilator-for-∨ F x  ⟩
 𝟏[ F ]           ∎


𝟏-left-unit-of-∧ : (F : Frame 𝓀 π“₯ 𝓦)
                 β†’ (x : ⟨ F ⟩) β†’ 𝟏[ F ] ∧[ F ] x ＝ x
𝟏-left-unit-of-∧ F x = 𝟏[ F ] ∧[ F ] x   ＝⟨ ∧[ F ]-is-commutative 𝟏[ F ] x ⟩
                       x ∧[ F ] 𝟏[ F ]   ＝⟨ 𝟏-right-unit-of-∧ F x          ⟩
                       x                 ∎

\end{code}

\begin{code}

distributivityβ€² : (F : Frame 𝓀 π“₯ 𝓦)
                β†’ (x : ⟨ F ⟩)
                β†’ (S : Fam 𝓦 ⟨ F ⟩)
                β†’ let open JoinNotation (Ξ» - β†’ ⋁[ F ] -) in
                  x ∧[ F ] (β‹βŸ¨ i ⟩ (S [ i ]))
                ＝ β‹βŸ¨ i ⟩ ((S [ i ]) ∧[ F ] x)
distributivityβ€² F x S =
 x ∧[ F ] (β‹βŸ¨ i ⟩ S [ i ])    ＝⟨ distributivity F x S ⟩
 β‹βŸ¨ i ⟩ (x ∧[ F ] (S [ i ]))  ＝⟨ †                    ⟩
 β‹βŸ¨ i ⟩ (S [ i ]) ∧[ F ] x    ∎
  where
   open PosetReasoning (poset-of F)
   open JoinNotation (Ξ» - β†’ ⋁[ F ] -)

   ‑ = ∧[ F ]-is-commutative x ∘ (_[_] S)
   † = ap (Ξ» - β†’ join-of F (index S , -)) (dfunext fe ‑)

distributivityβ€²-right : (F : Frame 𝓀 π“₯ 𝓦)
                      β†’ (x : ⟨ F ⟩)
                      β†’ (S : Fam 𝓦 ⟨ F ⟩)
                      β†’ let open JoinNotation (Ξ» - β†’ ⋁[ F ] -) in
                         (β‹βŸ¨ i ⟩ (S [ i ])) ∧[ F ] x ＝ β‹βŸ¨ i ⟩ ((S [ i ]) ∧[ F ] x)
distributivityβ€²-right F x S =
 (β‹βŸ¨ i ⟩ (S [ i ])) ∧[ F ] x  ＝⟨ †                     ⟩
 x ∧[ F ] (β‹βŸ¨ i ⟩ (S [ i ]))  ＝⟨ distributivityβ€² F x S ⟩
 β‹βŸ¨ i ⟩ (S [ i ] ∧[ F ] x)    ∎
  where
   open JoinNotation (Ξ» - β†’ ⋁[ F ] -)

   † = ∧[ F ]-is-commutative (β‹βŸ¨ i ⟩ (S [ i ])) x

absorption-right : (F : Frame 𝓀 π“₯ 𝓦) (x y : ⟨ F ⟩)
                 β†’ x ∨[ F ] (x ∧[ F ] y) ＝ x
absorption-right F x y = ≀-is-antisymmetric (poset-of F) Ξ² Ξ³
 where
  Ξ² : ((x ∨[ F ] (x ∧[ F ] y)) ≀[ poset-of F ] x) holds
  Ξ² = ∨[ F ]-least (≀-is-reflexive (poset-of F) x) (∧[ F ]-lower₁ x y)

  Ξ³ : (x ≀[ poset-of F ] (x ∨[ F ] (x ∧[ F ] y))) holds
  Ξ³ = ∨[ F ]-upper₁ x (x ∧[ F ] y)

absorption-left : (F : Frame 𝓀 π“₯ 𝓦) (x y : ⟨ F ⟩)
                β†’ x ∨[ F ] (y ∧[ F ] x) ＝ x
absorption-left F x y =
 x ∨[ F ] (y ∧[ F ] x) ＝⟨ ap (Ξ» - β†’ x ∨[ F ] -) (∧[ F ]-is-commutative y x) ⟩
 x ∨[ F ] (x ∧[ F ] y) ＝⟨ absorption-right F x y                            ⟩
 x                     ∎

absorptionα΅’α΅–-right : (F : Frame 𝓀 π“₯ 𝓦) β†’ (x y : ⟨ F ⟩) β†’ x ∧[ F ] (x ∨[ F ] y) ＝ x
absorptionα΅’α΅–-right F x y = ≀-is-antisymmetric (poset-of F) Ξ² Ξ³
 where
  Ξ² : ((x ∧[ F ] (x ∨[ F ] y)) ≀[ poset-of F ] x) holds
  Ξ² = ∧[ F ]-lower₁ x (x ∨[ F ] y)

  Ξ³ : (x ≀[ poset-of F ] (x ∧[ F ] (x ∨[ F ] y))) holds
  γ = ∧[ F ]-greatest x (x ∨[ F ] y) x
       (≀-is-reflexive (poset-of F) x)
       (∨[ F ]-upper₁ x y)

absorptionα΅’α΅–-left : (F : Frame 𝓀 π“₯ 𝓦) (x y : ⟨ F ⟩)
                  β†’ x ∧[ F ] (y ∨[ F ] x) ＝ x
absorptionα΅’α΅–-left F x y =
 x ∧[ F ] (y ∨[ F ] x)  ＝⟨ ap (Ξ» - β†’ x ∧[ F ] -) (∨[ F ]-is-commutative y x) ⟩
 x ∧[ F ] (x ∨[ F ] y)  ＝⟨ absorptionα΅’α΅–-right F x y                          ⟩
 x                      ∎

binary-distributivity : (F : Frame 𝓀 π“₯ 𝓦)
                      β†’ (x y z : ⟨ F ⟩)
                      β†’ x ∧[ F ] (y ∨[ F ] z) ＝ (x ∧[ F ] y) ∨[ F ] (x ∧[ F ] z)
binary-distributivity {𝓦 = 𝓦} F x y z =
 x ∧[ F ] (y ∨[ F ] z)                            ＝⟨ † ⟩
 ⋁[ F ] ⁅ x ∧[ F ] w ∣ w Ξ΅ binary-family 𝓦 y z ⁆  ＝⟨ ‑ ⟩
 (x ∧[ F ] y) ∨[ F ] (x ∧[ F ] z)                 ∎
  where
   † = distributivity F x (binary-family 𝓦 y z)
   ‑ = ap (Ξ» - β†’ join-of F -) (fmap-binary-family 𝓦 (Ξ» - β†’ x ∧[ F ] -) y z)

binary-distributivity-right : (F : Frame 𝓀 π“₯ 𝓦)
                            β†’ {x y z : ⟨ F ⟩}
                            β†’ (x ∨[ F ] y) ∧[ F ] z ＝ (x ∧[ F ] z) ∨[ F ] (y ∧[ F ] z)
binary-distributivity-right F {x} {y} {z} =
 (x ∨[ F ] y) ∧[ F ] z             ＝⟨ β…  ⟩
 z ∧[ F ] (x ∨[ F ] y)             ＝⟨ β…‘ ⟩
 (z ∧[ F ] x) ∨[ F ] (z ∧[ F ] y)  ＝⟨ β…’ ⟩
 (x ∧[ F ] z) ∨[ F ] (z ∧[ F ] y)  ＝⟨ β…£ ⟩
 (x ∧[ F ] z) ∨[ F ] (y ∧[ F ] z)  ∎
  where
   β…  = ∧[ F ]-is-commutative (x ∨[ F ] y) z
   β…‘ = binary-distributivity F z x y
   β…’ = ap (Ξ» - β†’ - ∨[ F ] (z ∧[ F ] y)) (∧[ F ]-is-commutative z x)
   β…£ = ap (Ξ» - β†’ (x ∧[ F ] z) ∨[ F ] -) (∧[ F ]-is-commutative z y)

binary-distributivity-op : (F : Frame 𝓀 π“₯ 𝓦) (x y z : ⟨ F ⟩)
                         β†’ x ∨[ F ] (y ∧[ F ] z) ＝ (x ∨[ F ] y) ∧[ F ] (x ∨[ F ] z)
binary-distributivity-op F x y z =
 x ∨[ F ] (y ∧[ F ] z)                                   ＝⟨ †    ⟩
 x ∨[ F ] ((z ∧[ F ] x) ∨[ F ] (z ∧[ F ] y))             ＝⟨ I    ⟩
 x ∨[ F ] (z ∧[ F ] (x ∨[ F ] y))                        ＝⟨ II   ⟩
 x ∨[ F ] ((x ∨[ F ] y) ∧[ F ] z)                        ＝⟨ III  ⟩
 (x ∧[ F ] (x ∨[ F ] y)) ∨[ F ] ((x ∨[ F ] y) ∧[ F ] z)  ＝⟨ IV   ⟩
 ((x ∨[ F ] y) ∧[ F ] x) ∨[ F ] ((x ∨[ F ] y) ∧[ F ] z)  ＝⟨ V    ⟩
 (x ∨[ F ] y) ∧[ F ] (x ∨[ F ] z)                        ∎
  where
   w   = (x ∨[ F ] y) ∧[ F ] z

   I   = ap (Ξ» - β†’ x ∨[ F ] -) ((binary-distributivity F z x y) ⁻¹)
   II  = ap (Ξ» - β†’ x ∨[ F ] -) (∧[ F ]-is-commutative z (x ∨[ F ] y))
   III = ap (Ξ» - β†’ - ∨[ F ] w) (absorptionα΅’α΅–-right F x y) ⁻¹
   IV  = ap (Ξ» - β†’ - ∨[ F ] w) (∧[ F ]-is-commutative x (x ∨[ F ] y))
   V   = (binary-distributivity F (x ∨[ F ] y) x z) ⁻¹

   † : x ∨[ F ] (y ∧[ F ] z) ＝ x ∨[ F ] ((z ∧[ F ] x) ∨[ F ] (z ∧[ F ] y))
   † = x ∨[ F ] (y ∧[ F ] z)                        ＝⟨ i    ⟩
       (x ∨[ F ] (z ∧[ F ] x)) ∨[ F ] (y ∧[ F ] z)  ＝⟨ ii   ⟩
       (x ∨[ F ] (z ∧[ F ] x)) ∨[ F ] (z ∧[ F ] y)  ＝⟨ iii  ⟩
       x ∨[ F ] ((z ∧[ F ] x) ∨[ F ] (z ∧[ F ] y))  ∎
        where
         i   = ap (Ξ» - β†’ - ∨[ F ] (y ∧[ F ] z)) (absorption-left F x z) ⁻¹
         ii  = ap (Ξ» - β†’ (x ∨[ F ] (z ∧[ F ] x)) ∨[ F ] -) (∧[ F ]-is-commutative y z)
         iii = ∨[ F ]-assoc x (z ∧[ F ] x) (z ∧[ F ] y)

\end{code}

\begin{code}

⋁[_]-iterated-join : (F : Frame 𝓀 π“₯ 𝓦) (I : 𝓦 Μ‡ )(J : I β†’ 𝓦 Μ‡)
                β†’ (f : (i : I) β†’ J i β†’ ⟨ F ⟩)
                β†’ ⋁[ F ] ((Ξ£ i κž‰ I , J i) , uncurry f)
                ＝ ⋁[ F ] ⁅ ⋁[ F ] ⁅ f i j ∣ j ∢ J i ⁆ ∣ i ∢ I ⁆
⋁[ F ]-iterated-join I J f = ⋁[ F ]-unique _ _ (Ξ² , Ξ³)
 where
  open Joins (Ξ» x y β†’ x ≀[ poset-of F ] y)
  open PosetReasoning (poset-of F) renaming (_β–  to _QED)

  Ξ² : ((⋁[ F ] (Ξ£ J , uncurry f))
      is-an-upper-bound-of
      ⁅ ⋁[ F ] ⁅ f i j ∣ j ∢ J i ⁆ ∣ i ∢ I ⁆) holds
  Ξ² i = ⋁[ F ]-least _ (_ , Ξ» jα΅’ β†’ ⋁[ F ]-upper _ (i , jα΅’))

  Ξ³ : (β±― (u , _) κž‰ upper-bound ⁅ ⋁[ F ] ⁅ f i j ∣ j ∢ J i ⁆ ∣ i ∢ I ⁆ ,
       (⋁[ F ] (Ξ£ J , uncurry f)) ≀[ poset-of F ] _ ) holds
  Ξ³ (u , p) = ⋁[ F ]-least (Ξ£ J , uncurry f) (_ , Ξ΄)
   where
    Ξ΄ : (u is-an-upper-bound-of (Ξ£ J , uncurry f)) holds
    Ξ΄  (i , j) = f i j                      β‰€βŸ¨ ⋁[ F ]-upper _ j ⟩
                 ⋁[ F ] ⁅ f i j ∣ j ∢ J i ⁆ β‰€βŸ¨ p i              ⟩
                 u                          QED

\end{code}

\begin{code}

∧[_]-is-idempotent : (F : Frame 𝓀 π“₯ 𝓦)
                   β†’ (x : ⟨ F ⟩) β†’ x ＝ x ∧[ F ] x
∧[ F ]-is-idempotent x = ≀-is-antisymmetric (poset-of F) Ξ² Ξ³
 where
  Ξ± : (x ≀[ poset-of F ] x) holds
  Ξ± = ≀-is-reflexive (poset-of F) x

  Ξ² : (x ≀[ poset-of F ] (x ∧[ F ] x)) holds
  β = ∧[ F ]-greatest x x x α α

  Ξ³ : ((x ∧[ F ] x) ≀[ poset-of F ] x) holds
  Ξ³ = ∧[ F ]-lower₁ x x

∨[_]-is-idempotent : (F : Frame 𝓀 π“₯ 𝓦)
                   β†’ (x : ⟨ F ⟩) β†’ x ＝ x ∨[ F ] x
∨[ F ]-is-idempotent x = ≀-is-antisymmetric (poset-of F) † ‑
 where
  † : (x ≀[ poset-of F ] (x ∨[ F ] x)) holds
  † = ∨[ F ]-upper₁ x x

  ‑ : ((x ∨[ F ] x) ≀[ poset-of F ] x) holds
  ‑ = ∨[ F ]-least (≀-is-reflexive (poset-of F) x) (≀-is-reflexive (poset-of F) x)

\end{code}

\begin{code}

distributivity+ : (F : Frame 𝓀 π“₯ 𝓦)
                β†’ let open JoinNotation (Ξ» - β†’ ⋁[ F ] -) in
                  (U@(I , _) V@(J , _) : Fam 𝓦 ⟨ F ⟩)
                β†’ (β‹βŸ¨ i ⟩ (U [ i ])) ∧[ F ] (β‹βŸ¨ j ⟩ (V [ j ]))
                ＝ (β‹βŸ¨ (i , j) ∢ (I Γ— J)  ⟩ ((U [ i ]) ∧[ F ] (V [ j ])))
distributivity+ F U@(I , _) V@(J , _) =
 (β‹βŸ¨ i ⟩ (U [ i ])) ∧[ F ] (β‹βŸ¨ j ⟩ (V [ j ]))     ＝⟨ i   ⟩
 (β‹βŸ¨ j ⟩ (V [ j ])) ∧[ F ] (β‹βŸ¨ i ⟩ (U [ i ]))     ＝⟨ ii  ⟩
 (β‹βŸ¨ i ⟩ (β‹βŸ¨ j ⟩ (V [ j ])) ∧[ F ] (U [ i ]))     ＝⟨ iii ⟩
 (β‹βŸ¨ i ⟩ (U [ i ] ∧[ F ] (β‹βŸ¨ j ⟩ (V [ j ]))))     ＝⟨ iv  ⟩
 (β‹βŸ¨ i ⟩ (β‹βŸ¨ j ⟩ (U [ i ] ∧[ F ] V [ j ])))       ＝⟨ v   ⟩
 (β‹βŸ¨ (i , j) ∢ I Γ— J  ⟩ (U [ i ] ∧[ F ] V [ j ])) ∎
 where
  open JoinNotation (Ξ» - β†’ ⋁[ F ] -)

  i   = ∧[ F ]-is-commutative (β‹βŸ¨ i ⟩ (U [ i ])) (β‹βŸ¨ j ⟩ (V [ j ]))
  ii  = distributivity F (β‹βŸ¨ j ⟩ (V [ j ])) U
  iii = ap
         (Ξ» - β†’ ⋁[ F ] (I , -))
         (dfunext fe Ξ» i β†’ ∧[ F ]-is-commutative (β‹βŸ¨ j ⟩ V [ j ]) (U [ i ]))
  iv  = ap
         (Ξ» - β†’ join-of F (I , -))
         (dfunext fe Ξ» i β†’ distributivity F (U [ i ]) V)
  v   = ⋁[ F ]-iterated-join I (Ξ» _ β†’ J) (Ξ» i j β†’ U [ i ] ∧[ F ] V [ j ]) ⁻¹

\end{code}

\section{Bases of frames}

We first define the notion of a β€œsmall” basis for a frame. Given a
(𝓀, π“₯, 𝓦)-frame, a small basis for it is a 𝓦-family, which has a
further subfamily covering any given element of the frame.

\begin{code}

is-basis-for : (F : Frame 𝓀 π“₯ 𝓦) β†’ Fam 𝓦 ⟨ F ⟩ β†’ (𝓀 βŠ” π“₯ βŠ” 𝓦 ⁺) Μ‡
is-basis-for {𝓦 = 𝓦} F (I , Ξ²) =
 (x : ⟨ F ⟩) β†’ Ξ£ J κž‰ Fam 𝓦 I , (x is-lub-of ⁅ Ξ² j ∣ j Ξ΅ J ⁆) holds
  where
   open Joins (Ξ» x y β†’ x ≀[ poset-of F ] y)

\end{code}

A 𝓦-frame has a (small) basis iff there exists a 𝓦-family
that forms a basis for it. Having a basis should be a property and
not a structure so this is important.

\begin{code}

has-basis : (F : Frame 𝓀 π“₯ 𝓦) β†’ Ξ© (𝓀 βŠ” π“₯ βŠ” 𝓦 ⁺)
has-basis {𝓦 = 𝓦} F = βˆ₯ Ξ£ ℬ κž‰ Fam 𝓦 ⟨ F ⟩ , is-basis-for F ℬ βˆ₯Ξ©

covering-index-family : (F : Frame 𝓀 π“₯ 𝓦) (ℬ : Fam 𝓦 ⟨ F ⟩) (b : is-basis-for F ℬ)
                      β†’ ⟨ F ⟩ β†’ Fam 𝓦 (index ℬ)
covering-index-family F ℬ p x = pr₁ (p x)

covers : (F : Frame 𝓀 π“₯ 𝓦) (ℬ : Fam 𝓦 ⟨ F ⟩) (b : is-basis-for F ℬ)
       β†’ (x : ⟨ F ⟩) β†’ let
                         ℐ = covering-index-family F ℬ b x
                       in
                         x ＝ ⋁[ F ] ⁅ ℬ [ i ] ∣ i Ξ΅ ℐ ⁆
covers F ℬ b x = ⋁[ F ]-unique ⁅ ℬ [ i ] ∣ i Ξ΅ ℐ ⁆ x (prβ‚‚ (b x))
 where
  ℐ = covering-index-family F ℬ b x

\end{code}

We also have the notion of a directed basis, in which every covering
family is directed.

\begin{code}

is-directed-basis : (F : Frame 𝓀 π“₯ 𝓦) (ℬ : Fam 𝓦 ⟨ F ⟩)
                  β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 ⁺ Μ‡
is-directed-basis {𝓦 = 𝓦} F ℬ =
 Ξ£ b κž‰ is-basis-for F ℬ ,
  Ξ  x κž‰ ⟨ F ⟩ , let
                 π’₯ = covering-index-family F ℬ b x
                in
                 is-directed F ⁅ ℬ [ j ] ∣ j Ξ΅ π’₯ ⁆ holds

has-directed-basisβ‚€ : (F : Frame 𝓀 π“₯ 𝓦) β†’ (𝓀 βŠ” π“₯ βŠ” 𝓦 ⁺) Μ‡
has-directed-basisβ‚€ {𝓦 = 𝓦} F =
 Ξ£ ℬ κž‰ Fam 𝓦 ⟨ F ⟩ , is-directed-basis F ℬ

has-directed-basis : (F : Frame 𝓀 π“₯ 𝓦) β†’ Ξ© (𝓀 βŠ” π“₯ βŠ” 𝓦 ⁺)
has-directed-basis {𝓦 = 𝓦} F = βˆ₯ has-directed-basisβ‚€ F βˆ₯Ξ©

directed-cover : (F : Frame 𝓀 π“₯ 𝓦) β†’ has-directed-basisβ‚€ F β†’ ⟨ F ⟩ β†’ Fam 𝓦 ⟨ F ⟩
directed-cover F (ℬ , Ξ²) U = ⁅ ℬ [ i ] ∣ i Ξ΅ pr₁ (pr₁ Ξ² U) ⁆

covers-are-directed : (F : Frame 𝓀 π“₯ 𝓦)
                    β†’ (b : has-directed-basisβ‚€ F)
                    β†’ (U : ⟨ F ⟩)
                    β†’ is-directed F (directed-cover F b U) holds
covers-are-directed F (ℬ , Ξ²) U = prβ‚‚ Ξ² U

\end{code}

The main development in this section is that every small basis can be
extended to a directed one whilst keeping it small.

\begin{code}

join-in-frame : (F : Frame 𝓀 π“₯ 𝓦) (S : Fam 𝓦 ⟨ F ⟩) β†’ List (index S) β†’ ⟨ F ⟩
join-in-frame F S = foldr (Ξ» i - β†’ (S [ i ]) ∨[ F ] -) 𝟎[ F ]

directify : (F : Frame 𝓀 π“₯ 𝓦) β†’ Fam 𝓦 ⟨ F ⟩ β†’ Fam 𝓦 ⟨ F ⟩
directify F (I , Ξ±) = List I , (foldr (Ξ» i - β†’ Ξ± i ∨[ F ] -) 𝟎[ F ])
 where open PosetNotation (poset-of F)

\end{code}

We could have defined `directify` in an alternative way, using the auxiliary
`join-list` function:

\begin{code}

join-list : (F : Frame 𝓀 π“₯ 𝓦) β†’ List ⟨ F ⟩ β†’ ⟨ F ⟩
join-list F = foldr (binary-join F) 𝟎[ F ]

infix 3 join-list

syntax join-list F xs = ⋁ₗ[ F ] xs

join-in-frameβ€² : (F : Frame 𝓀 π“₯ 𝓦) (S : Fam 𝓦 ⟨ F ⟩) β†’ List (index S) β†’ ⟨ F ⟩
join-in-frameβ€² F (I , Ξ±) = join-list F ∘ map Ξ±

directifyβ€² : (F : Frame 𝓀 π“₯ 𝓦) β†’ Fam 𝓦 ⟨ F ⟩ β†’ Fam 𝓦 ⟨ F ⟩
directifyβ€² F (I , Ξ±) = List I , join-in-frameβ€² F (I , Ξ±)

\end{code}

However, the direct definition given in `directify` turns out to be more
convenient for some purposes, so we avoid using `directifyβ€²` as the default
definition. It is a trivial fact that `directify` is the same as `directifyβ€²`.

\begin{code}

join-in-frame-equality : (F : Frame 𝓀 π“₯ 𝓦) (S : Fam 𝓦 ⟨ F ⟩)
                       β†’ join-in-frame F S ∼ join-in-frameβ€² F S
join-in-frame-equality F S []       = refl
join-in-frame-equality F S (i ∷ is) =
 join-in-frame F S (i ∷ is)              ＝⟨ refl ⟩
 (S [ i ]) ∨[ F ] join-in-frame  F S is  ＝⟨ †    ⟩
 (S [ i ]) ∨[ F ] join-in-frameβ€² F S is  ＝⟨ refl ⟩
 join-in-frameβ€² F S (i ∷ is)             ∎
  where
   † = ap (Ξ» - β†’ (S [ i ]) ∨[ F ] -) (join-in-frame-equality F S is)

\end{code}

Note that `directify` is a monoid homomorphism from the free monoid on I
to (_∨_, 𝟎).

\begin{code}

directify-functorial : (F : Frame 𝓀 π“₯ 𝓦) (S : Fam 𝓦 ⟨ F ⟩)
                     β†’ (is js : List (index S))
                     β†’ directify F S [ is ++ js ]
                     ＝ directify F S [ is ] ∨[ F ] directify F S [ js ]
directify-functorial F S@(I , Ξ±) = Ξ³
 where
  Ξ³ : (is js : List I)
    β†’ directify F S [ is ++ js ]
    ＝ directify F S [ is ] ∨[ F ] directify F S [ js ]
  γ []       js = directify F S [ [] ++ js ]          ＝⟨ refl ⟩
                  directify F S [ js ]                ＝⟨ †    ⟩
                  𝟎[ F ]  ∨[ F ] directify F S [ js ] ∎
                   where
                    † = 𝟎-right-unit-of-∨ F (directify F S [ js ]) ⁻¹
  γ (i ∷ is) js =
   directify F S [ (i ∷ is) ++ js ]                              ＝⟨ refl ⟩
   Ξ± i ∨[ F ] directify F S [ is ++ js ]                         ＝⟨ †    ⟩
   Ξ± i ∨[ F ] (directify F S [ is ] ∨[ F ] directify F S [ js ]) ＝⟨ ‑    ⟩
   (α i ∨[ F ] directify F S [ is ]) ∨[ F ] directify F S [ js ] ＝⟨ refl ⟩
   directify F S [ i ∷ is ] ∨[ F ] directify F S [ js ]          ∎
    where
     † = ap (Ξ» - β†’ binary-join F (Ξ± i) -) (Ξ³ is js)
     ‑ = ∨[ F ]-assoc (Ξ± i) (directify F S [ is ]) (directify F S [ js ]) ⁻¹

\end{code}

`directify` does what it is supposed to do: the family it gives is a
directed one.

\begin{code}

directify-is-directed : (F : Frame 𝓀 π“₯ 𝓦) (S : Fam 𝓦 ⟨ F ⟩)
                      β†’ is-directed F (directify F S) holds
directify-is-directed F S@(I , Ξ±) = ∣ [] ∣ , Ο…
 where
  open PropositionalTruncation pt
  open PosetNotation (poset-of F)

  Ο… : (β±― is κž‰ List I
     , β±― js κž‰ List I
     , (Ǝ ks κž‰ List I
      , (((directify F S [ is ] ≀ directify F S [ ks ])
        ∧ (directify F S [ js ] ≀ directify F S [ ks ])) holds))) holds
  Ο… is js = ∣ (is ++ js) , Ξ² , Ξ³ ∣
    where
     open PosetReasoning (poset-of F)

     ‑ = directify-functorial F S is js ⁻¹

     Ξ² : (directify F S [ is ] ≀ directify F S [ is ++ js ]) holds
     Ξ² = directify F S [ is ]                             β‰€βŸ¨ † ⟩
         directify F S [ is ] ∨[ F ] directify F S [ js ] ＝⟨ ‑ βŸ©β‚š
         directify F S [ is ++ js ]                       β– 
          where
           † = ∨[ F ]-upper₁ (directify F S [ is ]) (directify F S [ js ])

     Ξ³ : (directify F S [ js ] ≀ directify F S [ is ++ js ]) holds
     Ξ³ = directify F S [ js ]                             β‰€βŸ¨ † ⟩
         directify F S [ is ] ∨[ F ] directify F S [ js ] ＝⟨ ‑ βŸ©β‚š
         directify F S [ is ++ js ] β– 
          where
           † = ∨[ F ]-upperβ‚‚ (directify F S [ is ]) (directify F S [ js ])

closed-under-binary-joins : (F : Frame 𝓀 π“₯ 𝓦) β†’ Fam 𝓦 ⟨ F ⟩ β†’ Ξ© (𝓀 βŠ” π“₯ βŠ” 𝓦)
closed-under-binary-joins {𝓦 = 𝓦} F S =
 β±― i κž‰ index S , β±― j κž‰ index S ,
  Ǝ k κž‰ index S , ((S [ k ]) is-lub-of (binary-family 𝓦 (S [ i ]) (S [ j ]))) holds
   where
    open Joins (Ξ» x y β†’ x ≀[ poset-of F ] y)

contains-bottom : (F : Frame 𝓀 π“₯ 𝓦) β†’ Fam 𝓦 ⟨ F ⟩ β†’ Ξ© (𝓀 βŠ” π“₯ βŠ” 𝓦)
contains-bottom F U =  Ǝ i κž‰ index U , is-bottom F (U [ i ]) holds

closed-under-finite-joins : (F : Frame 𝓀 π“₯ 𝓦) β†’ Fam 𝓦 ⟨ F ⟩ β†’ Ξ© (𝓀 βŠ” π“₯ βŠ” 𝓦)
closed-under-finite-joins F S =
 contains-bottom F S ∧ closed-under-binary-joins F S

closed-under-fin-joins-implies-directed : (F : Frame 𝓀 π“₯ 𝓦) (S : Fam 𝓦 ⟨ F ⟩)
                                        β†’ (closed-under-finite-joins F S
                                        β‡’ is-directed F S) holds
closed-under-fin-joins-implies-directed F S (iβ‚€ , Γ°) =
 βˆ₯βˆ₯-rec (holds-is-prop (is-directed F S)) Ξ³ iβ‚€
  where
   open PropositionalTruncation pt
   open PosetNotation (poset-of F)
   open Joins (Ξ» x y β†’ x ≀[ poset-of F ] y)

   Ξ³ : (Ξ£ i κž‰ index S , is-bottom F (S [ i ]) holds)
     β†’ is-directed F S holds
   γ (i , _) = ∣ i ∣ , δ
    where
     Ξ΄ : (m n : index S)
       β†’ (Ǝ o κž‰ index S , ((S [ m ] ≀ S [ o ]) ∧ (S [ n ] ≀ S [ o ])) holds) holds
     Ξ΄ m n = βˆ₯βˆ₯-rec βˆƒ-is-prop Ο΅ (Γ° m n)
      where
       Ο΅ : Ξ£ o κž‰ index S , ((S [ o ]) is-lub-of (binary-family 𝓦 (S [ m ]) (S [ n ]))) holds
         β†’ (Ǝ o κž‰ index S , ((S [ m ] ≀ S [ o ]) ∧ (S [ n ] ≀ S [ o ])) holds) holds
       Ο΅ (o , ψ , _) = ∣ o , ψ (inl ⋆) , ψ (inr ⋆) ∣

directify-is-closed-under-fin-joins : (F : Frame 𝓀 π“₯ 𝓦) (S : Fam 𝓦 ⟨ F ⟩)
                                    β†’ closed-under-finite-joins F (directify F S) holds
directify-is-closed-under-fin-joins F S = † , ‑
 where
  open PropositionalTruncation pt

  † : contains-bottom F (directify F S) holds
  † = ∣ [] , 𝟎-is-bottom F ∣

  ‑ : closed-under-binary-joins F (directify F S) holds
  ‑ is js = ∣ (is ++ js) , β™  , ♣ ∣
   where
    open Joins (Ξ» x y β†’ x ≀[ poset-of F ] y)
    open PosetReasoning (poset-of F)

    Ͱ = directify-functorial F S is js ⁻¹

    β™  : ((directify F S [ is ++ js ])
         is-an-upper-bound-of
         ⁅ directify F S [ is ] , directify F S [ js ] ⁆) holds
    β™  (inl p) = directify F S [ is ]                                β‰€βŸ¨ β…  ⟩
                directify F S [ is ] ∨[ F ] directify F S [ js ]    ＝⟨ Ν° βŸ©β‚š
                directify F S [ is ++ js ]                          β– 
                 where
                  β…  = ∨[ F ]-upper₁ (directify F S [ is ]) (directify F S [ js ])
    β™  (inr p) = directify F S [ js ]                              β‰€βŸ¨ β…  ⟩
                directify F S [ is ] ∨[ F ] directify F S [ js ]  ＝⟨ Ν° βŸ©β‚š
                directify F S [ is ++ js ]                        β– 
                 where
                  β…  = ∨[ F ]-upperβ‚‚ (directify F S [ is ]) (directify F S [ js ])

    ♣ : ((u , _) : upper-bound ⁅ directify F S [ is ] , directify F S [ js ] ⁆)
      β†’ ((directify F S [ is ++ js ]) ≀[ poset-of F ] u) holds
    ♣ (u , ΞΆ) =
     directify F S [ is ++ js ]                          ＝⟨ Ν° ⁻¹ βŸ©β‚š
     directify F S [ is ] ∨[ F ] directify F S [ js ]    β‰€βŸ¨ β€» ⟩
     u                                                   β– 
      where
       β€» = ∨[ F ]-least (ΞΆ (inl ⋆) ) (ΞΆ (inr ⋆))

\end{code}

`directify` also preserves the join while doing what it is supposed to
do.

\begin{code}

directify-preserves-joins : (F : Frame 𝓀 π“₯ 𝓦) (S : Fam 𝓦 ⟨ F ⟩)
                          β†’ ⋁[ F ] S ＝ ⋁[ F ] directify F S
directify-preserves-joins F S = ≀-is-antisymmetric (poset-of F) Ξ² Ξ³
 where
  open PosetNotation  (poset-of F)
  open PosetReasoning (poset-of F)

  Ξ² : ((⋁[ F ] S) ≀ (⋁[ F ] directify F S)) holds
  Ξ² = ⋁[ F ]-least S ((⋁[ F ] (directify F S)) , Ξ½)
   where
    Ξ½ : (i : index S) β†’ (S [ i ] ≀ (⋁[ F ] directify F S)) holds
    Ξ½ i =
     S [ i ]                   ＝⟨ 𝟎-right-unit-of-∨ F (S [ i ]) ⁻¹       βŸ©β‚š
     𝟎[ F ] ∨[ F ] S [ i ]     ＝⟨ ∨[ F ]-is-commutative 𝟎[ F ] (S [ i ]) βŸ©β‚š
     S [ i ] ∨[ F ] 𝟎[ F ]     ＝⟨ refl                                   βŸ©β‚š
     directify F S [ i ∷ [] ]  β‰€βŸ¨ ⋁[ F ]-upper (directify F S) (i ∷ [])  ⟩
     ⋁[ F ] directify F S      β– 

  Ξ³ : ((⋁[ F ] directify F S) ≀[ poset-of F ] (⋁[ F ] S)) holds
  Ξ³ = ⋁[ F ]-least (directify F S) ((⋁[ F ] S) , ΞΊ)
   where
    ΞΊ : (is : List (index S)) β†’ ((directify F S [ is ]) ≀ (⋁[ F ] S)) holds
    ΞΊ []       = 𝟎-is-bottom F (⋁[ F ] S)
    ΞΊ (i ∷ is) = S [ i ] ∨[ F ] directify F S [ is ] β‰€βŸ¨ † ⟩
                 ⋁[ F ] S                              β– 
                  where
                   † = ∨[ F ]-least (⋁[ F ]-upper S i) (ΞΊ is)

directify-preserves-joinsβ‚€ : (F : Frame 𝓀 π“₯ 𝓦) (S : Fam 𝓦 ⟨ F ⟩)
                           β†’ let open Joins (Ξ» x y β†’ x ≀[ poset-of F ] y) in
                             (x : ⟨ F ⟩)
                           β†’ (x is-lub-of S β‡’ x is-lub-of directify F S) holds
directify-preserves-joinsβ‚€ F S x p =
 transport (Ξ» - β†’ (- is-lub-of directify F S) holds) (q ⁻¹)
  (⋁[ F ]-upper (directify F S) , ⋁[ F ]-least (directify F S))
 where
  open Joins (Ξ» x y β†’ x ≀[ poset-of F ] y)

  abstract
   q : x ＝ ⋁[ F ] directify F S
   q = x                    ＝⟨ ⋁[ F ]-unique S x p           ⟩
       ⋁[ F ] S             ＝⟨ directify-preserves-joins F S ⟩
       ⋁[ F ] directify F S ∎

\end{code}

\begin{code}

directified-basis-is-basis : (F : Frame 𝓀 π“₯ 𝓦)
                           β†’ (ℬ : Fam 𝓦 ⟨ F ⟩)
                           β†’ is-basis-for F ℬ
                           β†’ is-basis-for F (directify F ℬ)
directified-basis-is-basis {𝓦 = 𝓦} F ℬ Ξ² = β↑
 where
  open PosetNotation (poset-of F)
  open Joins (Ξ» x y β†’ x ≀ y)

  ℬ↑ = directify F ℬ

  π’₯ : ⟨ F ⟩ β†’ Fam 𝓦 (index ℬ)
  π’₯ x = pr₁ (Ξ² x)

  𝒦 : ⟨ F ⟩ β†’ Fam 𝓦 (List (index ℬ))
  𝒦 x = List (index (π’₯ x)) , (Ξ» - β†’ π’₯ x [ - ]) <$>_

  abstract
   Ο† : (x : ⟨ F ⟩)
     β†’ (is : List (index (π’₯ x)))
     β†’ directify F ℬ [ (Ξ» - β†’ π’₯ x [ - ]) <$> is ]
     ＝ directify F ⁅ ℬ [ j ] ∣ j Ξ΅ π’₯ x ⁆ [ is ]
   Ο† x []       = refl
   Ο† x (i ∷ is) = ap (Ξ» - β†’ (_ ∨[ F ] -)) (Ο† x is)

  ψ : (x : ⟨ F ⟩)
    β†’ ⁅ directify F ℬ [ is ] ∣ is Ξ΅ 𝒦 x ⁆ ＝ directify F ⁅ ℬ [ j ] ∣ j Ξ΅ π’₯ x ⁆
  ψ x = to-Ξ£-＝ (refl , dfunext fe (Ο† x))

  β↑ : (x : ⟨ F ⟩)
     β†’ Ξ£ J κž‰ Fam 𝓦 (index ℬ↑) , (x is-lub-of ⁅ ℬ↑ [ j ] ∣ j Ξ΅ J ⁆) holds
  β↑ x = 𝒦 x , transport (Ξ» - β†’ (x is-lub-of -) holds) (ψ x ⁻¹) Ξ΄
    where
    p : (x is-lub-of ⁅ ℬ [ j ] ∣ j Ξ΅ π’₯ x ⁆) holds
    p = prβ‚‚ (Ξ² x)

    Ξ΄ : (x is-lub-of directify F ⁅ ℬ [ j ] ∣ j Ξ΅ π’₯ x ⁆) holds
    Ξ΄ = directify-preserves-joinsβ‚€ F ⁅ ℬ [ j ] ∣ j Ξ΅ π’₯ x ⁆ x p

  δ : (x : ⟨ F ⟩)
    β†’ is-directed F ⁅ directify F ℬ [ is ] ∣ is Ξ΅ 𝒦 x ⁆ holds
  Ξ΄ x = transport (Ξ» - β†’ is-directed F - holds) (ψ x ⁻¹) Ξ΅
    where
    Ξ΅ = directify-is-directed F ⁅ ℬ [ j ] ∣ j Ξ΅ π’₯ x ⁆

covers-of-directified-basis-are-directed : (F : Frame 𝓀 π“₯ 𝓦)
                                         β†’ (ℬ : Fam 𝓦 ⟨ F ⟩)
                                         β†’ (Ξ² : is-basis-for F ℬ)
                                         β†’ (x : ⟨ F ⟩)
                                         β†’ let
                                            ℬ↑ = directify F ℬ
                                            β↑ = directified-basis-is-basis F ℬ Ξ²
                                            π’₯↑ = pr₁ (β↑ x)
                                           in
                                            is-directed F ⁅ ℬ↑ [ i ] ∣ i Ξ΅ π’₯↑ ⁆ holds
covers-of-directified-basis-are-directed {𝓦 = 𝓦} F ℬ Ξ² x =
 transport (Ξ» - β†’ is-directed F - holds) (ψ ⁻¹) Ξ΅
  where
   π’₯ = pr₁ (Ξ² x)

   𝒦 : Fam 𝓦 (List (index ℬ))
   𝒦 = ⁅ (Ξ» - β†’ π’₯ [ - ]) <$> is ∣ is ∢ List (index π’₯) ⁆

   abstract
    Ο† : (is : List (index π’₯))
      β†’ directify F ℬ [ (Ξ» - β†’ π’₯ [ - ]) <$> is ]
      ＝ directify F ⁅ ℬ [ j ] ∣ j Ξ΅ π’₯ ⁆ [ is ]
    Ο† []       = refl
    Ο† (i ∷ is) = ap (Ξ» - β†’ (_ ∨[ F ] -)) (Ο† is)

    ψ : ⁅ directify F ℬ [ is ] ∣ is Ξ΅ 𝒦 ⁆ ＝ directify F ⁅ ℬ [ j ] ∣ j Ξ΅ π’₯ ⁆
    ψ = to-Ξ£-＝ (refl , dfunext fe Ο†)

    Ξ΅ : is-directed F (directify F ⁅ ℬ [ j ] ∣ j Ξ΅ π’₯ ⁆) holds
    Ξ΅ = directify-is-directed F ⁅ ℬ [ j ] ∣ j Ξ΅ π’₯ ⁆

directify-basis : (F : Frame 𝓀 π“₯ 𝓦)
                β†’ (has-basis F β‡’ has-directed-basis F) holds
directify-basis {𝓦 = 𝓦} F = βˆ₯βˆ₯-rec (holds-is-prop (has-directed-basis F)) Ξ³
 where
  open PropositionalTruncation pt
  open PosetNotation (poset-of F)
  open Joins (Ξ» x y β†’ x ≀ y)

  Ξ³ : Ξ£ ℬ κž‰ Fam 𝓦 ⟨ F ⟩ , is-basis-for F ℬ β†’ has-directed-basis F holds
  Ξ³ (ℬ , Ξ²) = ∣ directify F ℬ , (directified-basis-is-basis F ℬ Ξ²) , Ξ΄ ∣
   where
    π’₯ : ⟨ F ⟩ β†’ Fam 𝓦 (index ℬ)
    π’₯ x = pr₁ (Ξ² x)

    𝒦 : ⟨ F ⟩ β†’ Fam 𝓦 (List (index ℬ))
    𝒦 x = List (index (π’₯ x)) , (Ξ» - β†’ π’₯ x [ - ]) <$>_

    Ο† : (x : ⟨ F ⟩)
      β†’ (is : List (index (π’₯ x)))
      β†’ directify F ℬ [ (Ξ» - β†’ π’₯ x [ - ]) <$> is ]
      ＝ directify F ⁅ ℬ [ j ] ∣ j Ξ΅ π’₯ x ⁆ [ is ]
    Ο† x []       = refl
    Ο† x (i ∷ is) = ap (Ξ» - β†’ (_ ∨[ F ] -)) (Ο† x is)

    ψ : (x : ⟨ F ⟩)
      β†’ ⁅ directify F ℬ [ is ] ∣ is Ξ΅ 𝒦 x ⁆ ＝ directify F ⁅ ℬ [ j ] ∣ j Ξ΅ π’₯ x ⁆
    ψ x = to-Ξ£-＝ (refl , dfunext fe (Ο† x))

    δ : (x : ⟨ F ⟩)
      β†’ is-directed F ⁅ directify F ℬ [ is ] ∣ is Ξ΅ 𝒦 x ⁆ holds
    Ξ΄ x = transport (Ξ» - β†’ is-directed F - holds) (ψ x ⁻¹) Ξ΅
     where
      Ξ΅ = directify-is-directed F ⁅ ℬ [ j ] ∣ j Ξ΅ π’₯ x ⁆

\end{code}

\section{Locale notation}

A _locale_ is a type that has a frame of opens.

\begin{code}

record Locale (𝓀 π“₯ 𝓦 : Universe) : 𝓀 ⁺ βŠ” π“₯ ⁺ βŠ” 𝓦 ⁺ Μ‡ where
 field
  ⟨_βŸ©β‚—         : 𝓀 Μ‡
  frame-str-of : frame-structure π“₯ 𝓦 ⟨_βŸ©β‚—

 π’ͺ : Frame 𝓀 π“₯ 𝓦
 π’ͺ = ⟨_βŸ©β‚— , frame-str-of

to-locale-＝ : (X Y : Locale 𝓀 π“₯ 𝓦) β†’ Locale.π’ͺ X ＝ Locale.π’ͺ Y β†’ X ＝ Y
to-locale-＝ X Y refl = refl

\end{code}

\section{Cofinality}

\begin{code}

cofinal-in : (F : Frame 𝓀 π“₯ 𝓦) β†’ Fam 𝓦 ⟨ F ⟩ β†’ Fam 𝓦 ⟨ F ⟩ β†’ Ξ© (π“₯ βŠ” 𝓦)
cofinal-in F R S =
 β±― i κž‰ index R , Ǝ j κž‰ index S , ((R [ i ]) ≀[ poset-of F ] (S [ j ])) holds

cofinal-implies-join-covered : (F : Frame 𝓀 π“₯ 𝓦) (R S : Fam 𝓦 ⟨ F ⟩)
                             β†’ cofinal-in F R S holds
                             β†’ ((⋁[ F ] R) ≀[ poset-of F ] (⋁[ F ] S)) holds
cofinal-implies-join-covered F R S Ο† = ⋁[ F ]-least R ((⋁[ F ] S) , Ξ²)
 where
  open PosetReasoning (poset-of F)
  open PropositionalTruncation pt

  Ξ² : (i : index R) β†’ ((R [ i ]) ≀[ poset-of F ] (⋁[ F ] S)) holds
  Ξ² i = βˆ₯βˆ₯-rec (holds-is-prop ((R [ i ]) ≀[ poset-of F ] (⋁[ F ] S))) Ξ³ (Ο† i)
   where
    Ξ³ : Ξ£ j κž‰ index S , (R [ i ] ≀[ poset-of F ] (S [ j ])) holds
        β†’ (R [ i ] ≀[ poset-of F ] (⋁[ F ] S)) holds
    Ξ³ (j , p) = R [ i ] β‰€βŸ¨ p ⟩ S [ j ] β‰€βŸ¨ ⋁[ F ]-upper S j ⟩ ⋁[ F ] S β– 

bicofinal-implies-same-join : (F : Frame 𝓀 π“₯ 𝓦) (R S : Fam 𝓦 ⟨ F ⟩)
                            β†’ cofinal-in F R S holds
                            β†’ cofinal-in F S R holds
                            β†’ ⋁[ F ] R ＝ ⋁[ F ] S
bicofinal-implies-same-join F R S Ο† ψ =
 ≀-is-antisymmetric
  (poset-of F)
  (cofinal-implies-join-covered F R S Ο†)
  (cofinal-implies-join-covered F S R ψ)

bicofinal-with-directed-family-implies-directed : (F : Frame 𝓀 π“₯ 𝓦)
                                                  (R S : Fam 𝓦 ⟨ F ⟩)
                                                β†’ cofinal-in F R S holds
                                                β†’ cofinal-in F S R holds
                                                β†’ is-directed F R holds
                                                β†’ is-directed F S holds
bicofinal-with-directed-family-implies-directed F R S Ο† ψ (δ₁ , Ξ΄β‚‚) = † , ‑
 where
  open PropositionalTruncation pt
  open PosetNotation (poset-of F)

  † : βˆ₯ index S βˆ₯Ξ© holds
  † = βˆ₯βˆ₯-rec (holds-is-prop βˆ₯ index S βˆ₯Ξ©) †₁ δ₁
   where
    †₁ : index R β†’ βˆ₯ index S βˆ₯Ξ© holds
    †₁ i = βˆ₯βˆ₯-rec (holds-is-prop βˆ₯ index S βˆ₯Ξ©) †₂ (Ο† i)
     where
      †₂ : Ξ£ j κž‰ index S , (R [ i ] ≀ S [ j ]) holds
         β†’ βˆ₯ index S βˆ₯Ξ© holds
      †₂ = ∣_∣ ∘ pr₁

  ‑ : (j₁ jβ‚‚ : index S)
    β†’ (Ǝ j κž‰ index S , (S [ j₁ ] ≀ S [ j ]) holds
                     Γ— (S [ jβ‚‚ ] ≀ S [ j ]) holds) holds
  ‑ j₁ jβ‚‚ = βˆ₯βˆ₯-recβ‚‚ βˆƒ-is-prop ‑₁ (ψ j₁) (ψ jβ‚‚)
   where
    ‑₁ : Ξ£ i₁ κž‰ index R , (S [ j₁ ] ≀ R [ i₁ ]) holds
       β†’ Ξ£ iβ‚‚ κž‰ index R , (S [ jβ‚‚ ] ≀ R [ iβ‚‚ ]) holds
       β†’ (Ǝ j κž‰ index S , (S [ j₁ ] ≀ S [ j ]) holds
                        Γ— (S [ jβ‚‚ ] ≀ S [ j ]) holds) holds
    ‑₁ (i₁ , p₁) (iβ‚‚ , pβ‚‚) = βˆ₯βˆ₯-rec βˆƒ-is-prop ‑₂ (Ξ΄β‚‚ i₁ iβ‚‚)
     where
      ‑₂ : Ξ£ i κž‰ index R , (R [ i₁ ] ≀ R [ i ]) holds
                         Γ— (R [ iβ‚‚ ] ≀ R [ i ]) holds
         β†’ (Ǝ j κž‰ index S , (S [ j₁ ] ≀ S [ j ]) holds
                          Γ— (S [ jβ‚‚ ] ≀ S [ j ]) holds) holds
      ‑₂ (i , q₁ , qβ‚‚) = βˆ₯βˆ₯-rec βˆƒ-is-prop ‑₃ (Ο† i)
       where
        ‑₃ : Ξ£ j κž‰ (index S) , (R [ i ] ≀ S [ j ]) holds
           β†’ (Ǝ j κž‰ index S , (S [ j₁ ] ≀ S [ j ]) holds
                            Γ— (S [ jβ‚‚ ] ≀ S [ j ]) holds) holds
        ‑₃ (j , p) = ∣ j , r₁ , rβ‚‚ ∣
         where
          open PosetReasoning (poset-of F)

          r₁ : (S [ j₁ ] ≀ S [ j ]) holds
          r₁ = S [ j₁ ] β‰€βŸ¨ p₁ ⟩ R [ i₁ ] β‰€βŸ¨ q₁ ⟩ R [ i ] β‰€βŸ¨ p ⟩ S [ j ] β– 

          rβ‚‚ : (S [ jβ‚‚ ] ≀ S [ j ]) holds
          rβ‚‚ = S [ jβ‚‚ ] β‰€βŸ¨ pβ‚‚ ⟩ R [ iβ‚‚ ] β‰€βŸ¨ qβ‚‚ ⟩ R [ i ] β‰€βŸ¨ p ⟩ S [ j ] β– 

open PropositionalTruncation pt

∨[_]-iterated-join : (F : Frame 𝓀 π“₯ 𝓦) (S₁ Sβ‚‚ : Fam 𝓦 ⟨ F ⟩)
                   β†’ βˆ₯ index S₁ βˆ₯
                   β†’ βˆ₯ index Sβ‚‚ βˆ₯
                   β†’ (⋁[ F ] S₁) ∨[ F ] (⋁[ F ] Sβ‚‚)
                   ＝ ⋁[ F ] ⁅ (S₁ [ i ]) ∨[ F ] (Sβ‚‚ [ j ]) ∣ (i , j) ∢ (index S₁ Γ— index Sβ‚‚) ⁆
∨[_]-iterated-join {𝓦 = 𝓦} F S₁ Sβ‚‚ i₁ iβ‚‚ =
 ≀-is-antisymmetric (poset-of F) † ‑
  where
   open PosetReasoning (poset-of F)
   open Joins (Ξ» x y β†’ x ≀[ poset-of F ] y)

   fam-lhs : Fam 𝓦 ⟨ F ⟩
   fam-lhs = binary-family 𝓦 (⋁[ F ] S₁) (⋁[ F ] Sβ‚‚)

   fam-rhs : Fam 𝓦 ⟨ F ⟩
   fam-rhs = ⁅ (S₁ [ i ]) ∨[ F ] (Sβ‚‚ [ j ]) ∣ (i , j) ∢ (index S₁ Γ— index Sβ‚‚) ⁆

   † : ((⋁[ F ] fam-lhs) ≀[ poset-of F ] (⋁[ F ] fam-rhs)) holds
   † = ∨[ F ]-least †₁ †₂
    where
     β™  : ((⋁[ F ] fam-rhs) is-an-upper-bound-of S₁) holds
     β™  i = βˆ₯βˆ₯-rec (holds-is-prop (_ ≀[ poset-of F ] _)) ♣ iβ‚‚
      where
       ♣ : index Sβ‚‚
         β†’ ((S₁ [ i ]) ≀[ poset-of F ] (⋁[ F ] fam-rhs)) holds
       ♣ j =
        S₁ [ i ]                       β‰€βŸ¨ β…  ⟩
        (S₁ [ i ]) ∨[ F ] (Sβ‚‚ [ j ])   β‰€βŸ¨ β…‘ ⟩
        ⋁[ F ] fam-rhs                 β– 
         where
          β…  = ∨[ F ]-upper₁ (S₁ [ i ]) (Sβ‚‚ [ j ])

          β…‘ : (((S₁ [ i ]) ∨[ F ] (Sβ‚‚ [ j ])) ≀[ poset-of F ] (⋁[ F ] fam-rhs)) holds
          β…‘ = ⋁[ F ]-upper fam-rhs (i , j)

     †₁ : ((⋁[ F ] S₁) ≀[ poset-of F ] (⋁[ F ] fam-rhs)) holds
     †₁ = ⋁[ F ]-least S₁ ((⋁[ F ] fam-rhs) , β™ )

     β™₯ : ((⋁[ F ] fam-rhs) is-an-upper-bound-of Sβ‚‚) holds
     β™₯ j = βˆ₯βˆ₯-rec (holds-is-prop (_ ≀[ poset-of F ] _)) β™’ i₁
      where
       β™’ : index S₁ β†’ ((Sβ‚‚ [ j ]) ≀[ poset-of F ] (⋁[ F ] fam-rhs)) holds
       β™’ i =
        Sβ‚‚ [ j ]                        β‰€βŸ¨ β…  ⟩
        (S₁ [ i ]) ∨[ F ] (Sβ‚‚ [ j ])    β‰€βŸ¨ β…‘ ⟩
        ⋁[ F ] fam-rhs                  β– 
         where
          β…  : ((Sβ‚‚ [ j ]) ≀[ poset-of F ] (S₁ [ i ] ∨[ F ] Sβ‚‚ [ j ])) holds
          β…  = ∨[ F ]-upperβ‚‚ (S₁ [ i ]) (Sβ‚‚ [ j ])

          β…‘ : ((S₁ [ i ] ∨[ F ] Sβ‚‚ [ j ]) ≀[ poset-of F ] (⋁[ F ] fam-rhs)) holds
          β…‘ = ⋁[ F ]-upper fam-rhs (i , j)

     †₂ : ((⋁[ F ] Sβ‚‚) ≀[ poset-of F ] (⋁[ F ] fam-rhs)) holds
     †₂ = ⋁[ F ]-least Sβ‚‚ ((⋁[ F ] fam-rhs) , β™₯)

   ‑ : ((⋁[ F ] fam-rhs) ≀[ poset-of F ] (⋁[ F ] fam-lhs)) holds
   ‑ = ⋁[ F ]-least fam-rhs ((⋁[ F ] fam-lhs) , ‑₁)
    where
     ‑₁ : ((⋁[ F ] fam-lhs) is-an-upper-bound-of fam-rhs) holds
     ‑₁ (i , j) =
      (S₁ [ i ])  ∨[ F ] (Sβ‚‚ [ j ])   β‰€βŸ¨ β…     ⟩
      (⋁[ F ] S₁) ∨[ F ] (Sβ‚‚ [ j ])   β‰€βŸ¨ β…‘    ⟩
      (⋁[ F ] S₁) ∨[ F ] (⋁[ F ] Sβ‚‚)  ＝⟨ β…’   βŸ©β‚š
      ⋁[ F ] fam-lhs                  β– 
       where
        β…  = ∨[ F ]-left-monotone  (⋁[ F ]-upper S₁ i)
        β…‘ = ∨[ F ]-right-monotone (⋁[ F ]-upper Sβ‚‚ j)
        β…’ = refl

\end{code}

If a function preserves (1) binary joins and (2) directed joins then it
preserves arbitrary joins.

\begin{code}

sc-and-∨-preserving-β‡’-⋁-preserving : (F : Frame 𝓀 π“₯ 𝓦) (G : Frame 𝓀′ π“₯β€² 𝓦)
                                   β†’ (h : ⟨ F ⟩ β†’ ⟨ G ⟩)
                                   β†’ is-scott-continuous F G h holds
                                   β†’ (h 𝟎[ F ] ＝ 𝟎[ G ])
                                   β†’ (((x y : ⟨ F ⟩) β†’ h (x ∨[ F ] y) ＝ h x ∨[ G ] h y))
                                   β†’ is-join-preserving F G h holds
sc-and-∨-preserving-β‡’-⋁-preserving F G h ΞΆ ψ Ο† S =
 h (⋁[ F ] S)              ＝⟨ ap h p ⟩
 h (⋁[ F ] S↑)             ＝⟨ β™       ⟩
 ⋁[ G ] ⁅ h xβƒ— ∣ xβƒ— Ξ΅ S↑ ⁆   ＝⟨ β™₯      ⟩
 ⋁[ G ] ⁅ h x ∣ x Ξ΅ S ⁆    ∎
  where
   open PropositionalTruncation pt
   open PosetReasoning (poset-of G)

   S↑ = directify F S

   Ξ΄ : is-directed F S↑ holds
   Ξ΄ = directify-is-directed F S

   p : ⋁[ F ] S ＝ ⋁[ F ] S↑
   p = directify-preserves-joins F S

   β™  = ⋁[ G ]-unique ⁅ h x ∣ x Ξ΅ S↑ ⁆ (h (⋁[ F ] S↑)) (ΞΆ S↑ Ξ΄)

   open Joins (Ξ» x y β†’ x ≀[ poset-of G ] y)

   lemma : ((⋁[ G ] ⁅ h x ∣ x Ξ΅ S ⁆) is-an-upper-bound-of ⁅ h xβƒ— ∣ xβƒ— Ξ΅ S↑ ⁆) holds
   lemma [] =
    h 𝟎[ F ]                  ＝⟨ ψ βŸ©β‚š
    𝟎[ G ]                    β‰€βŸ¨ 𝟎-is-bottom G (⋁[ G ] ⁅ h x ∣ x Ξ΅ S ⁆) ⟩
    ⋁[ G ] ⁅ h x ∣ x Ξ΅ S ⁆    β– 
   lemma (i ∷ iβƒ—) =
    h ((S [ i ]) ∨[ F ] directify F S [ iβƒ— ])    ＝⟨ Ο† _ _ βŸ©β‚š
    h (S [ i ]) ∨[ G ] h (directify F S [ iβƒ— ])  β‰€βŸ¨ †     ⟩
    ⋁[ G ] ⁅ h x ∣ x Ξ΅ S ⁆                      β– 
     where
      †₀ : (h (S [ i ]) ≀[ poset-of G ] (⋁[ G ] ⁅ h x ∣ x Ξ΅ S ⁆)) holds
      †₀ = ⋁[ G ]-upper ⁅ h x ∣ x Ξ΅ S ⁆ i

      †₁ : (h (directify F S [ iβƒ— ]) ≀[ poset-of G ] (⋁[ G ] ⁅ h x ∣ x Ξ΅ S ⁆)) holds
      †₁ = lemma iβƒ—

      †  = ∨[ G ]-least †₀ †₁

   β™₯₁ : ((⋁[ G ] ⁅ h xβƒ— ∣ xβƒ— Ξ΅ S↑ ⁆) ≀[ poset-of G ] (⋁[ G ] ⁅ h x ∣ x Ξ΅ S ⁆)) holds
   β™₯₁ = ⋁[ G ]-least ⁅ h xβƒ— ∣ xβƒ— Ξ΅ S↑ ⁆ ((⋁[ G ] ⁅ h x ∣ x Ξ΅ S ⁆) , lemma)

   β™₯β‚‚ : ((⋁[ G ] ⁅ h x ∣ x Ξ΅ S ⁆) ≀[ poset-of G ] (⋁[ G ] ⁅ h xβƒ— ∣ xβƒ— Ξ΅ S↑ ⁆)) holds
   β™₯β‚‚ = ⋁[ G ]-least ⁅ h x ∣ x Ξ΅ S ⁆ ((⋁[ G ] ⁅ h xβƒ— ∣ xβƒ— Ξ΅ S↑ ⁆) , †)
    where
     † : ((⋁[ G ] ⁅ h xβƒ— ∣ xβƒ— Ξ΅ S↑ ⁆) is-an-upper-bound-of ⁅ h x ∣ x Ξ΅ S ⁆) holds
     † i = h (S [ i ])                ＝⟨ ap h (𝟎-left-unit-of-∨ F (S [ i ]) ⁻¹) βŸ©β‚š
           h (S [ i ] ∨[ F ] 𝟎[ F ])  ＝⟨ refl βŸ©β‚š
           h (S↑ [ i ∷ [] ])          β‰€βŸ¨ ‑ ⟩
           ⋁[ G ] ⁅ h xβƒ— ∣ xβƒ— Ξ΅ S↑ ⁆    β– 
            where
             ‑ = ⋁[ G ]-upper ⁅ h xβƒ— ∣ xβƒ— Ξ΅ S↑ ⁆ (i ∷ [])

   β™₯ = ≀-is-antisymmetric (poset-of G) β™₯₁ β™₯β‚‚

join-𝟎-lemma₁ : (F : Frame 𝓀 π“₯ 𝓦)
              β†’ {x y : ⟨ F ⟩}
              β†’ x ∨[ F ] y ＝ 𝟎[ F ]
              β†’ x ＝ 𝟎[ F ]
join-𝟎-lemma₁ F {x} {y} p = only-𝟎-is-below-𝟎 F x †
 where
  open PosetReasoning (poset-of F)

  † : (x ≀[ poset-of F ] 𝟎[ F ]) holds
  † = x β‰€βŸ¨ ∨[ F ]-upper₁ x y ⟩ x ∨[ F ] y ＝⟨ p βŸ©β‚š 𝟎[ F ] β– 

join-𝟎-lemmaβ‚‚ : (F : Frame 𝓀 π“₯ 𝓦)
              β†’ {x y : ⟨ F ⟩}
              β†’ x ∨[ F ] y ＝ 𝟎[ F ]
              β†’ y ＝ 𝟎[ F ]
join-𝟎-lemmaβ‚‚ F {x} {y} p = only-𝟎-is-below-𝟎 F y †
 where
  open PosetReasoning (poset-of F)

  † : (y ≀[ poset-of F ] 𝟎[ F ]) holds
  † = y β‰€βŸ¨ ∨[ F ]-upperβ‚‚ x y ⟩ x ∨[ F ] y ＝⟨ p βŸ©β‚š 𝟎[ F ] β– 

\end{code}

The proofs `order-is-set`, `frame-data-is-set`, and `frame-structure-is-set`
below have been been added on 2024-04-17.

\begin{code}

order-is-set : {π“₯ : Universe} (pe : propext π“₯) (A : 𝓀  Μ‡) β†’ is-set (A β†’ A β†’ Ξ© π“₯)
order-is-set {π“₯} pe A {_≀₁_} {_≀₂_} =
 Ξ -is-set fe Ξ» x β†’ Ξ -is-set fe Ξ» y β†’ Ξ©-is-set fe pe

frame-data-is-set : (A : 𝓀  Μ‡) (Οƒ : is-set A) (π“₯ 𝓦 : Universe) β†’ propext π“₯ β†’ is-set (frame-data π“₯ 𝓦 A)
frame-data-is-set A Οƒ π“₯ 𝓦 pe =
 Ξ£-is-set (order-is-set pe A) Ξ» _≀_ β†’
  Γ—-is-set
   Οƒ
   (Γ—-is-set (Ξ -is-set fe Ξ» _ β†’ Ξ -is-set fe Ξ» _ β†’ Οƒ) (Ξ -is-set fe Ξ» _ β†’ Οƒ))

frame-structure-is-set : {𝓀 : Universe}
                       β†’ (A : 𝓀  Μ‡) (π“₯ 𝓦 : Universe)
                       β†’ propext π“₯
                       β†’ is-set (frame-structure π“₯ 𝓦 A)
frame-structure-is-set A π“₯ 𝓦 pe {(d₁ , p₁)} {(dβ‚‚ , pβ‚‚)} =
 Ξ£-is-set
  (frame-data-is-set A Οƒ π“₯ 𝓦 pe)
  (Ξ» d β†’ props-are-sets (satisfying-frame-laws-is-prop d))
   where
    Οƒ : is-set A
    Οƒ = carrier-of-[ poset-of (A , (d₁ , p₁)) ]-is-set

\end{code}

Added on 2024-08-18.

\begin{code}

open import UF.Equiv using (_≃_; logically-equivalent-props-are-equivalent)
open import UF.Size using (_is_small)

local-smallness-of-frame-gives-local-smallness-of-carrier
 : (F : Frame 𝓀 π“₯ 𝓦)
 β†’ (x y : ⟨ F ⟩)
 β†’ (x ＝ y) is π“₯ small
local-smallness-of-frame-gives-local-smallness-of-carrier F x y =
 (x ≣[ poset-of F ] y) holds , e
  where
   open PosetNotation (poset-of F) using (_≀_)

   s : (x ≣[ poset-of F ] y) holds β†’ x ＝ y
   s = uncurry (≀-is-antisymmetric (poset-of F))

   r : x ＝ y β†’ (x ≣[ poset-of F ] y) holds
   r p = reflexivity+ (poset-of F) p , reflexivity+ (poset-of F) (p ⁻¹)

   e : (x ≣[ poset-of F ] y) holds ≃ (x ＝ y)
   e = logically-equivalent-props-are-equivalent
        (holds-is-prop (x ≣[ poset-of F ] y))
        carrier-of-[ poset-of F ]-is-set
        s
        r

local-smallness-of-carrier-gives-local-smallness-of-frame
 : (F : Frame 𝓀 π“₯ 𝓦)
 β†’ (x y : ⟨ F ⟩)
 β†’ (x ≀[ poset-of F ] y) holds is 𝓀 small
local-smallness-of-carrier-gives-local-smallness-of-frame F x y =
 (x ∧[ F ] y ＝ x) , e
  where
   open PosetNotation (poset-of F) using (_≀_)

   s : x ∧[ F ] y ＝ x β†’ (x ≀ y) holds
   s p = connecting-lemmaβ‚‚ F (p ⁻¹)

   r : (x ≀ y) holds β†’ x ∧[ F ] y ＝ x
   r p = connecting-lemma₁ F p ⁻¹

   e : (x ∧[ F ] y ＝ x) ≃ (x ≀ y) holds
   e = logically-equivalent-props-are-equivalent
        carrier-of-[ poset-of F ]-is-set
        (holds-is-prop (x ≀ y))
        s
        r

\end{code}