---
title: Morphism of formal topologies
author: Ayberk Tosun
date-started: 2026-08-25
date-completed: 2026-08-27
---

This module defines morphisms between formal topologies as well as quasi formal
topologies, following [1] as a reference.

\begin{code}

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

open import UF.FunExt
open import UF.PropTrunc
open import UF.Subsingletons

module Locales.FormalTopology.Morphism
        (pt : propositional-truncations-exist)
        (fe : Fun-Ext)
        (pe : Prop-Ext)
       where

open import Locales.FormalTopology.Definition pt fe
open import Locales.Frame pt fe hiding (⟨_⟩)
open import MLTT.Spartan
open import Notation.CanonicalMap
open import Notation.UnderlyingType
open import UF.Logic
open import UF.Powerset
open import UF.Sets
open import UF.Sets-Properties
open import UF.SubtypeClassifier

open AllCombinators pt fe
open PropositionalTruncation pt

\end{code}

\section{Preliminaries}

Given a subset `U : π“Ÿ A` and a function `f : A β†’ π“Ÿ B`, the type
`relational-image f U` denotes the union `⋃_{u ∈ U} f u`.

\begin{code}

relational-image : {A B : 𝓀 Μ‡} β†’ (A β†’ π“Ÿ B) β†’ π“Ÿ A β†’ π“Ÿ B
relational-image {𝓀} {A} {B} f U = ⋃ {𝕋 U} Ξ» { (a , _) β†’ f a }
 where
  open unions-of-small-families pt 𝓀 𝓀 B

\end{code}

We define the syntax `f β¦… U ⦆` for the image of a relation over a subset `U`.

\begin{code}

relational-image-syntax : {A B : 𝓀 Μ‡} β†’ (A β†’ π“Ÿ B) β†’ π“Ÿ A β†’ π“Ÿ B
relational-image-syntax f U = relational-image f U

infix 25 relational-image-syntax
syntax relational-image-syntax f U = f β¦… U ⦆

\end{code}

\section{Morphisms of quasi formal topologies}

\begin{code}

module Quasi-Formal-Topology-Morphism
        {𝓀 : Universe}
        (π’œ : Quasi-Formal-Topology 𝓀)
        (ℬ : Quasi-Formal-Topology 𝓀)
       where

 private
  A = ⟨ π’œ ⟩
  B = ⟨ ℬ ⟩

\end{code}

Negri [1] defines a quasi formal topology morphism as a relation (1) preserving
the top subset, and (2) preserving the covering relation.

\begin{code}

 preserves-top : (A β†’ π“Ÿ B) β†’ Ξ© 𝓀
 preserves-top f = full ◁Q⁺[ ℬ ] f β¦… full ⦆

 preserves-covering : (A β†’ π“Ÿ B) β†’ Ξ© (𝓀 ⁺)
 preserves-covering f =
  β±― a κž‰ A , β±― U κž‰ π“Ÿ A , a ◁Q[ π’œ ] U β‡’ f a ◁Q⁺[ ℬ ] f β¦… U ⦆

 is-quasi-formal-topology-morphism : (A β†’ π“Ÿ B) β†’ Ξ© (𝓀 ⁺)
 is-quasi-formal-topology-morphism f = preserves-top f ∧ preserves-covering f

\end{code}

Using this, we write down the type of quasi formal topology morphisms between
quasi formal topologies `π’œ` and `ℬ`.

\begin{code}

 _─qftβ†’_ : 𝓀 ⁺  Μ‡
 _─qftβ†’_ = Ξ£ f κž‰ (A β†’ π“Ÿ B) , is-quasi-formal-topology-morphism f holds

 infix 0 _─qftβ†’_

\end{code}

We denote by `fun 𝒻` the underlying function of a quasi formal topology
morphism `𝒻`.

\begin{code}

 fun : _─qftβ†’_ β†’ A β†’ π“Ÿ B
 fun (f , _) = f

 instance
  canonical-map-quasi-formal-topology-morphism-function
   : Canonical-Map _─qftβ†’_ (A β†’ π“Ÿ B)
  ΞΉ {{canonical-map-quasi-formal-topology-morphism-function}} = fun

\end{code}

We now define named projections for the `_─qftβ†’_` type.

\begin{code}

 fun-is-quasi-formal-topology-morphism
  : (𝒻 : _─qftβ†’_)
  β†’ is-quasi-formal-topology-morphism [ 𝒻 ] holds
 fun-is-quasi-formal-topology-morphism (_ , Ο†) = Ο†

 fun-preserves-top : (𝒻 : _─qftβ†’_) β†’ preserves-top [ 𝒻 ] holds
 fun-preserves-top (_ , Ο† , _) = Ο†

 fun-preserves-covering : (𝒻 : _─qftβ†’_) β†’ preserves-covering [ 𝒻 ] holds
 fun-preserves-covering (_ , _ , ψ) = ψ

 fun-preserves-covering-plus
  : (𝒻 : _─qftβ†’_)
  β†’ (β±― U V κž‰ π“Ÿ ⟨ π’œ ⟩ , U ◁Q⁺[ π’œ ] V β‡’ [ 𝒻 ] β¦… U ⦆ ◁Q⁺[ ℬ ] [ 𝒻 ] β¦… V ⦆) holds
 fun-preserves-covering-plus 𝒻 U V p b h =
  βˆ₯βˆ₯-rec (holds-is-prop (b βˆˆβ‚š (Ξ» - β†’ - ◁Q[ ℬ ] ([ 𝒻 ] β¦… V ⦆)))) † h
   where
    f = [ 𝒻 ]

    † : Ξ£ (a , _) κž‰ 𝕋 U , b ∈ f a β†’ b ∈ (Ξ» - β†’ - ◁Q[ ℬ ] f β¦… V ⦆)
    † ((a , ΞΌ) , q) = b         β—βŸ¨  β…  ⟩
                      f a       β—βΊβŸ¨ β…‘ ⟩
                      f β¦… V ⦆   β– 
     where
      open Quasi-Cover-Reasoning ℬ

      β…‘ : (f a ◁Q⁺[ ℬ ] f β¦… V ⦆) holds
      β…‘ = fun-preserves-covering 𝒻 a V (p a ΞΌ)

      β…  : (b ◁Q[ ℬ ] f a) holds
      β…  = reflexivity-of-quasi-cover ℬ b (f a) q

\end{code}

The lemma below states that the extensional equality of the underlying function
is sufficient to establish the equality of two quasi formal topology morphisms.

\begin{code}

 to-quasi-formal-topology-morphism-＝
  : (𝒻 β„Š : _─qftβ†’_)
  β†’ [ 𝒻 ] ∼ [ β„Š ]
  β†’ 𝒻 ＝ β„Š
 to-quasi-formal-topology-morphism-＝ 𝒻 β„Š = to-subtype-＝ † ∘ dfunext fe
  where
   † : (f : A β†’ π“Ÿ B)
     β†’ is-prop (is-quasi-formal-topology-morphism f holds)
   † f = holds-is-prop (is-quasi-formal-topology-morphism f)

\end{code}

The type of quasi formal topology morphisms is a set.

\begin{code}

 _─qftβ†’_-is-set : is-set _─qftβ†’_
 _─qftβ†’_-is-set =
  subsets-of-sets-are-sets
   (A β†’ π“Ÿ B)
   (_holds ∘ is-quasi-formal-topology-morphism)
   (Ξ -is-set fe (Ξ» _ β†’ π“Ÿ-is-set' fe pe))
   (Ξ» {f} β†’ holds-is-prop (is-quasi-formal-topology-morphism f))

\end{code}

\section{Morphisms of formal topologies}

We now define the notion of formal topology morphism, following Definition 2.4
of [1]. A formal topology morphism is a quasi formal topology morphism that
additionally preserves binary meets in the sense of Condition 2 from [1].

\begin{code}

module Formal-Topology-Morphism
        (π’œ : Formal-Topology 𝓀)
        (ℬ : Formal-Topology 𝓀)
       where

 private
  A = ⟨ π’œ ⟩
  B = ⟨ ℬ ⟩

  π’œβ‚€ : Quasi-Formal-Topology 𝓀
  π’œβ‚€ = underlying-quasi-formal-topology π’œ

  ℬ₀ : Quasi-Formal-Topology 𝓀
  ℬ₀ = underlying-quasi-formal-topology ℬ

 open Downward-Closure-Intersection-Syntax (Ξ» a b β†’ a βŠ‘[ ℬ ] b)
  renaming (_βŠ“_ to _βŠ“β„¬_)
 open Quasi-Formal-Topology-Morphism π’œβ‚€ ℬ₀

\end{code}

We denote by `lower-bounds a b` the set of lower bounds for `a` and `b`.

\begin{code}

 lower-bounds : ⟨ π’œ ⟩ β†’ ⟨ π’œ ⟩ β†’ π“Ÿ ⟨ π’œ ⟩
 lower-bounds a b = Ξ» c β†’ (c βŠ‘[ π’œ ] a) ∧ (c βŠ‘[ π’œ ] b)

\end{code}

A function `f : ⟨ π’œ ⟩ β†’ π“Ÿ ⟨ ℬ ⟩` is said to _preserve binary meets_
if `f β¦… lower-bounds a₁ aβ‚‚ ⦆` covers `f a₁ βŠ“ f aβ‚‚` for every pair of elements
`a₁ aβ‚‚ : ⟨ π’œ ⟩`.

\begin{code}

 preserves-binary-meets : (⟨ π’œ ⟩ β†’ π“Ÿ ⟨ ℬ ⟩) β†’ Ξ© 𝓀
 preserves-binary-meets f =
  β±― a₁ aβ‚‚ κž‰ ⟨ π’œ ⟩ , (f a₁ βŠ“β„¬ f aβ‚‚) ◁⁺[ ℬ ] f β¦… lower-bounds a₁ aβ‚‚ ⦆

\end{code}

A formal topology morphism is a function `f : ⟨ π’œ ⟩ β†’ π“Ÿ ⟨ ℬ ⟩` that

  1. preserves the top subset,
  2. preserves binary meets, and
  3. preserves the covering relation.

\begin{code}

 is-formal-topology-morphism : (A β†’ π“Ÿ B) β†’ Ξ© (𝓀 ⁺)
 is-formal-topology-morphism f =
  preserves-top f ∧ preserves-binary-meets f ∧ preserves-covering f

\end{code}

Using this, we write down the type of formal topology morphisms between the
formal topologies `π’œ` and `ℬ` and then define the named projections.

\begin{code}

 _─ftβ†’_ : 𝓀 ⁺  Μ‡
 _─ftβ†’_ = Ξ£ f κž‰ (A β†’ π“Ÿ B) , is-formal-topology-morphism f holds

 infix 0 _─ftβ†’_

 ft-fun : _─ftβ†’_ β†’ A β†’ π“Ÿ B
 ft-fun (f , _) = f

 instance
  canonical-map-formal-topology-morphism-function
   : Canonical-Map _─ftβ†’_ (A β†’ π“Ÿ B)
  ΞΉ {{canonical-map-formal-topology-morphism-function}} = ft-fun

 fun-is-formal-topology-morphism
  : (𝒻 : _─ftβ†’_)
  β†’ is-formal-topology-morphism [ 𝒻 ] holds
 fun-is-formal-topology-morphism (_ , Ο†) = Ο†

 ft-fun-preserves-top : (𝒻 : _─ftβ†’_) β†’ preserves-top [ 𝒻 ] holds
 ft-fun-preserves-top (_ , Ο† , _) = Ο†

 ft-fun-preserves-binary-meets : (𝒻 : _─ftβ†’_) β†’ preserves-binary-meets [ 𝒻 ] holds
 ft-fun-preserves-binary-meets (_ , _ , ψ , _) = ψ

 ft-fun-preserves-covering : (𝒻 : _─ftβ†’_) β†’ preserves-covering [ 𝒻 ] holds
 ft-fun-preserves-covering (_ , _ , _ , Ο‡) = Ο‡

\end{code}

Every formal topology morphism is a quasi formal topology morphism when
Condition (2) is dropped.

\begin{code}

 to-qft-morphism : _─ftβ†’_ β†’ _─qftβ†’_
 to-qft-morphism (f , Ο† , _ , Ο‡) = f , Ο† , Ο‡

 from-qft-morphism : (𝒻 : _─qftβ†’_) β†’ preserves-binary-meets [ 𝒻 ] holds β†’ _─ftβ†’_
 from-qft-morphism 𝒻@(f , Ξ² , Ξ΄) Ξ³ =  f , Ξ² , Ξ³ , Ξ΄

\end{code}

We now prove the analogue of `to-quasi-formal-topology-morphism-＝` for formal
topologies.

\begin{code}

 to-formal-topology-morphism-＝
  : (𝒻 β„Š : _─ftβ†’_)
  β†’ [ 𝒻 ] ∼ [ β„Š ]
  β†’ 𝒻 ＝ β„Š
 to-formal-topology-morphism-＝ 𝒻 β„Š = to-subtype-＝ † ∘ dfunext fe
  where
   † : (f : A β†’ π“Ÿ B) β†’ is-prop (is-formal-topology-morphism f holds)
   † f = holds-is-prop (is-formal-topology-morphism f)

\end{code}

The type of formal topology morphisms is a set.

\begin{code}

 _─ftβ†’_-is-set : is-set _─ftβ†’_
 _─ftβ†’_-is-set =
  subsets-of-sets-are-sets
   (A β†’ π“Ÿ B)
   (_holds ∘ is-formal-topology-morphism)
   (Ξ -is-set fe (Ξ» _ β†’ π“Ÿ-is-set' fe pe))
   (Ξ» {f} β†’ holds-is-prop (is-formal-topology-morphism f))

\end{code}

\section{Identity morphisms}

In this section, we define the identity morphisms on formal and quasi formal
topologies.

\begin{code}

open Quasi-Formal-Topology-Morphism hiding (preserves-top; preserves-covering)

identity-morphism-qft : (π’œ : Quasi-Formal-Topology 𝓀) β†’ π’œ ─qftβ†’ π’œ
identity-morphism-qft π’œ = (Ξ» a β†’ ❴ a ❡) , Ξ² , Ξ³
 where
  open singleton-subsets (carrier-of-quasi-formal-topology-is-set π’œ)
  open Quasi-Formal-Topology-Morphism π’œ π’œ

  Ξ² : preserves-top (Ξ» - β†’ ❴ - ❡) holds
  Ξ² a ⋆ = reflexivity-of-quasi-cover π’œ a (❴_❡ β¦… full ⦆) ∣ (a , ⋆) , refl ∣

  singleton-image-lemma : (U : π“Ÿ ⟨ π’œ ⟩) β†’ ((Ξ» - β†’ ❴ - ❡) β¦… U ⦆) ＝ U
  singleton-image-lemma U = subset-extensionality pe fe β…  β…‘
   where
    β…  : (❴_❡ β¦… U ⦆) βŠ† U
    β…  a p = βˆ₯βˆ₯-rec (holds-is-prop (a βˆˆβ‚š U)) † p
     where
      † : _
      † ((b , h) , q) = transport (Ξ» - β†’ - ∈ U) q h

    β…‘ : U βŠ† (❴_❡ β¦… U ⦆)
    β…‘ a p = ∣ (a , p) , refl ∣

  Ξ³ : preserves-covering (Ξ» - β†’ ❴ - ❡) holds
  Ξ³ a U p =
   transport (Ξ» V β†’ (❴ a ❡ ◁Q⁺[ π’œ ] V) holds) (singleton-image-lemma U ⁻¹) †
    where
     † : (❴ a ❡ ◁Q⁺[ π’œ ] U) holds
     † b q = transport (Ξ» - β†’ cover-of-quasi-formal-topology π’œ - U holds) q p

open Formal-Topology-Morphism

identity-morphism-ft : (π’œ : Formal-Topology 𝓀) β†’ π’œ ─ftβ†’ π’œ
identity-morphism-ft π’œ = from-qft-morphism π’œ π’œ (identity-morphism-qft π’œβ‚€) Ξ²
 where
  π’œβ‚€ = underlying-quasi-formal-topology π’œ
  P  = underlying-poset-of-formal-topology π’œ

  open singleton-subsets (carrier-of-quasi-formal-topology-is-set π’œβ‚€)

  Ξ² : preserves-binary-meets π’œ π’œ (fun π’œβ‚€ π’œβ‚€ (identity-morphism-qft π’œβ‚€)) holds
  Ξ² a₁ aβ‚‚ a (p₁ , pβ‚‚) = βˆ₯βˆ₯-recβ‚‚ (holds-is-prop (a ◁Q[ π’œβ‚€ ] _)) Ξ³ p₁ pβ‚‚
   where
    Ξ³ : Ξ£ a₁′ κž‰ ⟨ π’œ ⟩ , (a₁ ＝ a₁′) Γ— (a ≀[ P ] a₁′) holds
      β†’ Ξ£ aβ‚‚β€² κž‰ ⟨ π’œ ⟩ , (aβ‚‚ ＝ aβ‚‚β€²) Γ— (a ≀[ P ] aβ‚‚β€²) holds
      β†’ (a ◁[ π’œ ] ❴_❡ β¦… lower-bounds π’œ π’œ a₁ aβ‚‚ ⦆) holds
    Ξ³ (a₁′ , r₁ , q₁) (aβ‚‚β€² , rβ‚‚ , qβ‚‚) =
     reflexivity-of-quasi-cover π’œβ‚€ a _ ∣ (a , β…  , β…‘) , refl ∣
      where
       open PosetReasoning P

       β…  : (a ≀[ P ] a₁) holds
       β…  = a β‰€βŸ¨ q₁ ⟩ a₁′ ＝⟨ r₁ ⁻¹ βŸ©β‚š a₁ β– 

       β…‘ : (a ≀[ P ] aβ‚‚) holds
       β…‘ = a β‰€βŸ¨ qβ‚‚ ⟩ aβ‚‚β€² ＝⟨ rβ‚‚ ⁻¹ βŸ©β‚š aβ‚‚ β– 

\end{code}

\section{Bibliography}

[1]: Sara Negri. _Continuous domains as formal spaces_. Mathematical Structures
     in Computer Science, Volume 12, No. 1, pp. 19–52, 2002.
     DOI:10.1017/S0960129501003450