--------------------------------------------------------------------------------
title:          Frame isomorphisms
author:         Ayberk Tosun
date-started:   2024-04-11
date-completed: 2024-04-18
--------------------------------------------------------------------------------

Various formulations of the notion of frame isomorphism, and proofs of their
equivalences.

\begin{code}[hide]

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

open import MLTT.Spartan hiding (𝟚; ₀; ₁)
open import UF.FunExt
open import UF.PropTrunc

module Locales.ContinuousMap.FrameIsomorphism-Definition
        (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.Equiv
open import UF.Equiv-FunExt
open import UF.Logic
open import UF.Retracts
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.SubtypeClassifier

open AllCombinators pt fe
open FrameHomomorphismProperties
open FrameHomomorphisms

\end{code}

We work in a module parameterized by two frames `F` and `G`.

\begin{code}

module FrameIsomorphisms (F : Frame 𝓤 𝓥 𝓦) (G : Frame 𝓤' 𝓥' 𝓦) where

\end{code}

We start with the record-based definition of the notion of frame isomorphism.

\begin{code}

 record Isomorphismᵣ : 𝓤 ⊔ 𝓤' ⊔ 𝓥 ⊔ 𝓥' ⊔ 𝓦 ⁺  ̇ where
  field
   𝓈 : F ─f→ G
   𝓇 : G ─f→ F

  s : ⟨ F ⟩ → ⟨ G ⟩
  s = fun F G 𝓈

  r : ⟨ G ⟩ → ⟨ F ⟩
  r = fun G F 𝓇

  s-is-homomorphism : is-a-frame-homomorphism F G s holds
  s-is-homomorphism = fun-is-a-frame-homomorphism F G 𝓈

  r-is-homomorphism : is-a-frame-homomorphism G F r holds
  r-is-homomorphism = fun-is-a-frame-homomorphism G F 𝓇

  field
   𝓇-cancels-𝓈 : r ∘ s ∼ id
   𝓈-cancels-𝓇 : s ∘ r ∼ id

\end{code}

We now show the equivalence of this to a Σ-based definition.

Given a frame homomorphism `F ─f→ G`, its type of homomorphic inverses is a
proposition.

\begin{code}

 homomorphic-inverse : (F ─f→ G) → 𝓤 ⊔ 𝓤' ⊔ 𝓥 ⊔ 𝓦 ⁺  ̇
 homomorphic-inverse s =
  Σ r ꞉ (G ─f→ F) , fun F G s ∘ fun G F r ∼ id
                  × fun G F r ∘ fun F G s ∼ id

 homomorphic-inverse-is-prop : (h : F ─f→ G) → is-prop (homomorphic-inverse h)
 homomorphic-inverse-is-prop h (r , φ , ψ) (r′ , φ′ , ψ′) =
  to-subtype-＝ † (to-frame-homomorphism-＝ G F r r′ ‡)
   where
    † : (h′ : G ─f→ F)
      → is-prop (fun F G h ∘ fun G F h′ ∼ id × fun G F h′ ∘ fun F G h ∼ id)
    † h′ = ×-is-prop
            (Π-is-prop fe (λ _ → carrier-of-[ poset-of G ]-is-set))
            (Π-is-prop fe (λ _ → carrier-of-[ poset-of F ]-is-set))

    ϑ : fun F G h ∘ fun G F r ∼ fun F G h ∘ fun G F r′
    ϑ y = fun F G h (fun G F r y)   ＝⟨ Ⅰ ⟩
          y                         ＝⟨ Ⅱ ⟩
          fun F G h (fun G F r′ y)  ∎
           where
            Ⅰ = φ y
            Ⅱ = φ′ y ⁻¹

    ξ : left-cancellable (fun F G h)
    ξ = sections-are-lc (fun F G h) (fun G F r , ψ)

    ‡ : (y : ⟨ G ⟩) → fun G F r y ＝ fun G F r′ y
    ‡ y = ξ (ϑ y)

\end{code}

To say that a frame homomorphism is an isomorphism is to say that its type
of homomorphic inverses is inhabited.

\begin{code}

 is-isomorphism : (F ─f→ G) → Ω (𝓤 ⊔ 𝓤' ⊔ 𝓥 ⊔ 𝓦 ⁺)
 is-isomorphism h = homomorphic-inverse h , homomorphic-inverse-is-prop h

\end{code}

We define the type of isomorphisms between frames `F` and `G` accordingly.

\begin{code}

 Isomorphism : 𝓤 ⊔ 𝓤' ⊔ 𝓥 ⊔ 𝓥' ⊔ 𝓦 ⁺  ̇
 Isomorphism = Σ h ꞉ F ─f→ G , is-isomorphism h holds

\end{code}

It is immediate that `Isomorphism` and `Isomorphismᵣ` are equivalent types.

\begin{code}

 isomorphism-to-isomorphismᵣ : Isomorphism → Isomorphismᵣ
 isomorphism-to-isomorphismᵣ (𝓈 , 𝓇 , φ , ψ) =
  record
   { 𝓈           = 𝓈
   ; 𝓇           = 𝓇
   ; 𝓇-cancels-𝓈 = ψ
   ; 𝓈-cancels-𝓇 = φ
   }

 isomorphismᵣ-to-isomorphism : Isomorphismᵣ → Isomorphism
 isomorphismᵣ-to-isomorphism iso =
  let
   open Isomorphismᵣ iso
  in
   𝓈 , 𝓇 , 𝓈-cancels-𝓇 , 𝓇-cancels-𝓈

 isomorphism-equiv-to-isomorphismᵣ : Isomorphism ≃ Isomorphismᵣ
 isomorphism-equiv-to-isomorphismᵣ = isomorphism-to-isomorphismᵣ
                                   , (isomorphismᵣ-to-isomorphism , λ _ → refl)
                                   , (isomorphismᵣ-to-isomorphism , λ _ → refl)

\end{code}

We now give an alternative definition of the same notion, which is more
convenient to use for the SIP.

The predicate `is-homomorphic` below expresses what it means for an equivalence
between the carrier sets of `F` and `G` to be homomorphic.

\begin{code}

 is-homomorphic : (⟨ F ⟩ ≃ ⟨ G ⟩) → Ω (𝓤 ⊔ 𝓥 ⊔ 𝓤' ⊔ 𝓥' ⊔ 𝓦 ⁺)
 is-homomorphic e = is-a-frame-homomorphism F G ⌜ e ⌝
                  ∧ is-a-frame-homomorphism G F (e⁻¹ (⌜⌝-is-equiv e))
  where
   e⁻¹ = inverse ⌜ e ⌝

\end{code}

The type of isomorphisms between `F` and `G` could alternatively be defined
as the type of homomorphic equivalences.

\begin{code}

 Isomorphism₀ : 𝓤 ⊔ 𝓤' ⊔ 𝓥 ⊔ 𝓥' ⊔ 𝓦 ⁺  ̇
 Isomorphism₀ = Σ e ꞉ ⟨ F ⟩ ≃ ⟨ G ⟩ , is-homomorphic e holds

\end{code}

These two notions of frame isomorphism are equivalent.

\begin{code}

 isomorphismᵣ-to-isomorphism₀ : Isomorphismᵣ → Isomorphism₀
 isomorphismᵣ-to-isomorphism₀ iso = (s , † , ‡) , φ , ψ
  where
   open Isomorphismᵣ iso

   † : has-section s
   † = r , 𝓈-cancels-𝓇

   ‡ : is-section s
   ‡ = r , 𝓇-cancels-𝓈

   φ : is-a-frame-homomorphism F G s holds
   φ = fun-is-a-frame-homomorphism F G 𝓈

   ψ : is-a-frame-homomorphism G F r holds
   ψ = fun-is-a-frame-homomorphism G F 𝓇

 isomorphism₀-to-isomorphismᵣ : Isomorphism₀ → Isomorphismᵣ
 isomorphism₀-to-isomorphismᵣ (e , φ , ψ)  =
  record
   { 𝓈           = ⌜ e ⌝ , φ
   ; 𝓇           = inverse ⌜ e ⌝ (⌜⌝-is-equiv e) , ψ
   ; 𝓇-cancels-𝓈 = inverses-are-retractions ⌜ e ⌝ (⌜⌝-is-equiv e)
   ; 𝓈-cancels-𝓇 = inverses-are-sections ⌜ e ⌝ (⌜⌝-is-equiv e)
   }

 isomorphism-to-isomorphism₀ : Isomorphism → Isomorphism₀
 isomorphism-to-isomorphism₀ =
  isomorphismᵣ-to-isomorphism₀ ∘ isomorphism-to-isomorphismᵣ

 isomorphism₀-to-isomorphism : Isomorphism₀ → Isomorphism
 isomorphism₀-to-isomorphism =
  isomorphismᵣ-to-isomorphism ∘ isomorphism₀-to-isomorphismᵣ

 isomorphism-equivalent-to-isomorphism₀ : Isomorphism ≃ Isomorphism₀
 isomorphism-equivalent-to-isomorphism₀ = isomorphism-to-isomorphism₀
                                        , (isomorphism₀-to-isomorphism , †)
                                        , (isomorphism₀-to-isomorphism , ‡)
  where
   † : isomorphism-to-isomorphism₀ ∘ isomorphism₀-to-isomorphism ∼ id
   † (h , _) =
    to-subtype-＝
     (holds-is-prop ∘ is-homomorphic)
     (to-subtype-＝ (being-equiv-is-prop (λ 𝓤 𝓥 → fe {𝓤} {𝓥})) refl)

   ‡ : isomorphism₀-to-isomorphism ∘ isomorphism-to-isomorphism₀ ∼ id
   ‡ iso = to-subtype-＝ (holds-is-prop ∘ is-isomorphism) refl

 isomorphismᵣ-equivalent-to-isomorphism₀ : Isomorphismᵣ ≃ Isomorphism₀
 isomorphismᵣ-equivalent-to-isomorphism₀ =
  Isomorphismᵣ   ≃⟨ Ⅰ ⟩
  Isomorphism    ≃⟨ Ⅱ ⟩
  Isomorphism₀   ■
   where
    Ⅰ = ≃-sym isomorphism-equiv-to-isomorphismᵣ
    Ⅱ = isomorphism-equivalent-to-isomorphism₀

\end{code}

Some nice syntax for frame isomorphisms.

\begin{code}

Isomorphismᵣ-Syntax : Frame 𝓤 𝓥 𝓦 → Frame 𝓤' 𝓥' 𝓦 → 𝓤 ⊔ 𝓤' ⊔ 𝓥 ⊔ 𝓥' ⊔ 𝓦 ⁺  ̇
Isomorphismᵣ-Syntax = FrameIsomorphisms.Isomorphismᵣ

infix 0 Isomorphismᵣ-Syntax
syntax Isomorphismᵣ-Syntax F G = F ≅f≅ G

\end{code}

Added on 2024-04-14.

We denote by `𝔦𝔡` the identity equivalence on the carrier set of a frame.

\begin{code}

𝔦𝔡 : (L : Frame 𝓤 𝓥 𝓦) → ⟨ L ⟩ ≃ ⟨ L ⟩
𝔦𝔡 L = ≃-refl ⟨ L ⟩

\end{code}

The proof that `𝔦𝔡` preserves the top element and meets is definitional.

\begin{code}

𝔦𝔡-preserves-top : (L : Frame 𝓤 𝓥 𝓦) → preserves-top L L ⌜ 𝔦𝔡 L ⌝ holds
𝔦𝔡-preserves-top L = refl

𝔦𝔡-preserves-binary-meets : (L : Frame 𝓤 𝓥 𝓦)
                          → preserves-binary-meets L L ⌜ 𝔦𝔡 L ⌝ holds
𝔦𝔡-preserves-binary-meets _ _ _ = refl

\end{code}

The fact that it preserves joins is also direct.

\begin{code}

𝔦𝔡-preserves-joins : (L : Frame 𝓤 𝓥 𝓦) → preserves-joins L L ⌜ 𝔦𝔡 L ⌝ holds
𝔦𝔡-preserves-joins L S = † , ‡
 where
  open Joins (λ x y → x ≤[ poset-of L ] y)

  † : ((⋁[ L ] S) is-an-upper-bound-of S) holds
  † = ⋁[ L ]-upper S

  ‡ : ((u , _) : upper-bound S) → ((⋁[ L ] S) ≤[ poset-of L ] u) holds
  ‡ = ⋁[ L ]-least S

\end{code}

We package these up together into the proof `𝔦𝔡-is-frame-homomorphism`,
and denote this frame homomorphism by `𝔦𝔡ₕ`.

\begin{code}

𝔦𝔡-is-frame-homomorphism : (L : Frame 𝓤 𝓥 𝓦)
                         → is-a-frame-homomorphism L L ⌜ 𝔦𝔡 L ⌝ holds
𝔦𝔡-is-frame-homomorphism L = 𝔦𝔡-preserves-top L
                           , 𝔦𝔡-preserves-binary-meets L
                           , 𝔦𝔡-preserves-joins L

𝔦𝔡ₕ : (L : Frame 𝓤 𝓥 𝓦) → L ─f·→ L
𝔦𝔡ₕ L =
 frame-homomorphism-to-frame-homomorphismᵣ
  L
  L
  (⌜ 𝔦𝔡 L ⌝ , 𝔦𝔡-is-frame-homomorphism L)

\end{code}

Finally, we record the fact that the identity equivalence is a homomorphic
equivalence.

\begin{code}

𝔦𝔡-is-homomorphic : (L : Frame 𝓤 𝓥 𝓦)
                  → FrameIsomorphisms.is-homomorphic L L (𝔦𝔡 L) holds
𝔦𝔡-is-homomorphic L =
 𝔦𝔡-is-frame-homomorphism L , 𝔦𝔡-is-frame-homomorphism L

\end{code}
