Ayberk Tosun, 15 October 2021

Based on `ayberkt/formal-topology-in-UF`.

\begin{code}[hide]

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

open import MLTT.Spartan
open import UF.FunExt
open import UF.PropTrunc

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

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 import UF.SubtypeClassifier

open AllCombinators pt fe
open FrameHomomorphismProperties
open FrameHomomorphisms
open Locale

\end{code}

\begin{code}

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

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

is-nucleus : (L : Frame 𝓀 π“₯ 𝓦) β†’ (⟨ L ⟩ β†’ ⟨ L ⟩) β†’ Ξ© (𝓀 βŠ” π“₯)
is-nucleus {𝓀 = 𝓀} {π“₯} {𝓦} F j = 𝓃₁ ∧  𝓃₂ ∧ 𝓃₃
 where
  open PosetNotation (poset-of F)

  𝓃₁ : Ξ© (𝓀 βŠ” π“₯)
  𝓃₁ = is-inflationary F j

  𝓃₂ : Ξ© (𝓀 βŠ” π“₯)
  𝓃₂ = is-idempotent F j

  𝓃₃ : Ξ© 𝓀
  𝓃₃ = preserves-binary-meets F F j

\end{code}

The type of nuclei on a given frame.

\begin{code}

Nucleus : Frame 𝓀 π“₯ 𝓦 β†’ 𝓀 βŠ” π“₯ Μ‡
Nucleus F = Ξ£ j κž‰ (⟨ F ⟩ β†’ ⟨ F ⟩) , is-nucleus F j holds

𝓃₁ : (L : Frame 𝓀 π“₯ 𝓦) ((j , _) : Nucleus L)
   β†’ (x : ⟨ L ⟩) β†’ (x ≀[ poset-of L ] j x) holds
𝓃₁ F (j , 𝓃₁ , _ , _)= 𝓃₁

𝓃₂ : (L : Frame 𝓀 π“₯ 𝓦) ((j , _) : Nucleus L)
   β†’ (U : ⟨ L ⟩) β†’ (j (j U) ≀[ poset-of L ] j U) holds
𝓃₂ F (j , _ , 𝓃₂ , _) = 𝓃₂

𝓃₃ : (L : Frame 𝓀 π“₯ 𝓦) ((j , _) : Nucleus L)
   β†’ (U V : ⟨ L ⟩) β†’ j (U ∧[ L ] V) ＝ j U ∧[ L ] j V
𝓃₃ F (j , _ , _ , 𝓃₃) = 𝓃₃

\end{code}

\begin{code}

identity-nucleus : (L : Frame 𝓀 π“₯ 𝓦) β†’ Nucleus L
identity-nucleus L = id , n₁ , nβ‚‚ , n₃
 where
  n₁ : is-inflationary L id holds
  n₁ = ≀-is-reflexive (poset-of L)

  nβ‚‚ : is-idempotent L id holds
  nβ‚‚ = ≀-is-reflexive (poset-of L)

  n₃ : preserves-binary-meets L L id holds
  n₃ x y = refl {x = x ∧[ L ] y}

\end{code}

In this development, it will be useful to define and work with the notion of a
prenucleus: a meet-preserving inflationary endomap (that is not necessary
idempotent):

\begin{code}

is-prenucleus : (L : Frame 𝓀 π“₯ 𝓦) (j : ⟨ L ⟩ β†’ ⟨ L ⟩) β†’ Ξ© (𝓀 βŠ” π“₯)
is-prenucleus L j = is-inflationary L j  ∧ preserves-binary-meets L L j

Prenucleus : Frame 𝓀 π“₯ 𝓦 β†’ (𝓀 βŠ” π“₯) Μ‡
Prenucleus L = Ξ£ j κž‰ (⟨ L ⟩ β†’ ⟨ L ⟩) , is-prenucleus L j holds

prenucleus-eq : (F : Frame 𝓀 π“₯ 𝓦) (𝒿 𝓀 : Prenucleus F)
              β†’ ((x : ⟨ F ⟩) β†’ 𝒿 .pr₁ x ＝ 𝓀 .pr₁ x)
              β†’ 𝒿 ＝ 𝓀
prenucleus-eq F 𝒿 𝓀 Ο† =
 to-subtype-＝ (Ξ» - β†’ holds-is-prop (is-prenucleus F -)) (dfunext fe Ο†)

module PrenucleusApplicationSyntax (L : Frame 𝓀 π“₯ 𝓦) where

 _$β‚š_ : Prenucleus L β†’ ⟨ L ⟩ β†’ ⟨ L ⟩
 _$β‚š_ = pr₁

 infixr 2 _$β‚š_

\end{code}

Inclusion of nuclei into the type of prenuclei:

\begin{code}

nucleus-pre : (L : Frame 𝓀 π“₯ 𝓦) β†’ Nucleus L β†’ Prenucleus L
nucleus-pre L 𝒿@(j , _) = j , 𝓃₁ L 𝒿 , 𝓃₃ L 𝒿

\end{code}

Prenuclei are monotone:

\begin{code}

prenuclei-are-monotone : (L : Frame 𝓀 π“₯ 𝓦)
                       β†’ ((j , _) : Prenucleus L)
                       β†’ is-monotonic (poset-of L) (poset-of L) j holds
prenuclei-are-monotone L (j , _ , ΞΌ) =
 meet-preserving-implies-monotone L L j ΞΌ

\end{code}

As a corollary, nuclei are monotone:

\begin{code}

nuclei-are-monotone : (L : Frame 𝓀 π“₯ 𝓦) ((j , _) : Nucleus L)
                    β†’ is-monotonic (poset-of L) (poset-of L) j holds
nuclei-are-monotone L 𝒿 = prenuclei-are-monotone L (nucleus-pre L 𝒿)

nuclei-are-idempotent : (L : Frame 𝓀 π“₯ 𝓦) ((j , _) : Nucleus L)
                      β†’ (x : ⟨ L ⟩) β†’ j (j x) ＝ j x
nuclei-are-idempotent L 𝒿@(j , _) x = ≀-is-antisymmetric (poset-of L) Ξ² Ξ³
 where
  Ξ² : (j (j x) ≀[ poset-of L ] j x) holds
  Ξ² = 𝓃₂ L 𝒿 x

  Ξ³ : (j x ≀[ poset-of L ] j (j x)) holds
  Ξ³ = 𝓃₁ L 𝒿 (j x)

\end{code}

\begin{code}

prenucleus-property₁ : (L : Frame 𝓀 π“₯ 𝓦)
                     β†’ ((j , _) (k , _) : Prenucleus L)
                     β†’ (β±― x κž‰ ⟨ L ⟩ , j x ≀[ poset-of L ] (j ∘ k) x) holds
prenucleus-property₁ L (j , _ , ΞΌj) (k , ΞΆ , _) x =
 meet-preserving-implies-monotone L L j ΞΌj (x , k x) (ΞΆ x)

prenucleus-propertyβ‚‚ : (L : Frame 𝓀 π“₯ 𝓦)
                     β†’ ((j , _) (k , _) : Prenucleus L)
                     β†’ (β±― x κž‰ ⟨ L ⟩ , k x ≀[ poset-of L ] (j ∘ k) x) holds
prenucleus-propertyβ‚‚ L (j , ΞΆj , _) (k , _) x = ΞΆj (k x)

\end{code}

\section{Closed nucleus}

\begin{code}

∨-is-inflationary : (L : Frame 𝓀 π“₯ 𝓦)
                  β†’ (x : ⟨ L ⟩) β†’ is-inflationary L (binary-join L x) holds
∨-is-inflationary L = ∨[ L ]-upperβ‚‚

∨-is-idempotent : (L : Frame 𝓀 π“₯ 𝓦)
                β†’ (x : ⟨ L ⟩) β†’ is-idempotent L (binary-join L x) holds
∨-is-idempotent L x y = ∨[ L ]-least
                         (∨[ L ]-upper₁ x y)
                         (≀-is-reflexive (poset-of L) (x ∨[ L ] y) )

∨-preserves-binary-meets : (L : Frame 𝓀 π“₯ 𝓦) (x : ⟨ L ⟩)
                         β†’ preserves-binary-meets L L (binary-join L x) holds
∨-preserves-binary-meets L x y₁ yβ‚‚ =
 x ∨[ L ] (y₁ ∧[ L ] yβ‚‚)             ＝⟨ binary-distributivity-op L x y₁ yβ‚‚ ⟩
 (x ∨[ L ] y₁) ∧[ L ] (x ∨[ L ] yβ‚‚)  ∎

∨-is-nucleus : (L : Frame 𝓀 π“₯ 𝓦)
             β†’ (x : ⟨ L ⟩)
             β†’ is-nucleus L (binary-join L x) holds
∨-is-nucleus L x = ∨-is-inflationary L x
                 , ∨-is-idempotent L x
                 , ∨-preserves-binary-meets L x

closed-nucleus : (X : Locale 𝓀 π“₯ 𝓦) (U : ⟨ π’ͺ X ⟩) β†’ Nucleus (π’ͺ X)
closed-nucleus X U = (Ξ» - β†’ U ∨[ π’ͺ X ] -) , ∨-is-nucleus (π’ͺ X) U

\end{code}

\begin{code}

open import Locales.HeytingImplication pt fe
open Locale

module NucleusHeytingImplicationLaw (X : Locale 𝓀 π“₯ π“₯)
                                    (𝒷 : has-basis (π’ͺ X) holds)
                                    (𝒿 : Nucleus (π’ͺ X))
                                     where

 open HeytingImplicationConstruction X 𝒷

 private
  j = pr₁ 𝒿

 nucleus-heyting-implication-law : (U V : ⟨ π’ͺ X ⟩)
                                 β†’ (U ==> j V) ＝ j U ==> j V
 nucleus-heyting-implication-law U V =
  ≀-is-antisymmetric (poset-of (π’ͺ X)) † ‑
   where
    open PosetReasoning (poset-of (π’ͺ X))

    ♣ : (((U ==> j V) ∧[ π’ͺ X ] j U) ≀[ poset-of (π’ͺ X) ] j V) holds
    ♣ = (U ==> j V)   ∧[ π’ͺ X ] j U     β‰€βŸ¨ β…   ⟩
        j (U ==> j V) ∧[ π’ͺ X ] j U     ＝⟨ β…‘ βŸ©β‚š
        j ((U ==> j V) ∧[ π’ͺ X ] U)     β‰€βŸ¨ β…’ ⟩
        j (j V)                        β‰€βŸ¨ β…£ ⟩
        j V                           β– 
         where
          β…  = ∧[ π’ͺ X ]-left-monotone (𝓃₁ (π’ͺ X) 𝒿 (U ==> j V))
          β…‘ = 𝓃₃ (π’ͺ X) 𝒿 (U ==> j V) U ⁻¹
          β…’ = nuclei-are-monotone (π’ͺ X) 𝒿 (_ , _) (mp-right U (j V))
          β…£ = 𝓃₂ (π’ͺ X) 𝒿 V

    β™₯ = (j U ==> j V) ∧[ π’ͺ X ] U       β‰€βŸ¨ β…  ⟩
        (j U ==> j V) ∧[ π’ͺ X ] j U     β‰€βŸ¨ β…‘ ⟩
        j V β– 
         where
          β…  = ∧[ π’ͺ X ]-right-monotone (𝓃₁ (π’ͺ X) 𝒿 U)
          β…‘ = mp-right (j U) (j V)

    † : ((U ==> j V) ≀[ poset-of (π’ͺ X) ] (j U ==> j V)) holds
    † = heyting-implication₁ (j U) (j V) (U ==> j V) ♣

    ‑ : ((j U ==> j V) ≀[ poset-of (π’ͺ X) ] (U ==> j V)) holds
    ‑ = heyting-implication₁ U (j V) (j U ==> j V) β™₯

\end{code}