Locales.ContinuousMap.Homeomorphism-Properties

--------------------------------------------------------------------------------
title:          Properties of locale homeomorphisms
author:         Ayberk Tosun
date-started:   2024-04-18
--------------------------------------------------------------------------------

Some properties of locale homeomorphisms.


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

open import MLTT.Spartan hiding (𝟚; ₀; ₁)
open import UF.FunExt
open import UF.PropTrunc
open import UF.Size
open import UF.Subsingletons
open import UF.UA-FunExt
open import UF.Univalence

module Locales.ContinuousMap.Homeomorphism-Properties
        (ua : Univalence)
        (pt : propositional-truncations-exist)
        (sr : Set-Replacement pt)
       where

private
 fe : Fun-Ext
 fe {𝓤} {𝓥} = univalence-gives-funext' 𝓤 𝓥 (ua 𝓤) (ua (𝓤 ⊔ 𝓥))

 pe : Prop-Ext
 pe {𝓤} = univalence-gives-propext (ua 𝓤)

open import Locales.ContinuousMap.FrameIsomorphism-Definition pt fe
open import Locales.ContinuousMap.Homeomorphism-Definition pt fe
open import Locales.Frame pt fe
open import Locales.SIP.FrameSIP ua pt sr
open import UF.Logic
open import UF.SubtypeClassifier

open AllCombinators pt fe
open Locale


Homeomorphic locales are equal.


homeomorphic-locales-are-equal : (X Y : Locale (𝓤 ⁺) 𝓤 𝓤) → X ≅c≅ Y → X ＝ Y
homeomorphic-locales-are-equal X Y 𝒽 = to-locale-＝ Y X † ⁻¹
 where
  open FrameIsomorphisms

  r : 𝒪 Y ≅f≅ 𝒪 X
  r = isomorphism-to-isomorphismᵣ
       (𝒪 Y)
       (𝒪 X)
       (isomorphismᵣ-to-isomorphism (𝒪 Y) (𝒪 X) 𝒽)

  † : 𝒪 Y ＝ 𝒪 X
  † = isomorphic-frames-are-equal (𝒪 Y) (𝒪 X) r


Transport lemma for homeomorphic locales.


≅c≅-transport : (X Y : Locale (𝓤 ⁺) 𝓤 𝓤)
              → (P : Locale (𝓤 ⁺) 𝓤 𝓤 → Ω 𝓣) → X ≅c≅ Y → P X holds → P Y holds
≅c≅-transport X Y P 𝒽 = transport (_holds ∘ P) p
 where
  p : X ＝ Y
  p = homeomorphic-locales-are-equal X Y 𝒽


Added on 2024-05-07.

Being homeomorphic is a symmetric relation.


≅c-sym : (X Y : Locale (𝓤 ⁺) 𝓤 𝓤) → X ≅c≅ Y → Y ≅c≅ X
≅c-sym X Y 𝒽 =
 record { 𝓈 = 𝓇 ; 𝓇 = 𝓈 ; 𝓇-cancels-𝓈 = 𝓈-cancels-𝓇 ; 𝓈-cancels-𝓇 = 𝓇-cancels-𝓈}
  where
   open FrameIsomorphisms.Isomorphismᵣ 𝒽