Ayberk Tosun, completed 30 November 2022.

The main result needed in this module is the extension lemma.

\begin{code}[hide]

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

open import MLTT.Spartan hiding (𝟚)
open import Slice.Family
open import UF.Base
open import UF.Equiv hiding (_β– )
open import UF.FunExt
open import UF.PropTrunc
open import UF.Sets
open import UF.Sets-Properties
open import UF.SubtypeClassifier

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

open import Locales.CompactRegular pt fe
open import Locales.ContinuousMap.FrameHomomorphism-Definition pt fe
open import Locales.ContinuousMap.FrameHomomorphism-Properties pt fe
open import Locales.Frame pt fe
open import UF.Logic
open import UF.Subsingletons

open FrameHomomorphismProperties
open AllCombinators pt fe
open PropositionalTruncation pt

\end{code}

\section{Definition of a Boolean algebra}

\begin{code}

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

\end{code}

Since the order is derivable from the meets (or the joins), it might be room for
further work to define the order using the meets. However, the universes will
change if we do this so it is not clear what it will result in.

\begin{code}

ba-data : {𝓀 : Universe} β†’ (π“₯ : Universe) β†’ 𝓀  Μ‡ β†’ 𝓀 βŠ” π“₯ ⁺  Μ‡
ba-data π“₯ A = (A β†’ A β†’ Ξ© π“₯ )  -- order
            Γ— A               -- top element
            Γ— (A β†’ A β†’ A)     -- binary meets
            Γ— A               -- bottom element
            Γ— (A β†’ A β†’ A)     -- binary joins
            Γ— (A β†’ A)         -- negation

\end{code}

\begin{code}

module Complementation {A : 𝓀  Μ‡ } (iss : is-set A) (𝟎 𝟏 : A) (_⋏_ _β‹Ž_ : A β†’ A β†’ A) where

 _complements_ : A β†’ A β†’ Ξ© 𝓀
 xβ€² complements x = (x ⋏ xβ€² ＝[ iss ]＝ 𝟎) ∧ (x β‹Ž xβ€² ＝[ iss ]＝ 𝟏)

\end{code}

\begin{code}

satisfies-ba-laws : {A : 𝓀  Μ‡ } β†’ ba-data π“₯ A β†’ 𝓀 βŠ” π“₯  Μ‡
satisfies-ba-laws {𝓀 = 𝓀} {π“₯ = π“₯} {A = A} (_≀_ , 𝟏 , _βŠ“_ , 𝟎 , _β‹Ž_ , Β¬_) =
 Ξ£ p κž‰ is-partial-order A _≀_ , rest p holds
  where
   open Meets (Ξ» x y β†’ x ≀ y)
   open Joins (Ξ» x y β†’ x ≀ y)

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

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

     open Complementation iss 𝟎 𝟏 _βŠ“_ _β‹Ž_

     Ξ² : Ξ© (𝓀 βŠ” π“₯)
     Ξ² = β±― x κž‰ A , β±― y κž‰ A , (x βŠ“ y) is-glb-of (x , y)

     Ξ³ : Ξ© (𝓀 βŠ” π“₯)
     Ξ³ = β±― x κž‰ A , x ≀ 𝟏

     Ξ΄ : Ξ© (𝓀 βŠ” π“₯)
     Ξ΄ = β±― x κž‰ A , β±― y κž‰ A , _is-lub-ofβ‚‚_ (x β‹Ž y) (x , y)

     Ο΅ : Ξ© (𝓀 βŠ” π“₯)
     Ο΅ = β±― x κž‰ A , 𝟎 ≀ x

     ΞΆ : Ξ© (𝓀 βŠ” 𝓀)
     ΞΆ = β±― x κž‰ A , β±― y κž‰ A , β±― z κž‰ A , x βŠ“ (y β‹Ž z) ＝[ iss ]＝ (x βŠ“ y) β‹Ž (x βŠ“ z)

     Ξ· : Ξ© (𝓀 βŠ” 𝓀)
     Ξ· = β±― x κž‰ A , (Β¬ x) complements x

\end{code}

\begin{code}

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

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

\end{code}

\begin{code}

βŸͺ_⟫ : BooleanAlgebra 𝓀 π“₯ β†’ 𝓀  Μ‡
βŸͺ A , _ ⟫ = A

poset-of-ba : BooleanAlgebra 𝓀 π“₯ β†’ Poset 𝓀 π“₯
poset-of-ba (A , ((_≀_ , _) , (Ο† , _))) = A , _≀_ , Ο†

carrier-of-ba-is-set : (B : BooleanAlgebra 𝓀 π“₯) β†’ is-set βŸͺ B ⟫
carrier-of-ba-is-set B = carrier-of-[ poset-of-ba B ]-is-set

meet-of-ba : (B : BooleanAlgebra 𝓀 π“₯) β†’ βŸͺ B ⟫ β†’ βŸͺ B ⟫ β†’ βŸͺ B ⟫
meet-of-ba (_ , (_ , _ , _⋏_ , _) , _) = _⋏_

⋏[_]-is-lower₁ : (B : BooleanAlgebra 𝓀 π“₯)
               β†’ (x y : βŸͺ B ⟫) β†’ ((x ⋏[ B ] y) ≀[ poset-of-ba B ] x) holds
⋏[_]-is-lower₁ B@(_ , _ , (_ , Ο† , _ , _)) x y = pr₁ (pr₁ (Ο† x y))

⋏[_]-is-lowerβ‚‚ : (B : BooleanAlgebra 𝓀 π“₯)
               β†’ (x y : βŸͺ B ⟫) β†’ ((x ⋏[ B ] y) ≀[ poset-of-ba B ] y) holds
⋏[_]-is-lowerβ‚‚ B@(_ , _ , (_ , Ο† , _ , _)) x y = prβ‚‚ (pr₁ (Ο† x y))

⋏[_]-is-greatest : (B : BooleanAlgebra 𝓀 π“₯) {x y l : βŸͺ B ⟫}
                 β†’ (l ≀[ poset-of-ba B ] x) holds
                 β†’ (l ≀[ poset-of-ba B ] y) holds
                 β†’ (l ≀[ poset-of-ba B ] (x ⋏[ B ] y)) holds
⋏[_]-is-greatest B@(_ , _ , (_ , Ο† , _ , _)) {x} {y} {l} p q =
 prβ‚‚ (Ο† x y) (l , p , q)

infixl 4 meet-of-ba

syntax meet-of-ba B x y = x ⋏[ B ] y

join-of-ba : (B : BooleanAlgebra 𝓀 π“₯) β†’ βŸͺ B ⟫ β†’ βŸͺ B ⟫ β†’ βŸͺ B ⟫
join-of-ba (_ , (_ , _ , _ , _ , _β‹Ž_ , _) , _) = _β‹Ž_

infixl 3 join-of-ba

syntax join-of-ba B x y = x β‹Ž[ B ] y

β‹Ž[_]-is-upper₁ : (B : BooleanAlgebra 𝓀 π“₯)
               β†’ (x y : βŸͺ B ⟫) β†’ (x ≀[ poset-of-ba B ] (x β‹Ž[ B ] y)) holds
β‹Ž[_]-is-upper₁ (_ , _ , (_ , _ , _ , Ο† , _)) x y = pr₁ (pr₁ (Ο† x y))

β‹Ž[_]-is-upperβ‚‚ : (B : BooleanAlgebra 𝓀 π“₯)
               β†’ (x y : βŸͺ B ⟫) β†’ (y ≀[ poset-of-ba B ] (x β‹Ž[ B ] y)) holds
β‹Ž[_]-is-upperβ‚‚ (_ , _ , (_ , _ , _ , Ο† , _)) x y = prβ‚‚ (pr₁ (Ο† x y))

β‹Ž[_]-is-least : (B : BooleanAlgebra 𝓀 π“₯)
              β†’ {u x y : βŸͺ B ⟫}
              β†’ (x ≀[ poset-of-ba B ] u) holds
              β†’ (y ≀[ poset-of-ba B ] u) holds
              β†’ ((x β‹Ž[ B ] y) ≀[ poset-of-ba B ] u) holds
β‹Ž[_]-is-least (_ , _ , (_ , _ , _ , Ο† , _)) {u} {x} {y} p q =
 prβ‚‚ (Ο† x y) (u , p , q)

⊀[_] : (B : BooleanAlgebra 𝓀 π“₯) β†’ βŸͺ B ⟫
⊀[ (_ , (_ , ⊀ , _ , _ , _ , _) , _) ] = ⊀

⊀[_]-is-top : (B : BooleanAlgebra 𝓀 π“₯)
            β†’ (b : βŸͺ B ⟫) β†’ (b ≀[ poset-of-ba B ] ⊀[ B ]) holds
⊀[ _ , _ , Ο† ]-is-top = pr₁ (prβ‚‚ (prβ‚‚ Ο†))

βŠ₯[_] : (B : BooleanAlgebra 𝓀 π“₯) β†’ βŸͺ B ⟫
βŠ₯[ (_ , (_ , _ , _ , βŠ₯ , _ , _) , _) ] = βŠ₯

βŠ₯[_]-is-bottom : (B : BooleanAlgebra 𝓀 π“₯)
               β†’ (b : βŸͺ B ⟫) β†’ (βŠ₯[ B ] ≀[ poset-of-ba B ] b) holds
βŠ₯[ _ , _ , Ο† ]-is-bottom = pr₁ (prβ‚‚ (prβ‚‚ (prβ‚‚ (prβ‚‚ Ο†))))

Β¬[_]_ : (B : BooleanAlgebra 𝓀 π“₯) β†’ βŸͺ B ⟫ β†’ βŸͺ B ⟫
Β¬[ B ] x = prβ‚‚ (prβ‚‚ (prβ‚‚ (prβ‚‚ (prβ‚‚ (pr₁ (prβ‚‚ B)))))) x

Β¬[_]-is-complement : (B : BooleanAlgebra 𝓀 π“₯)
                   β†’ let
                      Οƒ = carrier-of-[ poset-of-ba B ]-is-set
                      open Complementation Οƒ βŠ₯[ B ] ⊀[ B ] (meet-of-ba B) (join-of-ba B)
                     in
                      (x : βŸͺ B ⟫) β†’ ((Β¬[ B ] x) complements x) holds
Β¬[_]-is-complement (_ , _ , (_ , _ , _ , _ , _ , _ , Ο†)) = Ο†

⋏-distributes-over-β‹Ž : (B : BooleanAlgebra 𝓀 π“₯)
                     β†’ (x y z : βŸͺ B ⟫)
                     β†’ x ⋏[ B ] (y β‹Ž[ B ] z) ＝ (x ⋏[ B ] y) β‹Ž[ B ] (x ⋏[ B ] z)
⋏-distributes-over-β‹Ž (_ , _ , (_ , _ , _ , _ , _ , Ο† , _)) = Ο†

\end{code}

\begin{code}

is-lattice-homomorphism : (B : BooleanAlgebra 𝓀′ π“₯β€²) (L : Frame 𝓀 π“₯ 𝓦)
                        β†’ (βŸͺ B ⟫ β†’ ⟨ L ⟩) β†’ Ξ© (𝓀′ βŠ” 𝓀)
is-lattice-homomorphism {𝓀′} {π“₯β€²} {𝓀} {π“₯} B L Ξ· = Ξ² ∧ Ξ³ ∧ Ξ΄ ∧ Ο΅
 where
  iss : is-set ⟨ L ⟩
  iss = carrier-of-[ poset-of L ]-is-set

  Ξ² : Ξ© 𝓀
  β = η ⊀[ B ] ＝[ iss ]＝ 𝟏[ L ]

  Ξ³ : Ξ© (𝓀′ βŠ” 𝓀)
  Ξ³ = β±― x κž‰ βŸͺ B ⟫ , β±― y κž‰ βŸͺ B ⟫ , Ξ· (x ⋏[ B ] y) ＝[ iss ]＝ Ξ· x ∧[ L ] Ξ· y

  Ξ΄ : Ξ© 𝓀
  Ξ΄ = Ξ· βŠ₯[ B ] ＝[ iss ]＝ 𝟎[ L ]

  Ο΅ : Ξ© (𝓀′ βŠ” 𝓀)
  Ο΅ = β±― x κž‰ βŸͺ B ⟫ , β±― y κž‰ βŸͺ B ⟫ , Ξ· (x β‹Ž[ B ] y) ＝[ iss ]＝ Ξ· x ∨[ L ] Ξ· y

is-ba-homomorphism : (B₁ : BooleanAlgebra 𝓀 π“₯) (Bβ‚‚ : BooleanAlgebra 𝓀' π“₯')
                   β†’ (f : βŸͺ B₁ ⟫ β†’ βŸͺ Bβ‚‚ ⟫) β†’ Ξ© (𝓀 βŠ” 𝓀')
is-ba-homomorphism {𝓀} {π“₯} {𝓀'} {π“₯'} B₁ Bβ‚‚ f = Ξ² ∧ Ξ³ ∧ Ξ΄ ∧ Ο΅
 where
  Οƒ : is-set βŸͺ Bβ‚‚ ⟫
  Οƒ = carrier-of-[ poset-of-ba Bβ‚‚ ]-is-set

  Ξ² : Ξ© 𝓀'
  Ξ² = f ⊀[ B₁ ] ＝[ Οƒ ]＝ ⊀[ Bβ‚‚ ]

  Ξ³ : Ξ© (𝓀 βŠ” 𝓀')
  Ξ³ = β±― x κž‰ βŸͺ B₁ ⟫ , β±― y κž‰ βŸͺ B₁ ⟫ , f (x ⋏[ B₁ ] y) ＝[ Οƒ ]＝ f x ⋏[ Bβ‚‚ ] f y

  Ξ΄ : Ξ© 𝓀'
  Ξ΄ = f βŠ₯[ B₁ ] ＝[ Οƒ ]＝ βŠ₯[ Bβ‚‚ ]

  Ο΅ : Ξ© (𝓀 βŠ” 𝓀')
  Ο΅ = β±― x κž‰ βŸͺ B₁ ⟫ , β±― y κž‰ βŸͺ B₁ ⟫ , f (x β‹Ž[ B₁ ] y) ＝[ Οƒ ]＝ f x β‹Ž[ Bβ‚‚ ] f y

lattice-homomorphisms-are-monotone : (B : BooleanAlgebra 𝓀′ π“₯β€²) (L : Frame 𝓀 π“₯ 𝓦)
                                    β†’ (h : βŸͺ B ⟫ β†’ ⟨ L ⟩)
                                    β†’ is-lattice-homomorphism B L h holds
                                    β†’ (x y : βŸͺ B ⟫)
                                    β†’ (x ≀[ poset-of-ba B ] y) holds
                                    β†’ (h x ≀[ poset-of L ] h y) holds
lattice-homomorphisms-are-monotone B L h (Ξ² , Ξ³ , _) x y p =
 h x ＝⟨ † ⁻¹ βŸ©β‚š h x ∧[ L ] h y β‰€βŸ¨ ∧[ L ]-lowerβ‚‚ (h x) (h y) ⟩ h y β– 
  where
   open PosetReasoning (poset-of L)

   ‑ : x ⋏[ B ] y ＝ x
   ‑ = ≀-is-antisymmetric (poset-of-ba B)
        (⋏[ B ]-is-lower₁ x y)
        (⋏[ B ]-is-greatest (≀-is-reflexive (poset-of-ba B) x) p)

   † : h x ∧[ L ] h y ＝ h x
   † = h x ∧[ L ] h y      ＝⟨ Ξ³ x y ⁻¹  ⟩
       h (x ⋏[ B ] y)      ＝⟨ ap h ‑    ⟩
       h x                 ∎

is-ba-embedding : (B : BooleanAlgebra 𝓀′ π“₯β€²) (L : Frame 𝓀 π“₯ 𝓦)
             β†’ (βŸͺ B ⟫ β†’ ⟨ L ⟩) β†’ Ξ© (𝓀′ βŠ” 𝓀)
is-ba-embedding {𝓀′} {π“₯β€²} {𝓀} {π“₯} {𝓦} B L Ξ· =
 ι ∧ is-lattice-homomorphism B L η
  where
   iss : is-set ⟨ L ⟩
   iss = carrier-of-[ poset-of L ]-is-set

   issβ‚€ : is-set βŸͺ B ⟫
   issβ‚€ = carrier-of-[ poset-of-ba B ]-is-set

   ΞΉ : Ξ© (𝓀′ βŠ” 𝓀)
   ΞΉ = β±― x κž‰ βŸͺ B ⟫ , β±― y κž‰ βŸͺ B ⟫ , (Ξ· x ＝[ iss ]＝ Ξ· y) β‡’ (x ＝[ issβ‚€ ]＝ y)

embedding-preserves-meets : (B : BooleanAlgebra 𝓀′ π“₯β€²) (L : Frame 𝓀 π“₯ 𝓦)
                          β†’ (Ξ· : βŸͺ B ⟫ β†’ ⟨ L ⟩)
                          β†’ is-ba-embedding B L Ξ· holds
                          β†’ (x y : βŸͺ B ⟫) β†’ Ξ· (x ⋏[ B ] y) ＝ Ξ· x ∧[ L ] Ξ· y
embedding-preserves-meets B L Ξ· (_ , (_ , ΞΎ , _)) = ΞΎ

embedding-injective : (B : BooleanAlgebra 𝓀′ π“₯β€²) (L : Frame 𝓀 π“₯ 𝓦)
                    β†’ (Ξ· : βŸͺ B ⟫ β†’ ⟨ L ⟩)
                    β†’ is-ba-embedding B L Ξ· holds
                    β†’ (x y : βŸͺ B ⟫) β†’ Ξ· x ＝ Ξ· y β†’ x ＝ y
embedding-injective B L Ξ· (ΞΉ , _) = ΞΉ

is-spectralβ€² : (B : BooleanAlgebra 𝓀′ π“₯β€²) (L : Frame 𝓀 π“₯ 𝓦)
            β†’ (f : βŸͺ B ⟫ β†’ ⟨ L ⟩) β†’ Ξ© (𝓀′ βŠ” 𝓀 βŠ” π“₯ βŠ” 𝓦 ⁺)
is-spectralβ€² B L f = β±― x κž‰ βŸͺ B ⟫ , is-compact-open L (f x)

\end{code}

\begin{code}

_is-sublattice-of_ : BooleanAlgebra 𝓀′ π“₯β€² β†’ Frame 𝓀 π“₯ 𝓦 β†’ Ξ© (𝓀′ βŠ” 𝓀)
_is-sublattice-of_ B L = Ǝ Ξ· κž‰ (βŸͺ B ⟫ β†’ ⟨ L ⟩) , is-ba-embedding B L Ξ· holds

\end{code}

\begin{code}

embedding-preserves-and-reflects-order : (B : BooleanAlgebra 𝓀′ π“₯β€²) (L : Frame 𝓀 π“₯ 𝓦)
                                       β†’ (Ξ· : βŸͺ B ⟫ β†’ ⟨ L ⟩)
                                       β†’ (ΞΌ : is-ba-embedding B L Ξ· holds)
                                       β†’ (x y : βŸͺ B ⟫)
                                       β†’ (x ≀[ poset-of-ba B ] y
                                       ⇔ Ξ· x ≀[ poset-of L ] Ξ· y) holds
embedding-preserves-and-reflects-order B L Ξ· ΞΌ x y = † , ‑
 where
  Ξ·-meet-preserving : (x y : βŸͺ B ⟫) β†’ Ξ· (x ⋏[ B ] y) ＝ Ξ· x ∧[ L ] Ξ· y
  Ξ·-meet-preserving = embedding-preserves-meets B L Ξ· ΞΌ

  † : (x ≀[ poset-of-ba B ] y β‡’ Ξ· x ≀[ poset-of L ] Ξ· y) holds
  † p = Ξ· x              ＝⟨ ap Ξ· (β€» ⁻¹)              βŸ©β‚š
        Ξ· (x ⋏[ B ] y)   ＝⟨ Ξ·-meet-preserving x y    βŸ©β‚š
        Ξ· x ∧[ L ] Ξ· y   β‰€βŸ¨ ∧[ L ]-lowerβ‚‚ (Ξ· x) (Ξ· y) ⟩
        Ξ· y              β– 
   where
    open PosetReasoning (poset-of L)

    β€» : x ⋏[ B ] y ＝ x
    β€» = ≀-is-antisymmetric (poset-of-ba B) ※₁ β€»β‚‚
     where
      ※₁ : ((x ⋏[ B ] y) ≀[ poset-of-ba B ] x) holds
      ※₁ = ⋏[ B ]-is-lower₁ x y

      β€»β‚‚ : (x ≀[ poset-of-ba B ] (x ⋏[ B ] y)) holds
      β€»β‚‚ = ⋏[ B ]-is-greatest (≀-is-reflexive (poset-of-ba B) x) p

  ‑ : (Ξ· x ≀[ poset-of L ] Ξ· y β‡’ x ≀[ poset-of-ba B ] y) holds
  ‑ p = x ＝⟨ β™  ⁻¹ βŸ©β‚š x ⋏[ B ] y β‰€βŸ¨ ⋏[ B ]-is-lowerβ‚‚ x y ⟩ y β– 
   where
    open PosetReasoning (poset-of-ba B)

    β™₯ : Ξ· (x ⋏[ B ] y) ＝ Ξ· x
    β™₯ = Ξ· (x ⋏[ B ] y)     ＝⟨ embedding-preserves-meets B L Ξ· ΞΌ x y ⟩
        Ξ· x ∧[ L ] Ξ· y     ＝⟨ connecting-lemma₁ L p ⁻¹              ⟩
        η x                ∎

    β™  : x ⋏[ B ] y ＝ x
    β™  = embedding-injective B L Ξ· ΞΌ (x ⋏[ B ] y) x β™₯

embeddings-lemma : (B : BooleanAlgebra 𝓀′ π“₯β€²) (L : Frame 𝓀 π“₯ 𝓦)
                 β†’ (Ξ· : βŸͺ B ⟫ β†’ ⟨ L ⟩)
                 β†’ is-ba-embedding B L Ξ· holds
                 β†’ (x : βŸͺ B ⟫) β†’ (Ξ· x ≀[ poset-of L ] 𝟎[ L ]) holds β†’ x ＝ βŠ₯[ B ]
embeddings-lemma B L Ξ· (ΞΉ , _ , (_ , ΞΎ , _)) x p = ΞΉ x βŠ₯[ B ] †
 where
  † : Ξ· x ＝ Ξ· βŠ₯[ B ]
  † = Ξ· x ＝⟨ only-𝟎-is-below-𝟎 L (Ξ· x) p ⟩ 𝟎[ L ] ＝⟨ ΞΎ ⁻¹   ⟩ Ξ· βŠ₯[ B ] ∎

\end{code}

\begin{code}

is-generated-by : (L : Frame 𝓀 𝓦 𝓦) β†’ (B : BooleanAlgebra 𝓦 π“₯)
                β†’ (βŸͺ B ⟫ β†’ ⟨ L ⟩) β†’ Ξ© 𝓀
is-generated-by {𝓦 = 𝓦} L B Ξ· =
 β±― x κž‰ ⟨ L ⟩ , x ＝[ Οƒ ]＝ (⋁[ L ] ⁅ Ξ· b ∣ (b , _) ∢ (Ξ£ b κž‰ βŸͺ B ⟫ , Ξ· b ≀ x) ⁆)
  where
   Οƒ : is-set ⟨ L ⟩
   Οƒ = carrier-of-[ poset-of L ]-is-set

   _≀_ = Ξ» x y β†’ (x ≀[ poset-of L ] y) holds

contains-compact-opens : (L : Frame 𝓀 𝓦 𝓦) (B : BooleanAlgebra 𝓦 π“₯)
                       β†’ (βŸͺ B ⟫ β†’ ⟨ L ⟩) β†’ Ξ© (𝓀 βŠ” 𝓦 ⁺)
contains-compact-opens L B Ξ· =
 β±― x κž‰ ⟨ L ⟩ , is-compact-open L x β‡’ (Ǝ b κž‰ βŸͺ B ⟫ , Ξ· b ＝ x)

\end{code}

\begin{code}

open FrameHomomorphisms

extension-lemma : (B : BooleanAlgebra 𝓦 𝓦) (L Lβ€² : Frame 𝓀 𝓦 𝓦)
                β†’ (Ξ· : βŸͺ B ⟫ β†’ ⟨ L ⟩)
                β†’ is-ba-embedding B L Ξ· holds
                β†’ is-spectral L holds
                β†’ is-spectralβ€² B L Ξ· holds
                β†’ is-generated-by L B Ξ· holds
                β†’ contains-compact-opens L B Ξ· holds
                β†’ (h : βŸͺ B ⟫ β†’ ⟨ Lβ€² ⟩)
                β†’ is-lattice-homomorphism B Lβ€² h holds
                β†’ βˆƒ! hβ‚€ κž‰ (⟨ L ⟩ β†’ ⟨ Lβ€² ⟩) ,
                   is-a-frame-homomorphism L Lβ€² hβ‚€ holds Γ— (h ＝ hβ‚€ ∘ Ξ·)
extension-lemma {𝓦} {𝓀} B L Lβ€² Ξ· e@(_ , _ , _ , β™₯₁ , β™₯β‚‚) Οƒ s Ξ³ π•œ h ΞΌ@(β™ β‚€ , ♠₁ , β™ β‚‚ , ♠₃) =
 (h⁻ , Ο† , ψ) , Ο‘
 where
  ↓↓_ : ⟨ L ⟩ β†’ Fam 𝓦 ⟨ Lβ€² ⟩
  ↓↓ x = ⁅ h b ∣ (b , _) ∢ Ξ£ b κž‰ βŸͺ B ⟫ , (Ξ· b ≀[ poset-of L ] x) holds  ⁆

  h⁻ : ⟨ L ⟩ β†’ ⟨ Lβ€² ⟩
  h⁻ x = ⋁[ Lβ€² ] ↓↓ x

\end{code}

We first show that `h⁻` preserves the top element.

\begin{code}

  Ο†β‚€ : h⁻ 𝟏[ L ] ＝ 𝟏[ Lβ€² ]
  Ο†β‚€ = only-𝟏-is-above-𝟏 Lβ€² (h⁻ 𝟏[ L ]) †
   where
    β™₯β‚€ = pr₁ (prβ‚‚ e)

    ‑ = ⋁[ Lβ€² ]-upper _ (⊀[ B ] , reflexivity+ (poset-of L) β™₯β‚€)

    open PosetReasoning (poset-of Lβ€²)

    † : (𝟏[ Lβ€² ] ≀[ poset-of Lβ€² ] h⁻ 𝟏[ L ]) holds
    † = 𝟏[ Lβ€² ]      ＝⟨ β™ β‚€ ⁻¹ βŸ©β‚š
        h ⊀[ B ]     β‰€βŸ¨ ‑ ⟩
        h⁻ 𝟏[ L ]    β– 

  φ₃ : h⁻ 𝟎[ L ] ＝ 𝟎[ Lβ€² ]
  φ₃ = only-𝟎-is-below-𝟎 Lβ€² (h⁻ 𝟎[ L ]) †
   where
    open PosetReasoning (poset-of Lβ€²)
    open Joins (Ξ» x y β†’ x ≀[ poset-of Lβ€² ] y)

    † : (h⁻ 𝟎[ L ] ≀[ poset-of Lβ€² ] 𝟎[ Lβ€² ]) holds
    † = h⁻ 𝟎[ L ]              ＝⟨ refl βŸ©β‚š
        ⋁[ Lβ€² ] (↓↓ 𝟎[ L ])    β‰€βŸ¨ β…      ⟩
        h βŠ₯[ B ]               ＝⟨ β™ β‚‚   βŸ©β‚š
        𝟎[ Lβ€² ]                β– 
         where
          β™₯ : Ξ· βŠ₯[ B ] ＝ 𝟎[ L ]
          β™₯ = pr₁ (prβ‚‚ (prβ‚‚ (prβ‚‚ e)))

          β€» : (h βŠ₯[ B ] is-an-upper-bound-of (↓↓ 𝟎[ L ])) holds
          β€» (b , q) = h b         ＝⟨ ap h (embeddings-lemma B L Ξ· e b q) βŸ©β‚š
                      h βŠ₯[ B ]    β– 

          β…  = ⋁[ Lβ€² ]-least (↓↓ 𝟎[ L ]) (h βŠ₯[ B ] , β€»)

\end{code}

The function `h⁻` also preserves meets.

\begin{code}

  φ₁ : (x y : ⟨ L ⟩) β†’ h⁻ (x ∧[ L ] y) ＝ h⁻ x ∧[ Lβ€² ] h⁻ y
  φ₁ x y = ≀-is-antisymmetric (poset-of Lβ€²) † ‑
   where
    † : (h⁻ (x ∧[ L ] y) ≀[ poset-of Lβ€² ] (h⁻ x ∧[ Lβ€² ] h⁻ y)) holds
    † = ∧[ Lβ€² ]-greatest (h⁻ x) (h⁻ y) (h⁻ (x ∧[ L ] y)) I II
     where
      open PosetReasoning (poset-of L)

      δ₁ : cofinal-in Lβ€² (↓↓ (x ∧[ L ] y)) (↓↓ x) holds
      δ₁ (b , p) = ∣ (b , (Ξ· b β‰€βŸ¨ p ⟩ x ∧[ L ] y β‰€βŸ¨ ∧[ L ]-lower₁ x y ⟩ x β– ))
                 , ≀-is-reflexive (poset-of Lβ€²) (h b) ∣

      Ξ΄β‚‚ : cofinal-in Lβ€² (↓↓ (x ∧[ L ] y)) (↓↓ y) holds
      Ξ΄β‚‚ (b , p) = ∣ (b , (Ξ· b β‰€βŸ¨ p ⟩ x ∧[ L ] y β‰€βŸ¨ ∧[ L ]-lowerβ‚‚ x y ⟩ y β– ))
                   , ≀-is-reflexive (poset-of Lβ€²) (h b) ∣

      I : (h⁻ (x ∧[ L ] y) ≀[ poset-of Lβ€² ] h⁻ x) holds
      I = cofinal-implies-join-covered Lβ€² _ _ δ₁

      II : (h⁻ (x ∧[ L ] y) ≀[ poset-of Lβ€² ] h⁻ y) holds
      II = cofinal-implies-join-covered Lβ€² _ _ Ξ΄β‚‚

    β„± : Fam 𝓦 ⟨ Lβ€² ⟩
    β„± = ⁅ (h b₁) ∧[ Lβ€² ] (h bβ‚‚)
         ∣ ((b₁ , _) , (bβ‚‚ , _))
            ∢ (Ξ£ b₁ κž‰ βŸͺ B ⟫ , (Ξ· b₁ ≀[ poset-of L ] x) holds)
            Γ— ((Ξ£ bβ‚‚ κž‰ βŸͺ B ⟫ , (Ξ· bβ‚‚ ≀[ poset-of L ] y) holds)) ⁆

    ‑ : ((h⁻ x ∧[ Lβ€² ] h⁻ y) ≀[ poset-of Lβ€² ] h⁻ (x ∧[ L ] y)) holds
    ‑ =
     h⁻ x ∧[ Lβ€² ] h⁻ y                        ＝⟨ refl βŸ©β‚š
     (⋁[ Lβ€² ] ↓↓ x) ∧[ Lβ€² ] (⋁[ Lβ€² ] ↓↓ y)    ＝⟨ β…  βŸ©β‚š
     ⋁[ Lβ€² ] β„±                                β‰€βŸ¨ β…‘ ⟩
     h⁻ (x ∧[ L ] y)                          β– 
      where
       open PosetReasoning (poset-of Lβ€²)
       open Joins (Ξ» x y β†’ x ≀[ poset-of Lβ€² ] y)

       β…  = distributivity+ Lβ€² (↓↓ x) (↓↓ y)

       Ξ² : (h⁻ (x ∧[ L ] y) is-an-upper-bound-of β„±) holds
       Ξ² ((b₁ , ϕ₁) , (bβ‚‚ , Ο•β‚‚)) = h b₁ ∧[ Lβ€² ] h bβ‚‚     ＝⟨ ♠₁ b₁ bβ‚‚ ⁻¹ βŸ©β‚š
                                   h (b₁ ⋏[ B ] bβ‚‚)      β‰€βŸ¨ ΞΆ ⟩
                                   h⁻ (x ∧[ L ] y)       β– 
        where
         ΞΎ : (Ξ· (b₁ ⋏[ B ] bβ‚‚) ≀[ poset-of L ] (x ∧[ L ] y)) holds
         ΞΎ = Ξ· (b₁ ⋏[ B ] bβ‚‚)      ＝⟨ pr₁ (prβ‚‚ (prβ‚‚ e)) b₁ bβ‚‚ ⟩L
             Ξ· b₁ ∧[ L ] Ξ· bβ‚‚      β‰€βŸ¨ ∧[ L ]-left-monotone ϕ₁ ⟩L
             x ∧[ L ] Ξ· bβ‚‚         β‰€βŸ¨ ∧[ L ]-right-monotone Ο•β‚‚ ⟩L
             x ∧[ L ] y            β– L
              where
               open PosetReasoning (poset-of L)
                renaming (_β‰€βŸ¨_⟩_ to _β‰€βŸ¨_⟩L_; _β–  to _β– L; _＝⟨_βŸ©β‚š_ to _＝⟨_⟩L_)

         ΞΆ : (h (b₁ ⋏[ B ] bβ‚‚) ≀[ poset-of Lβ€² ] (⋁[ Lβ€² ] ↓↓ (x ∧[ L ] y))) holds
         ΞΆ = ⋁[ Lβ€² ]-upper (↓↓ (x ∧[ L ] y)) ((b₁ ⋏[ B ] bβ‚‚) , ΞΎ)

       β…‘ = ⋁[ Lβ€² ]-least _ (h⁻ (x ∧[ L ] y) , Ξ²)

\end{code}

\begin{code}

  h⁻-is-monotone : is-monotonic (poset-of L) (poset-of Lβ€²) h⁻ holds
  h⁻-is-monotone = meet-preserving-implies-monotone L Lβ€² h⁻ φ₁

\end{code}

\begin{code}

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

  Οˆβ‚ : h ∼ h⁻ ∘ Ξ·
  Οˆβ‚ b = ≀-is-antisymmetric (poset-of Lβ€²) (Ο‡ b) (Ο• b)
   where
    open PosetReasoning (poset-of Lβ€²)

    Ο‡ : (b : βŸͺ B ⟫) β†’ (h b ≀[ poset-of Lβ€² ] h⁻ (Ξ· b)) holds
    Ο‡ b = ⋁[ Lβ€² ]-upper (↓↓ (Ξ· b)) (b , ≀-is-reflexive (poset-of L) (Ξ· b))

    Ο• : (b : βŸͺ B ⟫) β†’ (h⁻ (Ξ· b) ≀[ poset-of Lβ€² ] h b) holds
    Ο• b = ⋁[ Lβ€² ]-least (↓↓ (Ξ· b)) (h b , ϕ₁)
     where
      ϕ₁ : (h b is-an-upper-bound-of (↓↓ Ξ· b)) holds
      ϕ₁ (bα΅’ , p) = lattice-homomorphisms-are-monotone B Lβ€² h ΞΌ bα΅’ b Ο•β‚‚
       where
        Ο•β‚‚ : (bα΅’ ≀[ poset-of-ba B ] b) holds
        Ο•β‚‚ = prβ‚‚ (embedding-preserves-and-reflects-order B L Ξ· e bα΅’ b) p

  ψ : h ＝ h⁻ ∘ η
  ψ = dfunext fe Οˆβ‚

\end{code}

\begin{code}

  ΢⁻ : is-scott-continuous L Lβ€² h⁻ holds
  ΢⁻ S Ξ΄ = transport (Ξ» - β†’ (- is-lub-of ⁅ h⁻ x ∣ x Ξ΅ S ⁆) holds) (β€» ⁻¹) ♣
   where
    † : (h⁻ (⋁[ L ] S) ≀[ poset-of Lβ€² ] (⋁[ Lβ€² ] ⁅ h⁻ x ∣ x Ξ΅ S ⁆)) holds
    † = ⋁[ Lβ€² ]-least (↓↓ (⋁[ L ] S)) ((⋁[ Lβ€² ] ⁅ h⁻ x ∣ x Ξ΅ S ⁆) , †₁)
     where
      open PosetReasoning (poset-of Lβ€²)

      †₁ : ((⋁[ Lβ€² ] ⁅ h⁻ x ∣ x Ξ΅ S ⁆) is-an-upper-bound-of (↓↓ (⋁[ L ] S))) holds
      †₁ (b , p) =
       h b                          ＝⟨ Οˆβ‚ b βŸ©β‚š
       h⁻ (Ξ· b)                     β‰€βŸ¨ †₂ ⟩
       ⋁[ Lβ€² ] ⁅ h⁻ x ∣ x Ξ΅ S ⁆     β– 
        where
         †₃ : (Ξ£ k κž‰ index S , ((Ξ· b ≀[ poset-of L ] (S [ k ])) holds))
            β†’ (h⁻ (Ξ· b) ≀[ poset-of Lβ€² ] (⋁[ Lβ€² ] (⁅ h⁻ x ∣ x Ξ΅ S ⁆))) holds
         †₃ (k , q) =
          h⁻ (Ξ· b)                   β‰€βŸ¨ h⁻-is-monotone (Ξ· b , S [ k ]) q ⟩
          h⁻ (S [ k ])               β‰€βŸ¨ ⋁[ Lβ€² ]-upper ⁅ h⁻ x ∣ x Ξ΅ S ⁆ k ⟩
          ⋁[ Lβ€² ] ⁅ h⁻ x ∣ x Ξ΅ S ⁆   β– 

         †₂ : (h⁻ (Ξ· b) ≀[ poset-of Lβ€² ] (⋁[ Lβ€² ] (⁅ h⁻ x ∣ x Ξ΅ S ⁆))) holds
         †₂ = βˆ₯βˆ₯-rec (holds-is-prop (_ ≀[ poset-of Lβ€² ] _)) †₃ (s b S Ξ΄ p)

    ‑ : ((⋁[ Lβ€² ] ⁅ h⁻ x ∣ x Ξ΅ S ⁆) ≀[ poset-of Lβ€² ] h⁻ (⋁[ L ] S)) holds
    ‑ = ⋁[ Lβ€² ]-least ⁅ h⁻ x ∣ x Ξ΅ S ⁆ (h⁻ (⋁[ L ] S) , ‑₁)
     where
      ‑₁ : (h⁻ (⋁[ L ] S) is-an-upper-bound-of ⁅ h⁻ x ∣ x Ξ΅ S ⁆) holds
      ‑₁ i = h⁻-is-monotone ((S [ i ]) , ⋁[ L ] S) (⋁[ L ]-upper S i)

    β€» : h⁻ (⋁[ L ] S) ＝ ⋁[ Lβ€² ] ⁅ h⁻ x ∣ x Ξ΅ S ⁆
    β€» = ≀-is-antisymmetric (poset-of Lβ€²) † ‑

    ♣ : ((⋁[ Lβ€² ] ⁅ h⁻ x ∣ x Ξ΅ S ⁆) is-lub-of ⁅ h⁻ x ∣ x Ξ΅ S ⁆) holds
    ♣ = ⋁[ Lβ€² ]-upper ⁅ h⁻ x ∣ x Ξ΅ S ⁆ , ⋁[ Lβ€² ]-least ⁅ h⁻ x ∣ x Ξ΅ S ⁆

  h⁻-preserves-∨ : (x y : ⟨ L ⟩) β†’ h⁻ (x ∨[ L ] y) ＝ h⁻ x ∨[ Lβ€² ] h⁻ y
  h⁻-preserves-∨ x y = ≀-is-antisymmetric (poset-of Lβ€²) † ‑
   where
    ※₁ : (h⁻ x ≀[ poset-of Lβ€² ] h⁻ (x ∨[ L ] y)) holds
    ※₁ = h⁻-is-monotone (x , (x ∨[ L ] y)) (∨[ L ]-upper₁ x y)

    β€»β‚‚ : (h⁻ y ≀[ poset-of Lβ€² ] h⁻ (x ∨[ L ] y)) holds
    β€»β‚‚ = h⁻-is-monotone (y , (x ∨[ L ] y)) (∨[ L ]-upperβ‚‚ x y)

    † : (h⁻ (x ∨[ L ] y) ≀[ poset-of Lβ€² ] (h⁻ x ∨[ Lβ€² ] h⁻ y)) holds
    † = ⋁[ Lβ€² ]-least (↓↓ (x ∨[ L ] y)) ((h⁻ x ∨[ Lβ€² ] h⁻ y) , †₁)
     where
      †₁ : ((h⁻ x ∨[ Lβ€² ] h⁻ y) is-an-upper-bound-of (↓↓ (x ∨[ L ] y))) holds
      †₁ (b , p) = βˆ₯βˆ₯-rec
                    (holds-is-prop (h b ≀[ poset-of Lβ€² ] (h⁻ x ∨[ Lβ€² ] h⁻ y)))
                    †₂
                    ΰ₯
       where
        ΰ₯ : (Ǝ (c , d) κž‰ (⟨ L ⟩ Γ— ⟨ L ⟩) ,
                (is-compact-open L c holds)
              Γ— (is-compact-open L d holds)
              Γ— (Ξ· b ≀[ poset-of L ] (c ∨[ L ] d)) holds
              Γ— (c ≀[ poset-of L ] x) holds
              Γ— (d ≀[ poset-of L ] y) holds)
             holds
        ΰ₯ = compact-join-lemma L Οƒ x y (Ξ· b) (s b) p

        †₂ : Ξ£ (c , d) κž‰ (⟨ L ⟩ Γ— ⟨ L ⟩) ,
                (is-compact-open L c holds)
             Γ— (is-compact-open L d holds)
             Γ— (Ξ· b ≀[ poset-of L ] (c ∨[ L ] d)) holds
             Γ— (c ≀[ poset-of L ] x) holds
             Γ— (d ≀[ poset-of L ] y) holds
           β†’ (h b ≀[ poset-of Lβ€² ] (h⁻ x ∨[ Lβ€² ] h⁻ y)) holds
        †₂ ((c , d) , ΞΊc , ΞΊd , Ο‘ , Ο‡ , ΞΎ) =
         h b                  ＝⟨ Οˆβ‚ b βŸ©β‚š
         h⁻ (Ξ· b)             β‰€βŸ¨ β…    ⟩
         h⁻ (c ∨[ L ] d)      β‰€βŸ¨ β…‘   ⟩
         h⁻ c ∨[ Lβ€² ] h⁻ d    β‰€βŸ¨ β…€   ⟩
         h⁻ c ∨[ Lβ€² ] h⁻ y    β‰€βŸ¨ β…₯   ⟩
         h⁻ x ∨[ Lβ€² ] h⁻ y    β– 
          where
           open PosetReasoning (poset-of Lβ€²)

           β…  = h⁻-is-monotone (Ξ· b , (c ∨[ L ] d)) Ο‘

           β…‘ : (h⁻ (c ∨[ L ] d) ≀[ poset-of Lβ€² ] ((h⁻ c) ∨[ Lβ€² ] (h⁻ d))) holds
           β…‘ = h⁻ (c ∨[ L ] d) β‰€βŸ¨ ♣ ⟩ π“‡π’½π“ˆ ＝⟨ β€» ⁻¹ βŸ©β‚š h⁻ c ∨[ Lβ€² ] h⁻ d β– 
            where
             open PosetReasoning (poset-of L)
              renaming (_β‰€βŸ¨_⟩_ to _β‰€βŸ¨_βŸ©β‚—_; _β–  to _π””π”ˆπ”‡; _＝⟨_βŸ©β‚š_ to _＝⟨_βŸ©β‚—_)

             π“‡π’½π“ˆ =
              ⋁[ Lβ€² ]
               ⁅ h b₁ ∨[ Lβ€² ] h bβ‚‚
                 ∣ ((b₁ , _) , (bβ‚‚ , _))
                    ∢ (Ξ£ b₁ κž‰ βŸͺ B ⟫ , (Ξ· b₁ ≀[ poset-of L ] c) holds)
                    Γ— (Ξ£ bβ‚‚ κž‰ βŸͺ B ⟫ , (Ξ· bβ‚‚ ≀[ poset-of L ] d) holds) ⁆

             β€» : h⁻ c ∨[ Lβ€² ] h⁻ d
               ＝ ⋁[ Lβ€² ]
                   ⁅ h b₁ ∨[ Lβ€² ] h bβ‚‚
                     ∣ ((b₁ , _) , (bβ‚‚ , _))
                        ∢ (Ξ£ b₁ κž‰ βŸͺ B ⟫ , (Ξ· b₁ ≀[ poset-of L ] c) holds)
                        Γ— (Ξ£ bβ‚‚ κž‰ βŸͺ B ⟫ , (Ξ· bβ‚‚ ≀[ poset-of L ] d) holds) ⁆
             β€» = ∨[ Lβ€² ]-iterated-join (↓↓ c) (↓↓ d) ∣ i₁ ∣ ∣ iβ‚‚ ∣
              where
               i₁ : index (↓↓ c)
               i₁ = βŠ₯[ B ] , (Ξ· βŠ₯[ B ]    ＝⟨ β™₯₁             βŸ©β‚—
                              𝟎[ L ]      β‰€βŸ¨ 𝟎-is-bottom L c βŸ©β‚—
                              c           π””π”ˆπ”‡)

               iβ‚‚ : index (↓↓ d)
               iβ‚‚ = βŠ₯[ B ] , (Ξ· βŠ₯[ B ]    ＝⟨ β™₯₁             βŸ©β‚—
                              𝟎[ L ]      β‰€βŸ¨ 𝟎-is-bottom L d βŸ©β‚—
                              d           π””π”ˆπ”‡)

             ♣₁ : (π“‡π’½π“ˆ is-an-upper-bound-of (↓↓ (c ∨[ L ] d))) holds
             ♣₁ (b , q) =
              βˆ₯βˆ₯-recβ‚‚ (holds-is-prop (h b ≀[ poset-of Lβ€² ] π“‡π’½π“ˆ)) ♣₂ (π•œ c ΞΊc) (π•œ d ΞΊd)
               where
                ♣₂ : (Ξ£ b₁ κž‰ βŸͺ B ⟫ , Ξ· b₁ ＝ c)
                   β†’ (Ξ£ bβ‚‚ κž‰ βŸͺ B ⟫ , Ξ· bβ‚‚ ＝ d)
                   β†’ (h b ≀[ poset-of Lβ€² ] π“‡π’½π“ˆ) holds
                ♣₂ (b₁ , r₁) (bβ‚‚ , rβ‚‚) =
                 h b                     β‰€βŸ¨ β… β‚€ ⟩
                 h (b₁ β‹Ž[ B ] bβ‚‚)        ＝⟨ ♠₃ b₁ bβ‚‚ βŸ©β‚š
                 (h b₁) ∨[ Lβ€² ] (h bβ‚‚)   β‰€βŸ¨ α•― ⟩
                 π“‡π’½π“ˆ                     β– 
                  where
                   ᕯ₁ = reflexivity+ (poset-of L) r₁
                   α•―β‚‚ = reflexivity+ (poset-of L) rβ‚‚
                   α•―  = ⋁[ Lβ€² ]-upper _ ((b₁ , ᕯ₁), (bβ‚‚ , α•―β‚‚))

                   Ξ½ : (Ξ· b ≀[ poset-of L ] Ξ· (b₁ β‹Ž[ B ] bβ‚‚)) holds
                   Ξ½ = Ξ· b                    β‰€βŸ¨ q βŸ©β‚—
                       c ∨[ L ] d             ＝⟨ ϟ βŸ©β‚—
                       (Ξ· b₁) ∨[ L ] d        ＝⟨ Ο‘ βŸ©β‚—
                       (Ξ· b₁) ∨[ L ] (Ξ· bβ‚‚)   ＝⟨ Ν± βŸ©β‚—
                       Ξ· (b₁ β‹Ž[ B ] bβ‚‚)       π””π”ˆπ”‡
                        where
                         ϟ = ap (Ξ» - β†’ - ∨[ L ] d) (r₁ ⁻¹)
                         Ο‘ = ap (Ξ» - β†’ (Ξ· b₁) ∨[ L ] -) (rβ‚‚ ⁻¹)
                         Ν± = β™₯β‚‚ b₁ bβ‚‚ ⁻¹

                   Ο… : (b ≀[ poset-of-ba B ] (b₁ β‹Ž[ B ] bβ‚‚)) holds
                   Ο… = prβ‚‚ (embedding-preserves-and-reflects-order B L Ξ· e b _) Ξ½

                   β… β‚€ = lattice-homomorphisms-are-monotone B Lβ€² h ΞΌ b _ Ο…

             ♣ = ⋁[ Lβ€² ]-least (↓↓ (c ∨[ L ] d)) (π“‡π’½π“ˆ , ♣₁)

           β…€ = ∨[ Lβ€² ]-right-monotone (h⁻-is-monotone (d , y) ΞΎ)
           β…₯ = ∨[ Lβ€² ]-left-monotone (h⁻-is-monotone (c , x) Ο‡)

    ‑ : ((h⁻ x ∨[ Lβ€² ] h⁻ y) ≀[ poset-of Lβ€² ] h⁻ (x ∨[ L ] y)) holds
    ‑ = ∨[ Lβ€² ]-least ‑₁ ‑₂
     where
      ‑₁ : (h⁻ x ≀[ poset-of Lβ€² ] h⁻ (x ∨[ L ] y)) holds
      ‑₁ = ⋁[ Lβ€² ]-least (↓↓ x) (h⁻ (x ∨[ L ] y) , ♣₁)
       where
        ♣₁ : (h⁻ (x ∨[ L ] y) is-an-upper-bound-of (↓↓ x)) holds
        ♣₁ (b , p) = h b             β‰€βŸ¨ ⋁[ Lβ€² ]-upper (↓↓ x) (b , p) ⟩
                     h⁻ x            β‰€βŸ¨ ※₁                           ⟩
                     h⁻ (x ∨[ L ] y) β– 
                      where
                       open PosetReasoning (poset-of Lβ€²)

      ‑₂ : (h⁻ y ≀[ poset-of Lβ€² ] h⁻ (x ∨[ L ] y)) holds
      ‑₂ = ⋁[ Lβ€² ]-least (↓↓ y) (h⁻ (x ∨[ L ] y) , ♣₂)
       where
        ♣₂ : (h⁻ (x ∨[ L ] y) is-an-upper-bound-of (↓↓ y)) holds
        ♣₂ (b , p) = h b                β‰€βŸ¨ ⋁[ Lβ€² ]-upper (↓↓ y) (b , p) ⟩
                     ⋁[ Lβ€² ] (↓↓ y)     β‰€βŸ¨ β€»β‚‚                           ⟩
                     h⁻ (x ∨[ L ] y)    β– 
                      where
                       open PosetReasoning (poset-of Lβ€²)

  Ο†β‚‚ : (S : Fam 𝓦 ⟨ L ⟩) β†’ (h⁻ (⋁[ L ] S) is-lub-of ⁅ h⁻ x ∣ x Ξ΅ S ⁆) holds
  Ο†β‚‚ S@(I , π“Ž) =
   transport (Ξ» - β†’ (- is-lub-of ⁅ h⁻ x ∣ x Ξ΅ S ⁆) holds) († ⁻¹) ‑
    where
     † : h⁻ (⋁[ L ] S) ＝ ⋁[ Lβ€² ] ⁅ h⁻ x ∣ x Ξ΅ S ⁆
     † = sc-and-∨-preserving-β‡’-⋁-preserving L Lβ€² h⁻ ΢⁻ φ₃ h⁻-preserves-∨ S

     ‑ : ((⋁[ Lβ€² ] ⁅ h⁻ x ∣ x Ξ΅ S ⁆) is-lub-of ⁅ h⁻ x ∣ x Ξ΅ S ⁆) holds
     ‑ = ⋁[ Lβ€² ]-upper ⁅ h⁻ x ∣ x Ξ΅ S ⁆ , ⋁[ Lβ€² ]-least ⁅ h⁻ x ∣ x Ξ΅ S ⁆

\end{code}

\begin{code}

  Ο† : is-a-frame-homomorphism L Lβ€² h⁻ holds
  Ο† = Ο†β‚€ , φ₁ , Ο†β‚‚

\end{code}

The map `h⁻` is the _unique_ map making the diagram commute.

\begin{code}

  Ο‘ : is-central
       (Ξ£ h⁻₀ κž‰ (⟨ L ⟩ β†’ ⟨ Lβ€² ⟩) ,
         is-a-frame-homomorphism L Lβ€² h⁻₀ holds Γ— (h ＝ h⁻₀ ∘ Ξ·) )
       (h⁻ , (Ο† , ψ))
  Ο‘ (h⁻₀ , Ο†β€²@(φ′₁ , Ο†β€²β‚‚ , φ′₃) , Οˆβ€²) = to-subtype-＝ † (dfunext fe ϑ₁)
   where
    _≀L_ = Ξ» x y β†’ (x ≀[ poset-of L ] y) holds

    † : (hβ€² : ⟨ L ⟩ β†’ ⟨ Lβ€² ⟩)
      β†’ is-prop (is-a-frame-homomorphism L Lβ€² hβ€² holds Γ— (h ＝ hβ€² ∘ Ξ·))
    † hβ€² = Γ—-is-prop
            (holds-is-prop (is-a-frame-homomorphism L Lβ€² hβ€²))
            (Ξ -is-set fe Ξ» _ β†’ carrier-of-[ poset-of Lβ€² ]-is-set)

    ϑ₁ : (x : ⟨ L ⟩) β†’ h⁻ x ＝ h⁻₀ x
    ϑ₁ x =
     h⁻ x                                                      ＝⟨ refl ⟩
     ⋁[ Lβ€² ] (↓↓ x)                                            ＝⟨ refl ⟩
     ⋁[ Lβ€² ] ⁅ h b ∣ (b , _) ∢ Ξ£ b κž‰ βŸͺ B ⟫ , Ξ· b ≀L x  ⁆       ＝⟨ β…     ⟩
     ⋁[ Lβ€² ] ⁅ h⁻₀ (Ξ· b) ∣ (b , _) ∢ Ξ£ b κž‰ βŸͺ B ⟫ , Ξ· b ≀L x  ⁆ ＝⟨ β…‘    ⟩
     h⁻₀ (⋁[ L ] ⁅ Ξ· b ∣ (b , _) ∢ Ξ£ b κž‰ βŸͺ B ⟫ , Ξ· b ≀L x  ⁆)  ＝⟨ β…’    ⟩
     h⁻₀ x                                                     ∎
      where
       Οˆβ€²β€² : (b : βŸͺ B ⟫) β†’ h b ＝ h⁻₀ (Ξ· b)
       Οˆβ€²β€² b = ap (Ξ» - β†’ - b) Οˆβ€²

       β…  = ap
            (Ξ» - β†’ ⋁[ Lβ€² ] (index (↓↓ x) , -))
            (dfunext fe Ξ» { (b , _) β†’ Οˆβ€²β€² b})

       β…‘ = ⋁[ Lβ€² ]-unique _ _ (φ′₃ ⁅ Ξ· b ∣ (b , _) ∢ Ξ£ b κž‰ βŸͺ B ⟫ , Ξ· b ≀L x  ⁆) ⁻¹

       β…’ = ap h⁻₀ (Ξ³ x ⁻¹ )

\end{code}

\section{Transport}

Given a Boolean algebra `L` on some set `X : 𝓀` that has a copy in universe `π“₯`,
then `L` itself has a copy in universe `π“₯`

\begin{code}

transport-ba-structure : (X : 𝓀  Μ‡ ) (Y : 𝓀'  Μ‡ ) (f : X β†’ Y)
                       β†’ is-equiv f
                       β†’ (b : ba-structure π“₯ X)
                       β†’ Ξ£ bβ€² κž‰ ba-structure π“₯ Y ,
                          (is-ba-homomorphism (X , b) (Y , bβ€²) f holds)
transport-ba-structure {𝓀} {𝓀'} {π“₯} X Y f e b = (d , †) , f-is-hom
 where
  B₁ : BooleanAlgebra 𝓀 π“₯
  B₁ = X , b

  P₁ : Poset 𝓀 π“₯
  P₁ = poset-of-ba B₁

  open PosetNotation P₁

  g : Y β†’ X
  g = inverse f e

  _β‰Όα΅’_ : Y β†’ Y β†’ Ξ© π“₯
  y₁ β‰Όα΅’ yβ‚‚ = g y₁ ≀[ P₁ ] g yβ‚‚

  η : f ∘ g ∼ id
  Ξ· = inverses-are-sections f e

  Ρ : g ∘ f ∼ id
  Ξ΅ = inverses-are-retractions f e

  f-reflects-order : {x₁ xβ‚‚ : X} β†’ (f x₁ β‰Όα΅’ f xβ‚‚ β‡’ x₁ ≀ xβ‚‚) holds
  f-reflects-order {x₁} {xβ‚‚} = transport _holds †
   where
    † : f x₁ β‰Όα΅’ f xβ‚‚ ＝ x₁ ≀ xβ‚‚
    † = f x₁ β‰Όα΅’ f xβ‚‚         ＝⟨ refl                           ⟩
        g (f x₁) ≀ g (f xβ‚‚)  ＝⟨ ap (Ξ» - β†’ - ≀ g (f xβ‚‚)) (Ξ΅ x₁) ⟩
        x₁ ≀ g (f xβ‚‚)        ＝⟨ ap (Ξ» - β†’ x₁ ≀ -) (Ξ΅ xβ‚‚)       ⟩
        x₁ ≀ xβ‚‚              ∎

  β‰Όα΅’-is-reflexive : is-reflexive _β‰Όα΅’_ holds
  β‰Όα΅’-is-reflexive = ≀-is-reflexive (poset-of-ba B₁) ∘ g

  β‰Όα΅’-is-transitive : is-transitive _β‰Όα΅’_ holds
  β‰Όα΅’-is-transitive x y z p q =
   ≀-is-transitive (poset-of-ba B₁) (g x) (g y) (g z) † ‑
    where
     † : (g x ≀ g y) holds
     † = f-reflects-order
          (transportβ‚‚ (Ξ» a b β†’ (a ≀ b) holds) (ap g (Ξ· x) ⁻¹) (ap g (Ξ· y) ⁻¹) p)

     ‑ : (g y ≀ g z) holds
     ‑ = f-reflects-order
          (transportβ‚‚ (Ξ» a b β†’ (a ≀ b) holds) (ap g (Ξ· y) ⁻¹) (ap g (Ξ· z) ⁻¹) q)

  β‰Όα΅’-is-antisymmetric : is-antisymmetric _β‰Όα΅’_
  β‰Όα΅’-is-antisymmetric {x} {y} p q =
   x ＝⟨ Ξ· x ⁻¹ ⟩ f (g x) ＝⟨ ap f † ⟩ f (g y) ＝⟨ Ξ· y ⟩ y ∎
    where
     † : g x ＝ g y
     † = ≀-is-antisymmetric (poset-of-ba B₁) p q

  𝟏ᡒ : Y
  𝟏ᡒ = f ⊀[ B₁ ]

  𝟎ᡒ : Y
  𝟎ᡒ = f βŠ₯[ B₁ ]

  _⋏ᡒ_ : Y β†’ Y β†’ Y
  y₁ ⋏ᡒ yβ‚‚ = f (g y₁ ⋏[ B₁ ] g yβ‚‚)

  _β‹Žα΅’_ : Y β†’ Y β†’ Y
  y₁ β‹Žα΅’ yβ‚‚ = f (g y₁ β‹Ž[ B₁ ] g yβ‚‚)

  Β¬α΅’_ : Y β†’ Y
  Β¬α΅’ y = f (Β¬[ B₁ ] g y)

  g-preserves-meets : {y₁ yβ‚‚ : Y} β†’ g (y₁ ⋏ᡒ yβ‚‚) ＝ g y₁ ⋏[ B₁ ] g yβ‚‚
  g-preserves-meets {y₁} {yβ‚‚} = Ξ΅ (g y₁ ⋏[ B₁ ] g yβ‚‚)

  g-preserves-joins : {y₁ yβ‚‚ : Y} β†’ g (y₁ β‹Žα΅’ yβ‚‚) ＝ g y₁ β‹Ž[ B₁ ] g yβ‚‚
  g-preserves-joins {y₁} {yβ‚‚} = Ξ΅ (g y₁ β‹Ž[ B₁ ] g yβ‚‚)

  d : ba-data π“₯ Y
  d = _β‰Όα΅’_ , f ⊀[ B₁ ] , _⋏ᡒ_ , f βŠ₯[ B₁ ] , _β‹Žα΅’_ , Β¬α΅’_

  open Meets (Ξ» x y β†’ x β‰Όα΅’ y)
  open Joins (Ξ» x y β†’ x β‰Όα΅’ y)

  ρ : is-partial-order Y _β‰Όα΅’_
  ρ = (β‰Όα΅’-is-reflexive , β‰Όα΅’-is-transitive) , β‰Όα΅’-is-antisymmetric

  Pβ‚‚ : Poset 𝓀' π“₯
  Pβ‚‚ = Y , (_β‰Όα΅’_ , ρ)

  𝟏ᡒ-is-top : (y : Y) β†’ (y β‰Όα΅’ 𝟏ᡒ) holds
  𝟏ᡒ-is-top y = g y    β‰€βŸ¨ ⊀[ B₁ ]-is-top (g y) ⟩
               ⊀[ B₁ ] ＝⟨ Ξ΅ ⊀[ B₁ ] ⁻¹ βŸ©β‚š
               g (f ⊀[ B₁ ]) β– 
   where
    open PosetReasoning P₁

  𝟎ᡒ-is-bottom : (y : Y) β†’ (𝟎ᡒ β‰Όα΅’ y) holds
  𝟎ᡒ-is-bottom y = g 𝟎ᡒ           ＝⟨ refl                   βŸ©β‚š
                   g (f βŠ₯[ B₁ ])  ＝⟨ Ξ΅ βŠ₯[ B₁ ]              βŸ©β‚š
                   βŠ₯[ B₁ ]        β‰€βŸ¨ βŠ₯[ B₁ ]-is-bottom (g y) ⟩
                   g y            β– 
   where
    open PosetReasoning P₁

  ⋏ᡒ-is-glb : (y₁ yβ‚‚ : Y) β†’ ((y₁ ⋏ᡒ yβ‚‚) is-glb-of (y₁ , yβ‚‚)) holds
  ⋏ᡒ-is-glb y₁ yβ‚‚ = † , ‑
   where
    open PosetReasoning P₁

    †₁ : ((y₁ ⋏ᡒ yβ‚‚) β‰Όα΅’ y₁) holds
    †₁ = g (y₁ ⋏ᡒ yβ‚‚)       ＝⟨ g-preserves-meets βŸ©β‚š
         g y₁ ⋏[ B₁ ] g yβ‚‚  β‰€βŸ¨ ⋏[ B₁ ]-is-lower₁ (g y₁) (g yβ‚‚) ⟩
         g y₁               β– 

    †₂ : ((y₁ ⋏ᡒ yβ‚‚) β‰Όα΅’ yβ‚‚) holds
    †₂ = g (y₁ ⋏ᡒ yβ‚‚)       ＝⟨ g-preserves-meets βŸ©β‚š
         g y₁ ⋏[ B₁ ] g yβ‚‚  β‰€βŸ¨ ⋏[ B₁ ]-is-lowerβ‚‚ (g y₁) (g yβ‚‚) ⟩
         g yβ‚‚               β– 

    † : ((y₁ ⋏ᡒ yβ‚‚) is-a-lower-bound-of (y₁ , yβ‚‚)) holds
    † = †₁ , †₂

    ‑ : ((𝓁 , _) : lower-bound (y₁ , yβ‚‚)) β†’ (g 𝓁 ≀[ P₁ ] g (y₁ ⋏ᡒ yβ‚‚)) holds
    ‑ (𝓁 , p , q) = g 𝓁               β‰€βŸ¨ ⋏[ B₁ ]-is-greatest p q ⟩
                    g y₁ ⋏[ B₁ ] g yβ‚‚ ＝⟨ g-preserves-meets ⁻¹   βŸ©β‚š
                    g (y₁ ⋏ᡒ yβ‚‚)      β– 

  β‹Žα΅’-is-lub : (y₁ yβ‚‚ : Y) β†’ ((y₁ β‹Žα΅’ yβ‚‚) is-lub-ofβ‚‚ (y₁ , yβ‚‚)) holds
  β‹Žα΅’-is-lub y₁ yβ‚‚ = † , ‑
   where
    open PosetReasoning P₁

    † : ((y₁ β‹Žα΅’ yβ‚‚) is-an-upper-bound-ofβ‚‚ (y₁ , yβ‚‚)) holds
    † = †₁ , †₂
     where
      †₁ : (y₁ β‰Όα΅’ (y₁ β‹Žα΅’ yβ‚‚)) holds
      †₁ = g y₁                 β‰€βŸ¨ β‹Ž[ B₁ ]-is-upper₁ (g y₁) (g yβ‚‚) ⟩
           g y₁ β‹Ž[ B₁ ] g yβ‚‚    ＝⟨ g-preserves-joins ⁻¹           βŸ©β‚š
           g (y₁ β‹Žα΅’ yβ‚‚)         β– 

      †₂ : (yβ‚‚ β‰Όα΅’ (y₁ β‹Žα΅’ yβ‚‚)) holds
      †₂ = g yβ‚‚                β‰€βŸ¨ β‹Ž[ B₁ ]-is-upperβ‚‚ (g y₁) (g yβ‚‚) ⟩
           g y₁ β‹Ž[ B₁ ] g yβ‚‚   ＝⟨ g-preserves-joins ⁻¹ βŸ©β‚š
           g (y₁ β‹Žα΅’ yβ‚‚)        β– 

    ‑ : ((π“Š , _) : upper-boundβ‚‚ (y₁ , yβ‚‚)) β†’ (g (y₁ β‹Žα΅’ yβ‚‚) ≀[ P₁ ] g π“Š) holds
    ‑ (u , p , q) = g (y₁ β‹Žα΅’ yβ‚‚)      ＝⟨ g-preserves-joins   βŸ©β‚š
                    g y₁ β‹Ž[ B₁ ] g yβ‚‚ β‰€βŸ¨ β‹Ž[ B₁ ]-is-least p q ⟩
                    g u               β– 

  distributivityα΅’ : (y₁ yβ‚‚ y₃ : Y) β†’ y₁ ⋏ᡒ (yβ‚‚ β‹Žα΅’ y₃) ＝ (y₁ ⋏ᡒ yβ‚‚) β‹Žα΅’ (y₁ ⋏ᡒ y₃)
  distributivityα΅’ y₁ yβ‚‚ y₃ =
   y₁ ⋏ᡒ (yβ‚‚ β‹Žα΅’ y₃)                                        ＝⟨ refl ⟩
   f (g y₁ ⋏[ B₁ ] g (yβ‚‚ β‹Žα΅’ y₃))                           ＝⟨ β…     ⟩
   f (g y₁ ⋏[ B₁ ] (g yβ‚‚ β‹Ž[ B₁ ] g y₃))                    ＝⟨ β…‘    ⟩
   f ((g y₁ ⋏[ B₁ ] g yβ‚‚) β‹Ž[ B₁ ] (g y₁ ⋏[ B₁ ] g y₃))     ＝⟨ β…’    ⟩
   f (g (y₁ ⋏ᡒ yβ‚‚) β‹Ž[ B₁ ] g (y₁ ⋏ᡒ y₃))                   ＝⟨ refl ⟩
   (y₁ ⋏ᡒ yβ‚‚) β‹Žα΅’ (y₁ ⋏ᡒ y₃)                                ∎
    where
     β€» = Ξ» x y β†’ g-preserves-meets {x} {y} ⁻¹
     β…  = ap (Ξ» - β†’ f (g y₁ ⋏[ B₁ ] -)) g-preserves-joins
     β…‘ = ap f (⋏-distributes-over-β‹Ž B₁ (g y₁) (g yβ‚‚) (g y₃))
     β…’ = apβ‚‚ (Ξ» a b β†’ f (a β‹Ž[ B₁ ] b)) (β€» y₁ yβ‚‚) (β€» y₁ y₃)

  Οƒ = carrier-of-[ Pβ‚‚ ]-is-set

  open Complementation Οƒ 𝟎ᡒ 𝟏ᡒ _⋏ᡒ_ _β‹Žα΅’_

  Β¬α΅’-is-complement : (y : Y) β†’ ((Β¬α΅’ y) complements y) holds
  Β¬α΅’-is-complement y = † , ‑
   where
    † : f (g y ⋏[ B₁ ] g (f (Β¬[ B₁ ] g y))) ＝ f βŠ₯[ B₁ ]
    † = f (g y ⋏[ B₁ ] g (f (Β¬[ B₁ ] g y)))    ＝⟨ β…  ⟩
        f (g y ⋏[ B₁ ] Β¬[ B₁ ] g y)            ＝⟨ β…‘ ⟩
        f βŠ₯[ B₁ ]                              ∎
         where
          β…  = ap (Ξ» - β†’ f (g y ⋏[ B₁ ] -)) (Ξ΅ (Β¬[ B₁ ] g y))
          β…‘ = ap f (pr₁ (Β¬[ B₁ ]-is-complement (g y)))

    ‑ : f (g y β‹Ž[ B₁ ] g (f (Β¬[ B₁ ] g y)) ) ＝ f ⊀[ B₁ ]
    ‑ = f (g y β‹Ž[ B₁ ] g (f (Β¬[ B₁ ] g y)) )   ＝⟨ β…  ⟩
        f (g y β‹Ž[ B₁ ] Β¬[ B₁ ] g y)            ＝⟨ β…‘ ⟩
        f ⊀[ B₁ ]                              ∎
         where
          β…  = ap (Ξ» - β†’ f (g y β‹Ž[ B₁ ] -)) (Ξ΅ (Β¬[ B₁ ] g y))
          β…‘ = ap f (prβ‚‚ (Β¬[ B₁ ]-is-complement (g y)))

  † : satisfies-ba-laws d
  † = ρ
    , ⋏ᡒ-is-glb , 𝟏ᡒ-is-top , β‹Žα΅’-is-lub , 𝟎ᡒ-is-bottom
    , distributivityα΅’ , Β¬α΅’-is-complement

  f-is-hom : is-ba-homomorphism (X , b) (Y , d , †) f holds
  f-is-hom = refl , Ξ³ , refl , Ο΅
   where
    Ξ³ : (x₁ xβ‚‚ : X) β†’ f (x₁ ⋏[ B₁ ] xβ‚‚) ＝ f x₁ ⋏ᡒ f xβ‚‚
    Ξ³ x₁ xβ‚‚ = f (x₁ ⋏[ B₁ ] xβ‚‚)               ＝⟨ β…     ⟩
              f (g (f x₁) ⋏[ B₁ ] xβ‚‚)         ＝⟨ β…‘    ⟩
              f (g (f x₁) ⋏[ B₁ ] g (f xβ‚‚))   ＝⟨ β…’    ⟩
              f (g (f x₁ ⋏ᡒ f xβ‚‚))            ＝⟨ β…£    ⟩
              f (g (f x₁) ⋏[ B₁ ] g (f xβ‚‚))   ＝⟨ refl ⟩
              f x₁ ⋏ᡒ f xβ‚‚                    ∎
               where
                β…  = ap (Ξ» - β†’ f (-        ⋏[ B₁ ] xβ‚‚)) (Ξ΅ x₁ ⁻¹)
                β…‘ = ap (Ξ» - β†’ f (g (f x₁) ⋏[ B₁ ] -))  (Ξ΅ xβ‚‚ ⁻¹)
                β…’ = ap f g-preserves-meets ⁻¹
                β…£ = Ξ· (f x₁ ⋏ᡒ f xβ‚‚)

    Ο΅ : (x₁ xβ‚‚ : X) β†’ f (x₁ β‹Ž[ B₁ ] xβ‚‚) ＝ f x₁ β‹Žα΅’ f xβ‚‚
    Ο΅ x₁ xβ‚‚ = f (x₁ β‹Ž[ B₁ ] xβ‚‚)               ＝⟨ β…  ⟩
              f (g (f x₁) β‹Ž[ B₁ ] xβ‚‚)         ＝⟨ β…‘ ⟩
              f (g (f x₁) β‹Ž[ B₁ ] g (f xβ‚‚))   ＝⟨ β…’ ⟩
              f (g (f x₁ β‹Žα΅’ f xβ‚‚))            ＝⟨ β…£ ⟩
              f x₁ β‹Žα΅’ f xβ‚‚                    ∎
               where
                β…  = ap (Ξ» - β†’ f (- β‹Ž[ B₁ ] xβ‚‚))       (Ξ΅ x₁ ⁻¹)
                β…‘ = ap (Ξ» - β†’ f (g (f x₁) β‹Ž[ B₁ ] -)) (Ξ΅ xβ‚‚ ⁻¹)
                β…’ = ap f (g-preserves-joins ⁻¹ )
                β…£ = Ξ· (f x₁ β‹Žα΅’ f xβ‚‚)

\end{code}