---
title: Category of formal topologies
author: Ayberk Tosun
date-started: 2026-08-27
date-completed: 2026-09-02
---

This module defines the category of formal topologies as well as that of 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.Category
        (pt : propositional-truncations-exist)
        (fe : Fun-Ext)
        (pe : Prop-Ext)
       where

open import Categories.Pre
open import Categories.Wild
open import Locales.FormalTopology.Definition pt fe
open import Locales.FormalTopology.Morphism pt fe pe
open import Locales.Frame pt fe hiding (⟨_⟩)
open import MLTT.Spartan
open import Notation.CanonicalMap
open import Notation.UnderlyingType
open import UF.Base
open import UF.Powerset
open import UF.SubtypeClassifier

open Formal-Topology-Morphism
open Quasi-Formal-Topology-Morphism

\end{code}

\section{Preliminaries}

We first prove a lemma establishing that `relational-image` commutes with
composition.

\begin{code}

open PropositionalTruncation pt

relational-image-commutes-with-composition
 : {A B C : 𝓀  Μ‡}
 β†’ (f : A β†’ π“Ÿ B)
 β†’ (g : B β†’ π“Ÿ C)
 β†’ (U : π“Ÿ A)
 β†’ g β¦… f β¦… U ⦆ ⦆ ＝ (Ξ» - β†’ g β¦… f - ⦆) β¦… U ⦆
relational-image-commutes-with-composition f g U =
 subset-extensionality pe fe † ‑
  where
   † : g β¦… f β¦… U ⦆ ⦆ βŠ† (Ξ» - β†’ g β¦… f - ⦆) β¦… U ⦆
   † c = βˆ₯βˆ₯-rec (holds-is-prop (c βˆˆβ‚š ((Ξ» - β†’ g β¦… f - ⦆) β¦… U ⦆))) β… 
    where
     β…  : Ξ£ (b , _) κž‰ 𝕋 (f β¦… U ⦆) , c ∈ g b β†’ c ∈ ((Ξ» - β†’ g β¦… f - ⦆) β¦… U ⦆)
     β…  ((b , h) , p) =
      βˆ₯βˆ₯-rec (holds-is-prop (c βˆˆβ‚š ((Ξ» - β†’ g β¦… f - ⦆) β¦… U ⦆))) β…‘ h
       where
        β…‘ : (Ξ£ (a , _) κž‰ 𝕋 U , b ∈ f a) β†’ c ∈ ((Ξ» - β†’ g β¦… f - ⦆) β¦… U ⦆)
        β…‘ ((a , ΞΌ) , q) = ∣ (a , ΞΌ) , β…’ ∣
         where
          β…’ : c ∈ (g β¦… f a ⦆)
          β…’ = ∣ (b , q) , p ∣

   ‑ : (Ξ» - β†’ g β¦… f - ⦆) β¦… U ⦆ βŠ† g β¦… f β¦… U ⦆ ⦆
   ‑ c = βˆ₯βˆ₯-rec (holds-is-prop (c βˆˆβ‚š (g β¦… f β¦… U ⦆ ⦆))) β… 
    where
     β…  : Ξ£ (a , _) κž‰ 𝕋 U , c ∈ (g β¦… f a ⦆) β†’ c ∈ (g β¦… f β¦… U ⦆ ⦆)
     β…  ((a , p) , h) = βˆ₯βˆ₯-rec (holds-is-prop (c βˆˆβ‚š (g β¦… f β¦… U ⦆ ⦆))) β…‘ h
      where
       β…‘ : Ξ£ (b , _) κž‰ 𝕋 (f a) , c ∈ g b β†’ c ∈ (g β¦… f β¦… U ⦆ ⦆)
       β…‘ ((b , q) , hβ€²) = ∣ (b , ∣ (a , p) , q ∣) , hβ€² ∣

\end{code}

\section{Category of quasi formal topologies}

We start by defining composition of quasi formal topology morphisms.

\begin{code}

qftop-composition
 : (π’œ ℬ π’ž : Quasi-Formal-Topology 𝓀)
 β†’ (ℬ ─qftβ†’ π’ž)
 β†’ (π’œ ─qftβ†’ ℬ)
 β†’ (π’œ ─qftβ†’ π’ž)
qftop-composition π’œ ℬ π’ž β„Š 𝒻 = h , h-preserves-top , h-preserves-covering
 where
  f = fun π’œ ℬ 𝒻
  g = fun ℬ π’ž β„Š

  h : ⟨ π’œ ⟩ β†’ π“Ÿ ⟨ π’ž ⟩
  h = Ξ» - β†’ g β¦… f - ⦆

  h-preserves-top : (full ◁Q⁺[ π’ž ] h β¦… full ⦆) holds
  h-preserves-top = β…€
   where
    β…  : (full ◁Q⁺[ ℬ ] f β¦… full ⦆) holds
    β…  = fun-preserves-top π’œ ℬ 𝒻

    β…‘ : (full ◁Q⁺[ π’ž ] g β¦… full ⦆) holds
    β…‘ = fun-preserves-top ℬ π’ž β„Š

    β…’ : (g β¦… full ⦆ ◁Q⁺[ π’ž ] g β¦… f β¦… full ⦆ ⦆) holds
    β…’ = fun-preserves-covering-plus ℬ π’ž β„Š full (f β¦… full ⦆) β… 

    β…£ : (full ◁Q⁺[ π’ž ] g β¦… f β¦… full ⦆ ⦆) holds
    β…£ = transitivity-of-quasi-cover-plus π’ž full _ _ β…‘ β…’

    β…€ : (full ◁Q⁺[ π’ž ] h β¦… full ⦆) holds
    β…€ = transport
         (Ξ» - β†’ (full ◁Q⁺[ π’ž ] -) holds)
         (relational-image-commutes-with-composition f g full)
         β…£

  h-preserves-covering
   : preserves-covering π’œ π’ž h holds
  h-preserves-covering a U ΞΊ = β…’
   where
    β…  : (f a ◁Q⁺[ ℬ ] f β¦… U ⦆) holds
    β…  = fun-preserves-covering π’œ ℬ 𝒻 a U ΞΊ

    β…‘ : (g β¦… f a ⦆ ◁Q⁺[ π’ž ] g β¦… f β¦… U ⦆ ⦆) holds
    β…‘ = fun-preserves-covering-plus ℬ π’ž β„Š (f a) (f β¦… U ⦆) β… 

    β…’ : (g β¦… f a ⦆ ◁Q⁺[ π’ž ] h β¦… U ⦆) holds
    β…’ = transport
         (Ξ» - β†’ (g β¦… f a ⦆ ◁Q⁺[ π’ž ] -) holds)
         (relational-image-commutes-with-composition f g U)
         β…‘

\end{code}

The identity morphism is neutral for composition.

\begin{code}

id-qftop-is-left-neutral
 : (π’œ ℬ : Quasi-Formal-Topology 𝓀)
 β†’ (𝒻 : π’œ ─qftβ†’ ℬ)
 β†’ qftop-composition π’œ ℬ ℬ (identity-morphism-qft ℬ) 𝒻 ＝ 𝒻
id-qftop-is-left-neutral π’œ ℬ 𝒻 =
 to-quasi-formal-topology-morphism-＝
  π’œ
  ℬ
  (qftop-composition π’œ ℬ ℬ (identity-morphism-qft ℬ) 𝒻)
  𝒻
  †
  where
   open singleton-subsets (carrier-of-quasi-formal-topology-is-set ℬ)

   f = fun π’œ ℬ 𝒻

   † : (a : ⟨ π’œ ⟩) β†’ (Ξ» - β†’ ❴ - ❡) β¦… f a ⦆ ＝ f a
   † a = subset-extensionality pe fe β…  β…‘
    where
     β…  : ❴_❡ β¦… f a ⦆ βŠ† f a
     β…  b = βˆ₯βˆ₯-rec (holds-is-prop (b βˆˆβ‚š f a)) ‑
      where
       ‑ : (Ξ£ (aβ€² , _) κž‰ 𝕋 (f a) , b ∈ ❴ aβ€² ❡) β†’ b ∈ f a
       ‑ ((aβ€² , p) , h) = transport (Ξ» - β†’ - ∈ f a) h p

     β…‘ : f a βŠ† ❴_❡ β¦… f a ⦆
     β…‘ b ΞΌ = ∣ (b , ΞΌ) , refl ∣

id-qftop-is-right-neutral
 : (π’œ ℬ : Quasi-Formal-Topology 𝓀)
 β†’ (𝒻 : π’œ ─qftβ†’ ℬ)
 β†’ qftop-composition π’œ π’œ ℬ 𝒻 (identity-morphism-qft π’œ) ＝ 𝒻
id-qftop-is-right-neutral π’œ ℬ 𝒻 =
 to-quasi-formal-topology-morphism-＝
  π’œ
  ℬ
  (qftop-composition π’œ π’œ ℬ 𝒻 (identity-morphism-qft π’œ))
  𝒻
  †
  where
   open singleton-subsets (carrier-of-quasi-formal-topology-is-set π’œ)

   f = fun π’œ ℬ 𝒻

   † : (a : ⟨ π’œ ⟩) β†’ f β¦… ❴ a ❡ ⦆ ＝ f a
   † a = subset-extensionality pe fe β…  β…‘ ⁻¹
    where
     β…  = Ξ» b p β†’ ∣ (a , refl) , p ∣

     β…‘ : f β¦… ❴ a ❡ ⦆ βŠ† f a
     β…‘ b = βˆ₯βˆ₯-rec (holds-is-prop (f a b)) Ξ³
      where
       Ξ³ : Ξ£ (aβ€² , _) κž‰ 𝕋 ❴ a ❡ , b ∈ f aβ€² β†’ b ∈ f a
       Ξ³ ((aβ€² , h) , q) = transport (Ξ» - β†’ b ∈ f -) (h ⁻¹) q

\end{code}

Associativity of `qftop-composition` stated with extensional equality of
functions. This follows directly from `relational-image-commutes-with-composition`.

\begin{code}

qftop-composition-is-associative-extensional
 : (π’œ ℬ π’ž π’Ÿ : Quasi-Formal-Topology 𝓀)
 β†’ (𝒻 : π’œ ─qftβ†’ ℬ)
 β†’ (β„Š : ℬ ─qftβ†’ π’ž)
 β†’ (𝒽 : π’ž ─qftβ†’ π’Ÿ)
 β†’ fun π’œ π’Ÿ (qftop-composition π’œ π’ž π’Ÿ 𝒽 (qftop-composition π’œ ℬ π’ž β„Š 𝒻))
   ∼ fun π’œ π’Ÿ (qftop-composition π’œ ℬ π’Ÿ (qftop-composition ℬ π’ž π’Ÿ 𝒽 β„Š) 𝒻)
qftop-composition-is-associative-extensional π’œ ℬ π’ž π’Ÿ 𝒻 β„Š 𝒽 =
 relational-image-commutes-with-composition g h ∘ f
  where
   f = fun π’œ ℬ 𝒻
   g = fun ℬ π’ž β„Š
   h = fun π’ž π’Ÿ 𝒽

\end{code}

Now, the actual associativity of composition for quasi formal topology
morphisms.

\begin{code}

qftop-composition-is-associative
 : (π’œ ℬ π’ž π’Ÿ : Quasi-Formal-Topology 𝓀)
 β†’ (𝒻 : π’œ ─qftβ†’ ℬ)
 β†’ (β„Š : ℬ ─qftβ†’ π’ž)
 β†’ (𝒽 : π’ž ─qftβ†’ π’Ÿ)
 β†’ qftop-composition π’œ π’ž π’Ÿ 𝒽 (qftop-composition π’œ ℬ π’ž β„Š 𝒻)
   ＝ qftop-composition π’œ ℬ π’Ÿ (qftop-composition ℬ π’ž π’Ÿ 𝒽 β„Š) 𝒻
qftop-composition-is-associative π’œ ℬ π’ž π’Ÿ 𝒻 β„Š 𝒽 =
 to-quasi-formal-topology-morphism-＝ π’œ π’Ÿ _ _ †
  where
   open Quasi-Formal-Topology-Morphism π’œ π’Ÿ
    hiding (to-quasi-formal-topology-morphism-＝; fun)

   † : [ qftop-composition π’œ π’ž π’Ÿ 𝒽 (qftop-composition π’œ ℬ π’ž β„Š 𝒻) ]
       ∼ [ qftop-composition π’œ ℬ π’Ÿ (qftop-composition ℬ π’ž π’Ÿ 𝒽 β„Š) 𝒻 ]
   † = qftop-composition-is-associative-extensional π’œ ℬ π’ž π’Ÿ 𝒻 β„Š 𝒽

\end{code}

We now have everything we need to define the precategory of quasi formal
topologies.

\begin{code}

QFTopWildCategory : (𝓀 : Universe) β†’ WildCategory (𝓀 ⁺) (𝓀 ⁺)
QFTopWildCategory 𝓀 =
 wildcategory
  (Quasi-Formal-Topology 𝓀)
  _─qftβ†’_
  (Ξ» {π’œ} β†’ identity-morphism-qft π’œ)
  (Ξ» {π’œ} {ℬ} {π’ž} β†’ qftop-composition π’œ ℬ π’ž)
  (Ξ» {π’œ} {ℬ} β†’ id-qftop-is-left-neutral π’œ ℬ)
  (Ξ» {π’œ} {ℬ} β†’ id-qftop-is-right-neutral π’œ ℬ)
  (Ξ» {π’œ} {ℬ} {π’ž} {π’Ÿ} β†’ qftop-composition-is-associative π’œ ℬ π’ž π’Ÿ)

QFTopPrecategory : (𝓀 : Universe) β†’ Precategory (𝓀 ⁺) (𝓀 ⁺)
QFTopPrecategory 𝓀 = QFTopWildCategory 𝓀 , _─qftβ†’_-is-set

\end{code}

\section{Category of formal topologies}

We define the category of formal topologies in this section, building atop the
category of quasi formal topologies.

\begin{code}

ftop-composition
 : (π’œ ℬ π’ž : Formal-Topology 𝓀)
 β†’ (ℬ ─ftβ†’ π’ž) β†’ (π’œ ─ftβ†’ ℬ) β†’ (π’œ ─ftβ†’ π’ž)
ftop-composition π’œ ℬ π’ž β„Š 𝒻 =
 from-qft-morphism π’œ π’ž (qftop-composition π’œβ‚€ ℬ₀ π’žβ‚€ β„Šβ‚€ 𝒻₀) Ξ²
  where
   π’œβ‚€ = underlying-quasi-formal-topology π’œ
   ℬ₀ = underlying-quasi-formal-topology ℬ
   π’žβ‚€ = underlying-quasi-formal-topology π’ž
   R  = underlying-poset-of-formal-topology π’ž

   𝒻₀ = to-qft-morphism π’œ ℬ 𝒻
   β„Šβ‚€ = to-qft-morphism ℬ π’ž β„Š

   f = ft-fun π’œ ℬ 𝒻
   g = ft-fun ℬ π’ž β„Š

   open Downward-Closure-Intersection-Syntax (Ξ» x y β†’ x βŠ‘[ ℬ ] y)
    renaming (_βŠ“_ to _βŠ“β‚‚_; ↓_ to ↓₂_)
   open Downward-Closure-Intersection-Syntax (Ξ» x y β†’ x βŠ‘[ π’ž ] y)
    renaming (_βŠ“_ to _βŠ“β‚ƒ_; ↓_ to ↓₃_)

   Ξ² : preserves-binary-meets π’œ π’ž (relational-image g ∘ f) holds
   Ξ² a₁ aβ‚‚ c (μ₁ , ΞΌβ‚‚) = βˆ₯βˆ₯-recβ‚‚ (holds-is-prop (_ ◁[ π’ž ] _)) † μ₁ ΞΌβ‚‚
    where
     † : Ξ£ c₁ κž‰ ⟨ π’ž ⟩ , c₁ ∈ (relational-image g ∘ f) a₁ Γ— (c ≀[ R ] c₁) holds
       β†’ Ξ£ cβ‚‚ κž‰ ⟨ π’ž ⟩ , cβ‚‚ ∈ (relational-image g ∘ f) aβ‚‚ Γ— (c ≀[ R ] cβ‚‚) holds
       β†’ (c ◁[ π’ž ] (relational-image g ∘ f) β¦… lower-bounds π’œ π’œ a₁ aβ‚‚ ⦆) holds
     † (c₁ , ν₁ , p₁) (cβ‚‚ , Ξ½β‚‚ , pβ‚‚) = βˆ₯βˆ₯-recβ‚‚ (holds-is-prop (_ ◁[ π’ž ] _)) Ξ³ ν₁ Ξ½β‚‚
      where
       Ξ³ : (Ξ£ (b₁ , _) κž‰ 𝕋 (f a₁) , c₁ ∈ g b₁)
         β†’ (Ξ£ (bβ‚‚ , _) κž‰ 𝕋 (f aβ‚‚) , cβ‚‚ ∈ g bβ‚‚)
         β†’ (c ◁[ π’ž ] (relational-image g ∘ f) β¦… lower-bounds π’œ π’œ a₁ aβ‚‚ ⦆) holds
       Ξ³ ((b₁ , θ₁) , q₁) ((bβ‚‚ , ΞΈβ‚‚) , qβ‚‚) =
         c                                                   β—βŸ¨  β…  ⟩
         g b₁ βŠ“β‚ƒ g bβ‚‚                                        β—βΊβŸ¨ β…‘ ⟩
         g β¦… lower-bounds ℬ ℬ b₁ bβ‚‚ ⦆                        β—βΊβŸ¨ β…’ ⟩
         g β¦… f β¦… lower-bounds π’œ π’œ a₁ aβ‚‚ ⦆ ⦆                  ＝⟨ β…£ ⟩c
         (relational-image g ∘ f) β¦… lower-bounds π’œ π’œ a₁ aβ‚‚ ⦆ β– 
         where
          β…  : (c ◁[ π’ž ] g b₁ βŠ“β‚ƒ g bβ‚‚) holds
          β…  = reflexivity-of-quasi-cover
               π’žβ‚€
               c
               (g b₁ βŠ“β‚ƒ g bβ‚‚)
               (∣ c₁ , q₁ , p₁ ∣ , ∣ cβ‚‚ , qβ‚‚ , pβ‚‚ ∣)

          β…‘ : (g b₁ βŠ“β‚ƒ g bβ‚‚ ◁⁺[ π’ž ] g β¦… lower-bounds ℬ ℬ b₁ bβ‚‚ ⦆) holds
          β…‘ = ft-fun-preserves-binary-meets ℬ π’ž β„Š b₁ bβ‚‚

          ΞΎ : (lower-bounds ℬ ℬ b₁ bβ‚‚ ◁⁺[ ℬ ] f β¦… lower-bounds π’œ π’œ a₁ aβ‚‚ ⦆) holds
          ΞΎ = lower-bounds ℬ ℬ b₁ bβ‚‚                  β—βΊβŸ¨ β…₯ ⟩
              f a₁ βŠ“β‚‚ f aβ‚‚                            β—βΊβŸ¨ β…¦ ⟩
              f β¦… lower-bounds π’œ π’œ a₁ aβ‚‚ ⦆ β– 
               where
                open Quasi-Cover-Reasoning ℬ₀

                β…₯ : (lower-bounds ℬ ℬ b₁ bβ‚‚ ◁⁺[ ℬ ] f a₁ βŠ“β‚‚ f aβ‚‚) holds
                β…₯ b (r₁ , rβ‚‚) = reflexivity-of-quasi-cover
                                 ℬ₀
                                 b
                                 (f a₁ βŠ“β‚‚ f aβ‚‚)
                                 (∣ b₁ , θ₁ , r₁ ∣ , ∣ bβ‚‚ , ΞΈβ‚‚ , rβ‚‚ ∣)

                β…¦ : (f a₁ βŠ“β‚‚ f aβ‚‚ ◁⁺[ ℬ ] f β¦… lower-bounds π’œ π’œ a₁ aβ‚‚ ⦆) holds
                β…¦ = ft-fun-preserves-binary-meets π’œ ℬ 𝒻 a₁ aβ‚‚

          β…’ : (g β¦… lower-bounds ℬ ℬ b₁ bβ‚‚ ⦆ ◁⁺[ π’ž ] g β¦… f β¦… lower-bounds π’œ π’œ a₁ aβ‚‚ ⦆ ⦆)
               holds
          β…’ = fun-preserves-covering-plus ℬ₀ π’žβ‚€ β„Šβ‚€ (lower-bounds ℬ ℬ b₁ bβ‚‚) _ ΞΎ

          β…£ = relational-image-commutes-with-composition f g (lower-bounds π’œ π’œ a₁ aβ‚‚)

          open Quasi-Cover-Reasoning π’žβ‚€

\end{code}

The identity morphism is left neutral for composition.

\begin{code}

id-ftop-is-left-neutral : (π’œ ℬ : Formal-Topology 𝓀)
                        β†’ (𝒻 : π’œ ─ftβ†’ ℬ)
                        β†’ ftop-composition π’œ ℬ ℬ (identity-morphism-ft ℬ) 𝒻 ＝ 𝒻
id-ftop-is-left-neutral π’œ ℬ 𝒻 = to-formal-topology-morphism-＝ π’œ ℬ _ 𝒻 †
 where
  π’œβ‚€ = underlying-quasi-formal-topology π’œ
  ℬ₀ = underlying-quasi-formal-topology ℬ

  𝒻₀ = to-qft-morphism π’œ ℬ 𝒻

  † : ft-fun π’œ ℬ (ftop-composition π’œ ℬ ℬ (identity-morphism-ft ℬ) 𝒻) ∼ ft-fun π’œ ℬ 𝒻
  † = happly (ap (fun π’œβ‚€ ℬ₀) (id-qftop-is-left-neutral π’œβ‚€ ℬ₀ 𝒻₀))

\end{code}

The identity morphism is right neutral for composition.

\begin{code}

id-ftop-is-right-neutral
 : (π’œ ℬ : Formal-Topology 𝓀)
 β†’ (𝒻 : π’œ ─ftβ†’ ℬ)
 β†’ ftop-composition π’œ π’œ ℬ 𝒻 (identity-morphism-ft π’œ) ＝ 𝒻
id-ftop-is-right-neutral π’œ ℬ 𝒻 = to-formal-topology-morphism-＝ π’œ ℬ _ 𝒻 †
 where
  π’œβ‚€ = underlying-quasi-formal-topology π’œ
  ℬ₀ = underlying-quasi-formal-topology ℬ

  𝒻₀ = to-qft-morphism π’œ ℬ 𝒻

  † : ft-fun π’œ ℬ (ftop-composition π’œ π’œ ℬ 𝒻 (identity-morphism-ft π’œ)) ∼ ft-fun π’œ ℬ 𝒻
  † = happly (ap (fun π’œβ‚€ ℬ₀) (id-qftop-is-right-neutral π’œβ‚€ ℬ₀ 𝒻₀))

\end{code}

Composition of formal topology morphisms is associative.

\begin{code}

ftop-composition-is-associative
 : (π’œ ℬ π’ž π’Ÿ : Formal-Topology 𝓀)
 β†’ (𝒻 : π’œ ─ftβ†’ ℬ)
 β†’ (β„Š : ℬ ─ftβ†’ π’ž)
 β†’ (𝒽 : π’ž ─ftβ†’ π’Ÿ)
 β†’ ftop-composition π’œ π’ž π’Ÿ 𝒽 (ftop-composition π’œ ℬ π’ž β„Š 𝒻)
   ＝ ftop-composition π’œ ℬ π’Ÿ (ftop-composition ℬ π’ž π’Ÿ 𝒽 β„Š) 𝒻
ftop-composition-is-associative π’œ ℬ π’ž π’Ÿ 𝒻 β„Š 𝒽 =
 to-formal-topology-morphism-＝ π’œ π’Ÿ _ _ †
 where
  open Formal-Topology-Morphism π’œ π’Ÿ
   hiding (to-formal-topology-morphism-＝; to-qft-morphism)

  π’œβ‚€ = underlying-quasi-formal-topology π’œ
  ℬ₀ = underlying-quasi-formal-topology ℬ
  π’žβ‚€ = underlying-quasi-formal-topology π’ž
  π’Ÿβ‚€ = underlying-quasi-formal-topology π’Ÿ

  𝒻₀ = to-qft-morphism π’œ ℬ 𝒻
  β„Šβ‚€ = to-qft-morphism ℬ π’ž β„Š
  𝒽₀ = to-qft-morphism π’ž π’Ÿ 𝒽

  † : [ (ftop-composition π’œ π’ž π’Ÿ 𝒽 (ftop-composition π’œ ℬ π’ž β„Š 𝒻)) ]
      ∼
      [ (ftop-composition π’œ ℬ π’Ÿ (ftop-composition ℬ π’ž π’Ÿ 𝒽 β„Š) 𝒻) ]
  † = qftop-composition-is-associative-extensional π’œβ‚€ ℬ₀ π’žβ‚€ π’Ÿβ‚€ 𝒻₀ β„Šβ‚€ 𝒽₀

\end{code}

Finally, we write down the precategory of formal topologies.

\begin{code}

FTopWildCategory : (𝓀 : Universe) β†’ WildCategory (𝓀 ⁺) (𝓀 ⁺)
FTopWildCategory 𝓀 =
 wildcategory
  (Formal-Topology 𝓀)
  _─ftβ†’_
  (Ξ» {π’œ} β†’ identity-morphism-ft π’œ)
  (Ξ» {π’œ} {ℬ} {π’ž} β†’ ftop-composition π’œ ℬ π’ž)
  (Ξ» {π’œ} {ℬ} β†’ id-ftop-is-left-neutral π’œ ℬ)
  (Ξ» {π’œ} {ℬ} β†’ id-ftop-is-right-neutral π’œ ℬ)
  (Ξ» {π’œ} {ℬ} {π’ž} {π’Ÿ} β†’ ftop-composition-is-associative π’œ ℬ π’ž π’Ÿ)

FTopPrecategory : (𝓀 : Universe) β†’ Precategory (𝓀 ⁺) (𝓀 ⁺)
FTopPrecategory 𝓀 = FTopWildCategory 𝓀 , †
 where
  † : is-precategory (FTopWildCategory 𝓀)
  † π’œ ℬ = _─ftβ†’_-is-set π’œ ℬ

\end{code}

[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