--------------------------------------------------------------------------------
title:          Homeomorphisms of locales
author:         Ayberk Tosun
date-started:   2024-04-11
date-completed: 2024-04-18
--------------------------------------------------------------------------------

A homeomorphism of locales is the same thing as an isomorphism of their
underlying frames. As we maintain a careful distinction between locales and
their defining frames, however, we give a different name to this notion.

\begin{code}[hide]

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

open import MLTT.Spartan hiding (𝟚; β‚€; ₁)
open import UF.FunExt
open import UF.PropTrunc

module Locales.ContinuousMap.Homeomorphism-Definition
        (pt : propositional-truncations-exist)
        (fe : Fun-Ext)
       where

open import Locales.ContinuousMap.FrameIsomorphism-Definition pt fe
open import Locales.Frame pt fe
open import UF.Logic

open AllCombinators pt fe
open Locale

\end{code}

A homeomorphism between locales `X` and `Y` is an isomorphism between their
defining frames.

\begin{code}

Homeomorphism : Locale 𝓀  π“₯  𝓦 β†’ Locale 𝓀' π“₯' 𝓦 β†’ 𝓀' βŠ” 𝓀 βŠ” π“₯ βŠ” π“₯' βŠ” 𝓦 ⁺ Μ‡
Homeomorphism X Y = Isomorphismα΅£ (π’ͺ Y) (π’ͺ X)
 where
  open FrameIsomorphisms

\end{code}

Declare syntax for homeomorphisms.

\begin{code}

Homeomorphism-Syntax : Locale 𝓀 π“₯ 𝓦 β†’ Locale 𝓀' π“₯' 𝓦 β†’ 𝓀 βŠ” 𝓀' βŠ” π“₯ βŠ” π“₯' βŠ” 𝓦 ⁺ Μ‡
Homeomorphism-Syntax = Homeomorphism

infix 0 Homeomorphism-Syntax
syntax Homeomorphism-Syntax X Y = X ≅c≅ Y

\end{code}