Martin Escardo, 24 June 2026.

In the module TypeTopology.TotallySeparated we construct the totally
separated reflection of a type X as the image of the evaluation map
X β†’ ((X β†’ 𝟚) β†’ 𝟚).

An alternative construction, developed here, is given by the set-quotient
of X by the equivalence relation

  x ＝₂ y := (p : X β†’ 𝟚) β†’ p x ＝ p y.

\begin{code}

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

open import UF.FunExt
open import UF.PropTrunc
open import Quotient.Type

module TypeTopology.TotallySeparatedReflectionViaQuotients
        (fe : FunExt)
        (pt : propositional-truncations-exist)
        (sq : set-quotients-exist)
       where

open import MLTT.Spartan
open import MLTT.Two-Properties
open import TypeTopology.TotallySeparated
open import UF.DiscreteAndSeparated
open import UF.Equiv
open import UF.ImageAndSurjection pt
open import UF.Sets
open import UF.Subsingletons
open import UF.Subsingletons-FunExt

open PropositionalTruncation pt
open general-set-quotients-exist sq
open totally-separated-reflection fe pt

private
 fe' : Fun-Ext
 fe' {𝓀} {π“₯} = fe 𝓀 π“₯

＝₂-eqrel : {X : 𝓀 Μ‡ } β†’ EqRel {𝓀} {𝓀} X
＝₂-eqrel = _＝₂_ ,
           (Ξ» x y β†’ Ξ -is-prop fe' (Ξ» _ β†’ 𝟚-is-set)) ,
           (Ξ» x p β†’ refl) ,
           (Ξ» x y e p β†’ (e p)⁻¹) ,
           (Ξ» x y z e d p β†’ e p βˆ™ d p)

𝕋₂ : 𝓀 Μ‡ β†’ 𝓀 Μ‡
𝕋₂ X = X / ＝₂-eqrel

Ο„ : {X : 𝓀 Μ‡ } β†’ X β†’ 𝕋₂ X
Ο„ = Ξ·/ ＝₂-eqrel

Ο„-identifies-＝₂ : {X : 𝓀 Μ‡ } {x y : X}
                 β†’ x ＝₂ y β†’ Ο„ x ＝ Ο„ y
Ο„-identifies-＝₂ = Ξ·/-identifies-related-points ＝₂-eqrel

𝕋₂-is-set : {X : 𝓀 Μ‡ } β†’ is-set (𝕋₂ X)
𝕋₂-is-set = /-is-set ＝₂-eqrel

Ο„-is-surjection : {X : 𝓀 Μ‡ } β†’ is-surjection (Ο„ {𝓀} {X})
Ο„-is-surjection = Ξ·/-is-surjection ＝₂-eqrel pt

\end{code}

Every map into a totally separated type respects ＝₂.

\begin{code}

maps-into-ts-identify-related-points : {X : 𝓀 Μ‡ } {A : π“₯ Μ‡ }
                                     β†’ is-totally-separated A
                                     β†’ (f : X β†’ A)
                                     β†’ ({x x' : X} β†’ x ＝₂ x' β†’ f x ＝ f x')
maps-into-ts-identify-related-points ts f e = ts (Ξ» p β†’ e (p ∘ f))

\end{code}

The universal property says that for any totally separated type A, the
restriction map _∘ Ο„ : (𝕋₂ X β†’ A) β†’ (X β†’ A) is an equivalence.

The extension of f : X β†’ A along Ο„ is the unique extension given by the
quotient universal property, which applies because A is totally
separated (hence f respects ＝₂).

\begin{code}

private
 ts-types-are-sets : {A : π“₯ Μ‡ } β†’ is-totally-separated A β†’ is-set A
 ts-types-are-sets {π“₯} {A} ts = totally-separated-types-are-sets fe' A ts

extension : {X : 𝓀 Μ‡ } {A : π“₯ Μ‡ }
          β†’ is-totally-separated A
          β†’ (X β†’ A) β†’ (𝕋₂ X β†’ A)
extension {𝓀} {π“₯} {X} {A} ts f =
 βˆƒ!-witness
  (/-universality ＝₂-eqrel (ts-types-are-sets ts) f
    (maps-into-ts-identify-related-points ts f))

extension-property : {X : 𝓀 Μ‡ } {A : π“₯ Μ‡ }
                   β†’ (ts  : is-totally-separated A)
                   β†’ (f : X β†’ A)
                   β†’ extension ts f ∘ Ο„ ∼ f
extension-property ts f =
 βˆƒ!-is-witness
  (/-universality ＝₂-eqrel (ts-types-are-sets ts) f
    (maps-into-ts-identify-related-points ts f))

\end{code}

We now show that the quotient type 𝕋₂ X is totally separated.  Given
two points u v : 𝕋₂ X with all 𝟚-valued maps agreeing on them, we use
the surjectivity of Ο„ to get preimages x and y, and then show that
x ＝₂ y by extending each p : X β†’ 𝟚 along Ο„.

\begin{code}

𝕋₂-is-totally-separated : {X : 𝓀 Μ‡ } β†’ is-totally-separated (𝕋₂ X)
𝕋₂-is-totally-separated {𝓀} {X} {u} {v} eβ‚‚ = III
 where
  _ : u ＝₂ v
  _ = eβ‚‚

  Ξ΅ : (X β†’ 𝟚) β†’ 𝕋₂ X β†’ 𝟚
  Ρ = extension 𝟚-is-totally-separated

  I : (x y : X) β†’ Ο„ x ＝ u β†’ Ο„ y ＝ v β†’ x ＝₂ y
  I x y ex ey p =
   p x       ＝⟨ (extension-property 𝟚-is-totally-separated p x)⁻¹ ⟩
   Ξ΅ p (Ο„ x) ＝⟨ ap (Ξ΅ p) ex ⟩
   Ξ΅ p u     ＝⟨ eβ‚‚ (Ξ΅ p) ⟩
   Ρ p v     ＝⟨ ap (Ρ p) (ey ⁻¹) ⟩
   Ξ΅ p (Ο„ y) ＝⟨ extension-property 𝟚-is-totally-separated p y ⟩
   p y       ∎

  II : (Ξ£ x κž‰ X , Ο„ x ＝ u) β†’ (Ξ£ y κž‰ X , Ο„ y ＝ v) β†’ u ＝ v
  II (x , ex) (y , ey) =
   u   ＝⟨ ex ⁻¹ ⟩
   Ο„ x ＝⟨ Ο„-identifies-＝₂ (I x y ex ey) ⟩
   Ο„ y ＝⟨ ey ⟩
   v   ∎

  III : u ＝ v
  III = βˆ₯βˆ₯-recβ‚‚ 𝕋₂-is-set II (Ο„-is-surjection u) (Ο„-is-surjection v)

extension-of-restriction : {X : 𝓀 Μ‡ } {A : π“₯ Μ‡ }
                         β†’ (ts  : is-totally-separated A)
                         β†’ (g : 𝕋₂ X β†’ A)
                         β†’ extension ts (g ∘ Ο„) ＝ g
extension-of-restriction ts g =
 ap pr₁
    (βˆƒ!-uniqueness
      (/-universality ＝₂-eqrel (ts-types-are-sets ts) (g ∘ Ο„)
        (maps-into-ts-identify-related-points ts (g ∘ Ο„)))
      g (Ξ» x β†’ refl))

universal-property : {X : 𝓀 Μ‡ } {A : π“₯ Μ‡ }
                   β†’ is-totally-separated A
                   β†’ (𝕋₂ X β†’ A) ≃ (X β†’ A)
universal-property ts = qinveq (_∘ Ο„)
                         (extension ts ,
                          extension-of-restriction ts ,
                          (Ξ» f β†’ dfunext fe' (extension-property ts f)))


\end{code}

We now record the comparison maps between 𝕋 X (the image construction)
and 𝕋₂ X (the quotient construction). Each one is the unique map given
by the universal property of the other.

\begin{code}

module comparison {X : 𝓀 Μ‡ } where

 c : 𝕋 X β†’ 𝕋₂ X
 c = extα΅€ 𝕋₂-is-totally-separated Ο„

 c-triangle : c ∘ Ξ·α΅€ ∼ Ο„
 c-triangle = ext-Ξ·α΅€ 𝕋₂-is-totally-separated Ο„

 𝕋-is-set : is-set (𝕋 X)
 𝕋-is-set = totally-separated-types-are-sets fe' (𝕋 X) 𝕋-is-totally-separated

 c⁻¹ : 𝕋₂ X β†’ 𝕋 X
 c⁻¹ = extension 𝕋-is-totally-separated Ξ·α΅€

 c⁻¹-triangle : c⁻¹ ∘ Ο„ ∼ Ξ·α΅€
 c⁻¹-triangle = extension-property 𝕋-is-totally-separated Ξ·α΅€

 c-is-section : c⁻¹ ∘ c ∼ id
 c-is-section = Ξ·α΅€-induction _ (Ξ» _ β†’ 𝕋-is-set) (Ξ» x β†’
  c⁻¹ (c (Ξ·α΅€ x)) ＝⟨ ap c⁻¹ (c-triangle x) ⟩
  c⁻¹ (Ο„ x)      ＝⟨ c⁻¹-triangle x ⟩
  Ξ·α΅€ x           ∎)

 c-is-retraction : c ∘ c⁻¹ ∼ id
 c-is-retraction = surjection-induction Ο„ Ο„-is-surjection _ (Ξ» _ β†’ 𝕋₂-is-set {𝓀} {X}) (Ξ» x β†’
  c (c⁻¹ (Ο„ x)) ＝⟨ ap c (c⁻¹-triangle x) ⟩
  c (Ξ·α΅€ x)      ＝⟨ c-triangle x ⟩
  Ο„ x           ∎)

 𝕋-≃-𝕋₂ : 𝕋 X ≃ 𝕋₂ X
 𝕋-≃-𝕋₂ = qinveq c (c⁻¹ , c-is-section , c-is-retraction)

\end{code}