---
title:          The patch locale of the SierpiΕ„ski locale
author:         Ayberk Tosun
date-completed: 2024-02-12
---

\begin{code}

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

open import MLTT.Spartan hiding (𝟚)
open import UF.FunExt
open import UF.PropTrunc
open import UF.Size
open import UF.Subsingletons

module Locales.Sierpinski.Patch
        (𝓀  : Universe)
        (pe : Prop-Ext)
        (pt : propositional-truncations-exist)
        (fe : Fun-Ext)
        (sr : Set-Replacement pt)
       where

open import Locales.ContinuousMap.Definition pt fe
open import Locales.ContinuousMap.FrameHomomorphism-Definition pt fe
open import Locales.ContinuousMap.FrameHomomorphism-Properties pt fe
open import Locales.Frame pt fe hiding (𝟚; is-directed)
open import Locales.Sierpinski.Definition 𝓀 pe pt fe sr
open import Locales.Sierpinski.Properties 𝓀 pe pt fe sr
open import Locales.Spectrality.SpectralMap pt fe
open import Locales.Stone pt fe sr
open import UF.SubtypeClassifier

open ContinuousMaps
open FrameHomomorphismProperties
open FrameHomomorphisms
open Locale
open PropositionalTruncation pt

\end{code}

We conclude by constructing the patch of SierpiΕ„ski.

\begin{code}

open import Locales.ScottLocale.ScottLocalesOfScottDomains pt fe sr 𝓀

open SpectralScottLocaleConstruction π•Šπ““ π•Šπ““-has-least hscb π•Šπ““-satisfies-dc π•Šπ““-bounded-complete pe

open import Locales.PatchLocale pt fe sr

open SmallPatchConstruction π•Š π•Š-is-spectralα΄° renaming (SmallPatch to Patch-π•Š)

patch-of-π•Š : Locale (𝓀 ⁺) 𝓀 𝓀
patch-of-π•Š = Patch-π•Š

\end{code}

The universal property of Patch then specializes to the following.

\begin{code}

open import Locales.UniversalPropertyOfPatch pt fe sr

open import Locales.PatchProperties pt fe sr

open ClosedNucleus π•Š π•Š-is-spectral
open ContinuousMaps

ump-for-patch-of-π•Š : (X : Locale (𝓀 ⁺) 𝓀 𝓀)
                   β†’ is-stone X holds
                   β†’ (𝒻@(f , _) : X ─cβ†’ π•Š)
                   β†’ is-spectral-map π•Š X 𝒻 holds
                   β†’ βˆƒ! 𝒻⁻@(f⁻ , _) κž‰ X ─cβ†’ Patch-π•Š ,
                      ((U : ⟨ π’ͺ π•Š ⟩) β†’ f U ＝ f⁻ β€˜ U ’)
ump-for-patch-of-π•Š = ump-of-patch π•Š π•Š-is-spectral π•Š-has-small-𝒦

\end{code}