Martin Escardo 2011, 2017, 2018.

We define and study totally separated types (which could also have
been called 𝟚-separated types). Most of the material in this file is
from January 2018.

The terminology "totally separated" comes from topology, where it
means that the clopens separate the points. Here the maps into 𝟚
separate the points, formulated in a positive way.

Any type has a totally separated reflection, assuming function
extensionality and propositional truncations.

All the simple types (those obtained from 𝟚 and β„• by iterating
function spaces) are totally separated (see the module
SimpleTypes). This is because the totally separated types form an
exponential ideal. Moreover, Ξ  Y is totally separated for any family
Y:X→U provided Y x is totally separated for all x:X. This assumes
function extensionality.

In particular, the Cantor and Baire types 𝟚^β„• and β„•^β„• are totally
separated (like in topology).

Closure under Ξ£ fails in general. However, we have closure under _Γ—_,
and β„•βˆž (defined with Ξ£) is totally separated (proved in the module
GenericConvergentSequence).

A counter-example to closure under Ξ£ (from 2012) is in the file
http://www.cs.bham.ac.uk/~mhe/agda-new/FailureOfTotalSeparatedness.html

This is the "compactification" of β„• with two points at infinity:

   Ξ£ \(u : β„•βˆž) β†’ u ≑ ∞ β†’ 𝟚.

If there is a 𝟚-valued function separating the two points at infinity,
then WLPO holds. (The totally separated reflection of this type should
be β„•βˆž if Β¬WLPO holds.)

(In the context of topology, I learned this example from the late
Klaus Keimel (but the rendering in type theory is mine), where it is a
T₁, non-Tβ‚‚, and non totally separated space which is zero dimensional
(has a base of clopen sets), and where the intersection of two compact
subsets need not be compact. The failure of the Hausdorff property is
with the two points an infinity, which can't be separated by disjoint
open neighbourhoods.)

The total separatedness of the reals (of any kind) should also give a
taboo. All non-sets fail (without the need of taboos) to be totally
separated, because totally separated spaces are sets.

Total separatedness is also characterized as the tightness of a
certain apartness relation that can be defined in any type.

We also show how to construct the tight reflection of any type
equipped with an apartness relation, given by a universal strongly
extensional map into a tight apartness type. Any type with a tight
apartness relation is a set, and so this reflection is always a set.


\begin{code}

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

module TotallySeparated where

open import SpartanMLTT

open import Two-Properties
open import DiscreteAndSeparated hiding (tight)
open import UF-Base
open import UF-Subsingletons
open import UF-Retracts
open import UF-Equiv
open import UF-LeftCancellable
open import UF-Embeddings
open import UF-FunExt
open import UF-PropTrunc
open import UF-ImageAndSurjection

\end{code}

An equality defined by a Leibniz principle with 𝟚-valued functions:

\begin{code}

_≑₂_ : {X : 𝓀 Μ‡ } β†’ X β†’ X β†’ 𝓀 Μ‡
x ≑₂ y = (p : _ β†’ 𝟚) β†’ p x ≑ p y

\end{code}

(In topological models, maps into 𝟚 classify clopens, and so total
separatedness amounts to "the clopens separate the points" in the
sense that any two points with the same clopen neighbourhoods are
equal. This notion in topology is called total separatedness.)

\begin{code}

is-totally-separated : 𝓀 Μ‡ β†’ 𝓀 Μ‡
is-totally-separated X = {x y : X} β†’ x ≑₂ y β†’ x ≑ y

\end{code}

Synonym:

\begin{code}

𝟚-separated : 𝓀 Μ‡ β†’ 𝓀 Μ‡
𝟚-separated = is-totally-separated

\end{code}

Excluded middle implies that all sets are discrete and hence totally
separated:

\begin{code}

discrete-totally-separated : {X : 𝓀 Μ‡ } β†’ is-discrete X β†’ is-totally-separated X
discrete-totally-separated {𝓀} {X} d {x} {y} Ξ± = g
 where
  open import DecidableAndDetachable
  p : X β†’ 𝟚
  p = pr₁ (characteristic-function (d x))

  Ο† : (y : X) β†’ (p y ≑ β‚€ β†’ x ≑ y) Γ— (p y ≑ ₁ β†’ Β¬ (x ≑ y))
  Ο† = prβ‚‚ (characteristic-function (d x))

  b : p x ≑ β‚€
  b = different-from-₁-equal-β‚€ (Ξ» s β†’ prβ‚‚ (Ο† x) s refl)

  a : p y ≑ β‚€
  a = (Ξ± p)⁻¹ βˆ™ b

  g : x ≑ y
  g = pr₁ (Ο† y) a

\end{code}

The converse fails: by the results below, e.g. (β„• β†’ 𝟚) is totally
separated, but its discreteness amounts to WLPO.

\begin{code}

retract-totally-separated : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡}
                          β†’ retract Y of X β†’ is-totally-separated X β†’ is-totally-separated Y
retract-totally-separated (r , (s , rs)) ts {y} {y'} Ξ± = section-lc s (r , rs) h
 where
  h : s y ≑ s y'
  h = ts (Ξ» p β†’ Ξ± (p ∘ s))

\end{code}

Recall that a type is called separated if the doubly negated equality
of any two element implies their equality, and that such a type is a
set.

\begin{code}

totally-separated-types-are-separated : (X : 𝓀 Μ‡ ) β†’ is-totally-separated X β†’ is-separated X
totally-separated-types-are-separated X ts = g
 where
  g : (x y : X) β†’ ¬¬(x ≑ y) β†’ x ≑ y
  g x y Ο†  = ts h
   where
    a : (p : X β†’ 𝟚) β†’ ¬¬(p x ≑ p y)
    a p = ¬¬-functor (ap p {x} {y}) Ο†

    h : (p : X β†’ 𝟚) β†’ p x ≑ p y
    h p = 𝟚-is-separated (p x) (p y) (a p)

open import UF-Miscelanea

totally-separated-types-are-sets : funext 𝓀 𝓀₀ β†’ (X : 𝓀 Μ‡ ) β†’ is-totally-separated X β†’ is-set X
totally-separated-types-are-sets fe X t = separated-types-are-sets fe (totally-separated-types-are-separated X t)

\end{code}

The converse fails: the type of propositions is a set, but its total
separatedness implies excluded middle. In fact, its separatedness
already implies excluded middle (exercise).

The need to define f and g in the following proof arises because the
function is-prop-is-exponential ideal requires a dependent function
with explicit arguments, but total separatedness is defined with
implicit arguments. The essence of the proof is that of p in the where
clause.

\begin{code}

total-separatedness-is-a-prop : funext 𝓀 𝓀 β†’ funext 𝓀 𝓀₀
                              β†’ (X : 𝓀 Μ‡ ) β†’ is-prop(is-totally-separated X)
total-separatedness-is-a-prop {𝓀} fe feβ‚€ X = Ξ³
 where
  T : 𝓀 Μ‡
  T = (x y : X) β†’ x ≑₂ y β†’ x ≑ y
  f : T β†’ is-totally-separated X
  f t {x} {y} Ο† = t x y Ο†
  g : is-totally-separated X β†’ T
  g t x y Ο† = t {x} {y} Ο†
  p : is-prop T
  p t = Ξ -is-prop fe
           (Ξ» x β†’ Ξ -is-prop fe
                    (Ξ» y β†’ Ξ -is-prop fe
                              (Ξ» p β†’ totally-separated-types-are-sets feβ‚€ X (f t))))
        t

  Ξ³ : is-prop (is-totally-separated X)
  Ξ³ = subtype-of-prop-is-a-prop g (Ξ» {t} {u} (q : g t ≑ g u) β†’ ap f q) p
\end{code}

Old proof which by-passes the step via separatedness:

\begin{code}

totally-separated-types-are-sets' : funext 𝓀 𝓀₀ β†’ (X : 𝓀 Μ‡ ) β†’ is-totally-separated X β†’ is-set X
totally-separated-types-are-sets' fe X t = Id-collapsibles-are-sets h
 where
  f : {x y : X} β†’ x ≑ y β†’ x ≑ y
  f r = t(Ξ» p β†’ ap p r)

  b : {x y : X} (Ο† Ξ³ : (p : X β†’ 𝟚) β†’ p x ≑ p y) β†’ Ο† ≑ Ξ³
  b Ο† Ξ³ = dfunext fe (Ξ» p β†’ discrete-types-are-sets 𝟚-is-discrete (Ο† p) (Ξ³ p))

  c : {x y : X} (r s : x ≑ y) β†’ (Ξ» p β†’ ap p r) ≑ (Ξ» p β†’ ap p s)
  c r s = b(Ξ» p β†’ ap p r) (Ξ» p β†’ ap p s)

  g : {x y : X} β†’ constant(f {x} {y})
  g r s = ap t (c r s)

  h : Id-collapsible X
  h {x} {y} = f , g

\end{code}

As discussed above, we don't have general closure under Ξ£, but we have
the following particular cases:

\begin{code}

Γ—-totally-separated : (X : 𝓀 Μ‡ ) (Y : π“₯ Μ‡)
                    β†’ is-totally-separated X
                    β†’ is-totally-separated Y
                    β†’ is-totally-separated (X Γ— Y)
Γ—-totally-separated X Y t u {a , b} {x , y} Ο† =
   to-Γ—-≑ (t (Ξ» (p : X β†’ 𝟚) β†’ Ο† (Ξ» (z : X Γ— Y) β†’ p (pr₁ z))))
          (u (Ξ» (q : Y β†’ 𝟚) β†’ Ο† (Ξ» (z : X Γ— Y) β†’ q (prβ‚‚ z))))

Ξ£-is-totally-separated : (X : 𝓀 Μ‡ ) (Y : X β†’ π“₯ Μ‡)
                       β†’ is-discrete X
                       β†’ ((x : X) β†’ is-totally-separated (Y x))
                       β†’ is-totally-separated (Ξ£ Y)
Ξ£-is-totally-separated X Y d t {a , b} {x , y} Ο† = to-Ξ£-≑ (r , s)
 where
  r : a ≑ x
  r = discrete-totally-separated d (Ξ» p β†’ Ο† (Ξ» z β†’ p (pr₁ z)))
  sβ‚‚ : transport Y r b ≑₂ y
  sβ‚‚ q = g
   where
    f : {u : X} β†’ (u ≑ x) + Β¬(u ≑ x) β†’ Y u β†’ 𝟚
    f (inl m) v = q (transport Y m v)
    f (inr _) v = β‚€ --<-- What we choose here is irrelevant.
    p : Ξ£ Y β†’ 𝟚
    p (u , v) = f (d u x) v
    i : p (a , b) ≑ q (transport Y r b)
    i = ap (Ξ» - β†’ f - b) (discrete-inl d a x r)
    j : p (a , b) ≑ p (x , y)
    j = Ο† p
    k : p (x , y) ≑ q (transport Y refl y)
    k = ap (Ξ» - β†’ f - y) (discrete-inl d x x refl)
    g : q (transport Y r b) ≑ q y
    g = i ⁻¹ βˆ™ j βˆ™ k
  s : transport Y r b ≑ y
  s = t x sβ‚‚

\end{code}

Maybe this can be further generalized by replacing the discreteness of X
with the assumption that

  (x : X) (q : Y x β†’ 𝟚) β†’ Ξ£ \(p : Ξ£ Y β†’ 𝟚) β†’ (y : Y x) β†’ q y ≑ p (x , y).

Then the previous few functions would be a particular case of this.


The following can also be considered as a special case of Σ (indexed by the type 𝟚):

\begin{code}

+-totally-separated : (X : 𝓀 Μ‡ ) (Y : π“₯ Μ‡)
                    β†’ is-totally-separated X
                    β†’ is-totally-separated Y
                    β†’ is-totally-separated (X + Y)
+-totally-separated X Y t u {inl x} {inl x'} Ο† =
    ap inl (t (Ξ» p β†’ Ο† (cases p (Ξ» (_ : Y) β†’ β‚€))))
+-totally-separated X Y t u {inl x} {inr y} Ο† =
    𝟘-elim (zero-is-not-one (Ο† (cases (Ξ» _ β†’ β‚€) (Ξ» _ β†’ ₁))))
+-totally-separated X Y t u {inr y} {inl x} Ο† =
    𝟘-elim (zero-is-not-one (Ο† (cases (Ξ» _ β†’ ₁) (Ξ» _ β†’ β‚€))))
+-totally-separated X Y t u {inr y} {inr y'} Ο† =
    ap inr (u (Ξ» p β†’ Ο† (cases (Ξ» (_ : X) β†’ β‚€) p)))

\end{code}

\begin{code}

𝟚-is-totally-separated : is-totally-separated 𝟚
𝟚-is-totally-separated e = e id

Ξ -is-totally-separated : funext 𝓀 π“₯ β†’ {X : 𝓀 Μ‡ } {Y : X β†’ π“₯ Μ‡}
                   β†’ ((x : X) β†’ is-totally-separated(Y x)) β†’ is-totally-separated(Ξ  Y)
Ξ -is-totally-separated fe {X} {Y} t {f} {g} e = dfunext fe h
 where
   P : (x : X) (p : Y x β†’ 𝟚) β†’ Ξ  Y β†’ 𝟚
   P x p f = p(f x)

   h : (x : X) β†’ f x ≑ g x
   h x = t x (Ξ» p β†’ e(P x p))

Cantor-is-totally-separated : funext 𝓀₀ 𝓀₀ β†’ is-totally-separated (β„• β†’ 𝟚)
Cantor-is-totally-separated fe = Ξ -is-totally-separated fe (Ξ» n β†’ 𝟚-is-totally-separated)

\end{code}

Closure under /-extensions (see the module InjectiveTypes). Notice
that j doesn't need to be an embedding (which which case the extension
is merely a Kan extension rather than a proper extension).

\begin{code}

module _ (fe : FunExt)  where

 open import InjectiveTypes fe

 /-is-totally-separated : {X : 𝓀 Μ‡ } {A : π“₯ Μ‡}
                          (j : X β†’ A)
                          (Y : X β†’ 𝓦 Μ‡ )
                        β†’ ((x : X) β†’ is-totally-separated (Y x))
                        β†’ (a : A) β†’ is-totally-separated ((Y / j) a)
 /-is-totally-separated {𝓀} {π“₯} {𝓦} j Y t a = Ξ -is-totally-separated (fe (𝓀 βŠ” π“₯) 𝓦)
                                                 (Ξ» (Οƒ : fiber j a) β†’ t (pr₁ Οƒ))

\end{code}

We now characterize the totally separated types X as those such that
the map eval {X} is an embedding, in order to construct totally
separated reflections.

\begin{code}

eval : {X : 𝓀 Μ‡ } β†’ X β†’ ((X β†’ 𝟚) β†’ 𝟚)
eval x = Ξ» p β†’ p x

tsieeval : {X : 𝓀 Μ‡ } β†’ funext 𝓀 𝓀₀ β†’ is-totally-separated X β†’ is-embedding(eval {𝓀} {X})
tsieeval {𝓀} {X} fe ts Ο† (x , p) (y , q) = to-Ξ£-≑ (t , r)
  where
   s : eval x ≑ eval y
   s = p βˆ™ q ⁻¹

   t : x ≑ y
   t = ts (happly s)

   r : transport (Ξ» - β†’ eval - ≑ Ο†) t p ≑ q
   r = totally-separated-types-are-sets fe
         ((X β†’ 𝟚) β†’ 𝟚) (Ξ -is-totally-separated fe (Ξ» p β†’ 𝟚-is-totally-separated)) _ q

ieevalts : {X : 𝓀 Μ‡ } β†’ funext 𝓀 𝓀₀ β†’ is-embedding(eval {𝓀} {X}) β†’ is-totally-separated X
ieevalts {𝓀} {X} fe i {x} {y} e = ap pr₁ q
  where
   Ο† : (X β†’ 𝟚) β†’ 𝟚
   Ο† = eval x

   h : is-prop (fiber eval  Ο†)
   h = i Ο†

   g : eval y ≑ Ο†
   g = dfunext fe (Ξ» p β†’ (e p)⁻¹)

   q : x , refl ≑ y , g
   q = h (x , refl) (y , g)

\end{code}

 Now, if a type is not (necessarily) totally separated, we can
 consider the image of the map eval {X}, and this gives the totally
 separated reflection, with the corestriction of eval {X} to its image
 as its reflector.

\begin{code}

module TotallySeparatedReflection
         (fe : FunExt)
         (pt : propositional-truncations-exist)
 where

 open PropositionalTruncation pt
 open ImageAndSurjection pt

\end{code}

We construct the reflection as the image of the evaluation map.

\begin{code}

 𝕋 : 𝓀 Μ‡ β†’ 𝓀 Μ‡
 𝕋 {𝓀} X = image (eval {𝓀} {X})

 tts : {X : 𝓀 Μ‡ } β†’ is-totally-separated(𝕋 X)
 tts {𝓀} {X} {Ο† , s} {Ξ³ , t} = g
  where
   f : (e : (q : 𝕋 X β†’ 𝟚) β†’ q (Ο† , s) ≑ q (Ξ³ , t)) (p : X β†’ 𝟚) β†’ Ο† p ≑ Ξ³ p
   f e p = e (Ξ» (x' : 𝕋 X) β†’ pr₁ x' p)

   g : (e : (q : 𝕋 X β†’ 𝟚) β†’ q (Ο† , s) ≑ q (Ξ³ , t)) β†’ (Ο† , s) ≑ (Ξ³ , t)
   g e = to-Ξ£-≑ (dfunext (fe 𝓀 𝓀₀) (f e), βˆ₯βˆ₯-is-a-prop _ t)

\end{code}

Then the reflector is the corestriction of the evaluation map. The
induction principle for surjections gives an induction principle for
the reflector.

\begin{code}


 Ξ· : {X : 𝓀 Μ‡ } β†’ X β†’ 𝕋 X
 Ξ· {X} = corestriction (eval {X})

 Ξ·-surjection : {X : 𝓀 Μ‡ } β†’ is-surjection(Ξ· {𝓀} {X})
 Ξ·-surjection = corestriction-surjection eval

 Ξ·-induction :  {X : 𝓀 Μ‡ } (P : 𝕋 X β†’ 𝓦 Μ‡ )
             β†’ ((x' : 𝕋 X) β†’ is-prop(P x'))
             β†’ ((x : X) β†’ P(Ξ· x))
             β†’ (x' : 𝕋 X) β†’ P x'
 Ξ·-induction = surjection-induction Ξ· Ξ·-surjection

\end{code}

Perhaps we could have used more induction in the following proof
rather than direct proofs (as in the proof of tight reflection below).

\begin{code}

 totally-separated-reflection : {X : 𝓀 Μ‡ } {A : π“₯ Μ‡} β†’ is-totally-separated A
                              β†’ (f : X β†’ A) β†’ βˆƒ! \(f' : 𝕋 X β†’ A) β†’ f' ∘ Ξ· ≑ f
 totally-separated-reflection {𝓀} {π“₯} {X} {A} ts f = go
  where
   iss : is-set A
   iss = totally-separated-types-are-sets (fe π“₯ 𝓀₀) A ts

   ie : (Ξ³ : (A β†’ 𝟚) β†’ 𝟚) β†’ is-prop (Ξ£ \(a : A) β†’ eval a ≑ Ξ³)
   ie = tsieeval (fe π“₯ 𝓀₀) ts

   h : (Ο† : (X β†’ 𝟚) β†’ 𝟚) β†’ (βˆƒ \(x : X) β†’ eval x ≑ Ο†) β†’ Ξ£ \(a : A) β†’ eval a ≑ (Ξ» q β†’ Ο†(q ∘ f))
   h Ο† = βˆ₯βˆ₯-rec (ie Ξ³) u
    where
     Ξ³ : (A β†’ 𝟚) β†’ 𝟚
     Ξ³ q = Ο† (q ∘ f)

     u : (Ξ£ \(x : X) β†’ (Ξ» p β†’ p x) ≑ Ο†) β†’ Ξ£ \(a : A) β†’ eval a ≑ Ξ³
     u (x , r) = f x , dfunext (fe π“₯ 𝓀₀) (Ξ» q β†’ happly r (q ∘ f))

   h' : (x' : 𝕋 X) β†’ Ξ£ \(a : A) β†’ eval a ≑ (Ξ» q β†’ pr₁ x' (q ∘ f))
   h' (Ο† , s) = h Ο† s

   f' : 𝕋 X β†’ A
   f' (Ο† , s) = pr₁ (h Ο† s)

   b : (x' : 𝕋 X) (q : A β†’ 𝟚) β†’ q(f' x') ≑ pr₁ x' (q ∘ f)
   b (Ο† , s) = happly (prβ‚‚ (h Ο† s))

   r : f' ∘ Ξ· ≑ f
   r = dfunext (fe 𝓀 π“₯) (Ξ» x β†’ ts (b (Ξ· x)))

   c : (Οƒ : Ξ£ \(f'' : 𝕋 X β†’ A) β†’ f'' ∘ Ξ· ≑ f) β†’ (f' , r) ≑ Οƒ
   c (f'' , s) = to-Ξ£-≑ (t , v)
    where
     w : βˆ€ x β†’ f'(Ξ· x) ≑ f''(Ξ· x)
     w = happly (r βˆ™ s ⁻¹)

     t : f' ≑ f''
     t = dfunext (fe 𝓀 π“₯) (Ξ·-induction _ (Ξ» _ β†’ iss) w)

     u : f'' ∘ Ξ· ≑ f
     u = transport (Ξ» - β†’ - ∘ Ξ· ≑ f) t r

     v : u ≑ s
     v = Ξ -is-set (fe 𝓀 π“₯) (Ξ» _ β†’ iss) u s

   go : βˆƒ! \(f' : 𝕋 X β†’ A) β†’ f' ∘ Ξ· ≑ f
   go = (f' , r) , c

\end{code}

We package the above as follows for convenient use elsewhere
(including the module 2CompactTypes).

\begin{code}

 totally-separated-reflection' : {X : 𝓀 Μ‡ } {A : π“₯ Μ‡} β†’ is-totally-separated A
                              β†’ is-equiv (Ξ» (f' : 𝕋 X β†’ A) β†’ f' ∘ Ξ·)
 totally-separated-reflection' ts = vv-equivs-are-equivs _ (totally-separated-reflection ts)

 totally-separated-reflection'' : {X : 𝓀 Μ‡ } {A : π“₯ Μ‡} β†’ is-totally-separated A
                               β†’ (𝕋 X β†’ A) ≃ (X β†’ A)
 totally-separated-reflection'' ts = (Ξ» f' β†’ f' ∘ Ξ·) , totally-separated-reflection' ts

\end{code}

In particular, because 𝟚 is totally separated, 𝕋 X and X have the same
boolean predicates (which we exploit in the module 2CompactTypes).

The notion of total separatedness (or 𝟚-separatedness) is analogous to
the Tβ‚€-separation axiom (which says that any two points with the same
open neighbourhoods are equal).

\begin{code}

𝟚-sober : 𝓦 Μ‡ β†’ 𝓀 ⁺ βŠ” 𝓦 Μ‡
𝟚-sober {𝓦} {𝓀} A = 𝟚-separated A Γ— ((X : 𝓀 Μ‡ ) (e : A β†’ X) β†’ is-equiv(dual 𝟚 e) β†’ is-equiv e)

\end{code}

TODO: example of 𝟚-separated type that fails to be 𝟚-sober, 𝟚-sober
reflection.

TODO: most of what we said doesn't depend on the type 𝟚, and total
separatedness can be generalized to S-separatedness for an arbitrary
type S, where 𝟚-separatedness is total separatedness. Then, for
example, Prop-separated is equivalent to is-set, all types in U are U
separated, Set-separatedness (where Set is the type of sets) should be
equivalent to is-1-groupoid, etc.

An interesting case is when S is (the total space of) a dominance,
generalizing the case S=Prop. Because the partial elements are defined
in terms of maps into S, the S-lifting of a type X should coincide
with the S-separated reflection of the lifting of X, and hence, in
this context, it makes sense to restrict our attention to S-separated
types.

Another useful thing is that in any type X we can define an apartness
relation xβ™―y by βˆƒ(p:Xβ†’πŸš), p(x)β€Œβ‰ p(y), which is tight iff X is totally
separated, where tightness means Β¬(xβ™―y)β†’x=y. Part of the following
should be moved to another module about apartness, but I keep it here
for the moment.

26 January 2018.

\begin{code}

module Apartness (pt : propositional-truncations-exist) where

 open PropositionalTruncation pt

 is-prop-valued is-irreflexive is-symmetric is-cotransitive is-tight is-apartness
     : {X : 𝓀 Μ‡ } β†’ (X β†’ X β†’ π“₯ Μ‡ ) β†’ 𝓀 βŠ” π“₯ Μ‡

 is-prop-valued  _β™―_ = βˆ€ x y β†’ is-prop(x β™― y)
 is-irreflexive  _β™―_ = βˆ€ x β†’ Β¬(x β™― x)
 is-symmetric    _β™―_ = βˆ€ x y β†’ x β™― y β†’ y β™― x
 is-cotransitive _β™―_ = βˆ€ x y z β†’ x β™― y β†’ x β™― z ∨ y β™― z
 is-tight        _β™―_ = βˆ€ x y β†’ Β¬(x β™― y) β†’ x ≑ y
 is-apartness    _β™―_ = is-prop-valued _β™―_ Γ— is-irreflexive _β™―_ Γ— is-symmetric _β™―_ Γ— is-cotransitive _β™―_

\end{code}

We now show that a type is totally separated iff a particular
apartness relation _β™―β‚‚ is tight:

\begin{code}

 _β™―β‚‚_ : {X : 𝓀 Μ‡ } β†’ X β†’ X β†’ 𝓀 Μ‡
 x β™―β‚‚ y = βˆƒ \(p : _ β†’ 𝟚) β†’ p x β‰’ p y

 β™―β‚‚-is-apartness : {X : 𝓀 Μ‡ } β†’ is-apartness (_β™―β‚‚_ {𝓀} {X})
 β™―β‚‚-is-apartness {𝓀} {X} = a , b , c , d
  where
   a : is-prop-valued _β™―β‚‚_
   a x y = βˆ₯βˆ₯-is-a-prop

   b : is-irreflexive _β™―β‚‚_
   b x = βˆ₯βˆ₯-rec 𝟘-is-prop g
    where
     g : Β¬ Ξ£ \(p : X β†’ 𝟚) β†’ p x β‰’ p x
     g (p , u) = u refl

   c : is-symmetric _β™―β‚‚_
   c x y = βˆ₯βˆ₯-functor g
    where
     g : (Ξ£ \(p : X β†’ 𝟚) β†’ p x β‰’ p y) β†’ Ξ£ \(p : X β†’ 𝟚) β†’ p y β‰’ p x
     g (p , u) = p , β‰’-sym u

   d : is-cotransitive _β™―β‚‚_
   d x y z = βˆ₯βˆ₯-functor g
    where
     g : (Ξ£ \(p : X β†’ 𝟚) β†’ p x β‰’ p y) β†’ (x β™―β‚‚ z) + (y β™―β‚‚ z)
     g (p , u) = h (discrete-is-cotransitive 𝟚-is-discrete {p x} {p y} {p z} u)
      where
       h : (p x β‰’ p z) + (p z β‰’ p y) β†’ (x β™―β‚‚ z) + (y β™―β‚‚ z)
       h (inl u) = inl ∣ p , u ∣
       h (inr v) = inr ∣ p , β‰’-sym v ∣

 β™―β‚‚-is-tight-ts : {X : 𝓀 Μ‡ } β†’ is-tight (_β™―β‚‚_ {𝓀} {X}) β†’ is-totally-separated X
 β™―β‚‚-is-tight-ts {𝓀} {X} t {x} {y} Ξ± = t x y (βˆ₯βˆ₯-rec 𝟘-is-prop h)
  where
   h : Β¬ Ξ£ \(p : X β†’ 𝟚) β†’ p x β‰’ p y
   h (p , u) = u (Ξ± p)

 ts-β™―β‚‚-is-tight : {X : 𝓀 Μ‡ } β†’ is-totally-separated X β†’ is-tight (_β™―β‚‚_ {𝓀} {X})
 ts-β™―β‚‚-is-tight {𝓀} {X} ts x y na = ts Ξ±
  where
   h : Β¬ Ξ£ \(p : X β†’ 𝟚) β†’ p x β‰’ p y
   h (p , u) = na ∣ p , u ∣

   Ξ± : (p : X β†’ 𝟚) β†’ p x ≑ p y
   Ξ± p = 𝟚-is-separated (p x) (p y) (Ξ» u β†’ h (p , u))

\end{code}

 12 Feb 2018. This was prompted by the discussion
 https://nforum.ncatlab.org/discussion/8282/points-of-the-localic-quotient-with-respect-to-an-apartness-relation/

 But is clearly related to the above characterization of total
 separatedness.

\begin{code}

 is-reflexive is-transitive is-equivalence-rel
     : {X : 𝓀 Μ‡ } β†’ (X β†’ X β†’ π“₯ Μ‡ ) β†’ 𝓀 βŠ” π“₯ Μ‡

 is-reflexive       _β‰ˆ_ = βˆ€ x β†’ x β‰ˆ x
 is-transitive      _β‰ˆ_ = βˆ€ x y z β†’ x β‰ˆ y β†’ y β‰ˆ z β†’ x β‰ˆ z
 is-equivalence-rel _β‰ˆ_ = is-prop-valued _β‰ˆ_ Γ— is-reflexive _β‰ˆ_ Γ— is-symmetric _β‰ˆ_ Γ— is-transitive _β‰ˆ_

\end{code}

 The following is the standard equivalence relation induced by an
 apartness relation. The tightness axiom defined above says that this
 equivalence relation is equality.

\begin{code}

 neg-apart-is-equiv : {X : 𝓀 Μ‡ } β†’ funext 𝓀 𝓀₀
                    β†’ (_β™―_ : X β†’ X β†’ 𝓀 Μ‡ ) β†’ is-apartness _β™―_ β†’ is-equivalence-rel (Ξ» x y β†’ Β¬(x β™― y))
 neg-apart-is-equiv {𝓀} {X} fe _β™―_ (β™―p , β™―i , β™―s , β™―c) = p , β™―i , s , t
  where
   p : (x y : X) β†’ is-prop (Β¬ (x β™― y))
   p x y = negations-are-props fe

   s : (x y : X) β†’ Β¬ (x β™― y) β†’ Β¬ (y β™― x)
   s x y u a = u (β™―s y x a)

   t : (x y z : X) β†’ Β¬ (x β™― y) β†’ Β¬ (y β™― z) β†’ Β¬ (x β™― z)
   t x y z u v a = v (β™―s z y (left-fails-then-right-holds (β™―p z y) b u))
    where
     b : (x β™― y) ∨ (z β™― y)
     b = β™―c x z y a

 \end{code}

 The following positive formulation of Β¬(x β™― y), which says that two
 elements have the same elements apart from them iff they are not
 apart, gives another way to see that it is an equivalence relation:

 \begin{code}

 not-apart-have-same-apart : {X : 𝓀 Μ‡ } (x y : X) (_β™―_ : X β†’ X β†’ π“₯ Μ‡ ) β†’ is-apartness _β™―_
                          β†’ Β¬(x β™― y) β†’ ((z : X) β†’ x β™― z ⇔ y β™― z)
 not-apart-have-same-apart {𝓀} {π“₯} {X} x y _β™―_ (p , i , s , c) = g
  where
   g : Β¬ (x β™― y) β†’ (z : X) β†’ x β™― z ⇔ y β™― z
   g n z = g₁ , gβ‚‚
    where
     g₁ : x β™― z β†’ y β™― z
     g₁ a = s z y (left-fails-then-right-holds (p z y) b n)
      where
       b : (x β™― y) ∨ (z β™― y)
       b = c x z y a

     n' : Β¬(y β™― x)
     n' a = n (s y x a)

     gβ‚‚ : y β™― z β†’ x β™― z
     gβ‚‚ a = s z x (left-fails-then-right-holds (p z x) b n')
      where
       b : (y β™― x) ∨ (z β™― x)
       b = c y z x a

 have-same-apart-are-not-apart : {X : 𝓀 Μ‡ } (x y : X) (_β™―_ : X β†’ X β†’ π“₯ Μ‡ ) β†’ is-apartness _β™―_
                               β†’ ((z : X) β†’ x β™― z ⇔ y β™― z) β†’ Β¬(x β™― y)
 have-same-apart-are-not-apart {𝓀} {π“₯} {X} x y _β™―_ (p , i , s , c) = f
  where
   f : ((z : X) β†’ x β™― z ⇔ y β™― z) β†’ Β¬ (x β™― y)
   f Ο† a = i y (pr₁(Ο† y) a)

\end{code}

 Not-not equal elements are not apart, and hence, in the presence of
 tightness, they are equal. It follows that tight apartness types are
 sets.

\begin{code}

 not-not-equal-not-apart : {X : 𝓀 Μ‡ } (x y : X) (_β™―_ : X β†’ X β†’ π“₯ Μ‡ )
                         β†’ is-apartness _β™―_ β†’ ¬¬(x ≑ y) β†’ Β¬(x β™― y)
 not-not-equal-not-apart x y _β™―_ (_ , i , _ , _) = contrapositive f
  where
   f : x β™― y β†’ Β¬(x ≑ y)
   f a p = i y (transport (Ξ» - β†’ - β™― y) p a)

 tight-is-separated : {X : 𝓀 Μ‡ } β†’ (_β™―_ : X β†’ X β†’ π“₯ Μ‡ )
                 β†’ is-apartness _β™―_ β†’ is-tight _β™―_ β†’ is-separated X
 tight-is-separated _β™―_ a t = f
  where
   f : βˆ€ x y β†’ ¬¬(x ≑ y) β†’ x ≑ y
   f x y Ο† = t x y (not-not-equal-not-apart x y _β™―_ a Ο†)

 tight-is-set : {X : 𝓀 Μ‡ } β†’ funext 𝓀 𝓀₀
           β†’ (_β™―_ : X β†’ X β†’ π“₯ Μ‡ ) β†’ is-apartness _β™―_ β†’ is-tight _β™―_ β†’ is-set X
 tight-is-set fe _β™―_ a t = separated-types-are-sets fe (tight-is-separated _β™―_ a t)

\end{code}

 The above use the apartness and tightness data, but their existence is
 enough, because being a separated type and being a set are
 propositions.

\begin{code}

 tight-separated' : {X : 𝓀 Μ‡ } β†’ funext 𝓀 𝓀 β†’ funext 𝓀 𝓀₀
                 β†’ (βˆƒ \(_β™―_ : X β†’ X β†’ 𝓀 Μ‡ ) β†’ is-apartness _β™―_ Γ— is-tight _β™―_) β†’ is-separated X
 tight-separated' {𝓀} {X} fe feβ‚€ = βˆ₯βˆ₯-rec (is-prop-separated fe feβ‚€) f
   where
    f : (Ξ£ \(_β™―_ : X β†’ X β†’ 𝓀 Μ‡ ) β†’ is-apartness _β™―_ Γ— is-tight _β™―_) β†’ is-separated X
    f (_β™―_ , a , t) = tight-is-separated _β™―_ a t

 tight-is-set' : {X : 𝓀 Μ‡ } β†’ funext 𝓀 𝓀 β†’ funext 𝓀 𝓀₀
           β†’ (βˆƒ \(_β™―_ : X β†’ X β†’ 𝓀 Μ‡ ) β†’ is-apartness _β™―_ Γ— is-tight _β™―_) β†’ is-set X
 tight-is-set' {𝓀} {X} fe feβ‚€ = βˆ₯βˆ₯-rec (being-set-is-a-prop fe) f
   where
    f : (Ξ£ \(_β™―_ : X β†’ X β†’ 𝓀 Μ‡ ) β†’ is-apartness _β™―_ Γ— is-tight _β™―_) β†’ is-set X
    f (_β™―_ , a , t) = tight-is-set feβ‚€ _β™―_ a t

\end{code}

 A map is called strongly extensional if it reflects apartness.

\begin{code}

 strongly-extensional : βˆ€ {𝓣} {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡}
                      β†’ (X β†’ X β†’ 𝓦 Μ‡ ) β†’ (Y β†’ Y β†’ 𝓣 Μ‡) β†’ (X β†’ Y) β†’ 𝓀 βŠ” 𝓦 βŠ” 𝓣 Μ‡
 strongly-extensional _β™―_ _β™―'_ f = βˆ€ {x x'} β†’ f x β™―' f x' β†’ x β™― x'

 preserves : βˆ€ {𝓣} {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡}
          β†’ (X β†’ X β†’ 𝓦 Μ‡ ) β†’ (Y β†’ Y β†’ 𝓣 Μ‡) β†’ (X β†’ Y) β†’ 𝓀 βŠ” 𝓦 βŠ” 𝓣 Μ‡
 preserves R S f = βˆ€ {x x'} β†’ R x x' β†’ S (f x) (f x')

 module TightReflection
          (fe : FunExt)
          (pe : propext π“₯)
          (X : 𝓀 Μ‡ )
          (_β™―_ : X β†’ X β†’ π“₯ Μ‡ )
          (β™―p : is-prop-valued _β™―_)
          (β™―i : is-irreflexive _β™―_)
          (β™―s : is-symmetric _β™―_)
          (β™―c : is-cotransitive _β™―_)
   where

\end{code}

  We now name the standard is-equivalence relation induced by _β™―_.

\begin{code}

  _~_ : X β†’ X β†’ π“₯ Μ‡
  x ~ y = Β¬(x β™― y)

\end{code}

  For certain purposes we need the apartness axioms packed in to a
  single axiom.

\begin{code}

  β™―a : is-apartness _β™―_
  β™―a = (β™―p , β™―i , β™―s , β™―c)

\end{code}

  Initially we tried to work with the function apart : X β†’ (X β†’ π“₯ Μ‡ )
  defined by apart = _β™―_. However, at some point in the development
  below it was difficult to proceed, when we need that the identity
  type apart x = apart y is a proposition. This should be the case
  because _β™―_ is is-prop-valued. The most convenient way to achieve this
  is to restrict the codomain of apart from V to Ξ©, so that the
  codomain of apart is a set.

\begin{code}

  apart : X β†’ (X β†’ Ξ© π“₯)
  apart x y = x β™― y , β™―p x y

\end{code}

  The following is an immediate consequence of the fact that two
  equivalent elements have the same apartness class, using functional
  and propositional extensionality.

\begin{code}

  apart-lemma : (x y : X) β†’ x ~ y β†’ apart x ≑ apart y
  apart-lemma x y na = dfunext (fe 𝓀 (π“₯ ⁺)) h
   where
    f : (z : X) β†’ x β™― z ⇔ y β™― z
    f = not-apart-have-same-apart x y _β™―_ β™―a na

    g : (z : X) β†’ x β™― z ≑ y β™― z
    g z = pe (β™―p x z) (β™―p y z) (pr₁ (f z)) (prβ‚‚ (f z))

    h : (z : X) β†’ apart x z ≑ apart y z
    h z = to-Ξ£-≑ (g z , being-a-prop-is-a-prop (fe π“₯ π“₯) _ _)

\end{code}

  We now construct the tight reflection of (X,β™―) to get (X',β™―')
  together with a universal strongly extensional map from X into
  tight apartness types. We take X' to be the image of the apart map.

\begin{code}

  open ImageAndSurjection pt

  X' : 𝓀 βŠ” π“₯ ⁺ Μ‡
  X' = image apart

\end{code}

The type X may or may not be a set, but its tight reflection is
necessarily a set, and we can see this before we define a tight
apartness on it.

\begin{code}

  X'-is-set : is-set X'
  X'-is-set = subsets-of-sets-are-sets (X β†’ Ξ© π“₯) _ (powersets-are-sets (fe 𝓀 (π“₯ ⁺)) (fe π“₯ π“₯) pe) βˆ₯βˆ₯-is-a-prop

  Ξ· : X β†’ X'
  Ξ· = corestriction apart

\end{code}

  The following induction principle is our main tool. Its uses look
  convoluted at times by the need to show that the property one is
  doing induction over is is-prop-valued. Typically this involves the use
  of the fact the propositions form an exponential ideal, and, more
  generally, are closed under products.

\begin{code}

  Ξ·-surjection : is-surjection Ξ·
  Ξ·-surjection = corestriction-surjection apart

  Ξ·-induction : (P : X' β†’ 𝓦 Μ‡ )
             β†’ ((x' : X') β†’ is-prop(P x'))
             β†’ ((x : X) β†’ P(Ξ· x))
             β†’ (x' : X') β†’ P x'
  Ξ·-induction = surjection-induction Ξ· Ξ·-surjection

\end{code}

  The apartness relation _β™―'_ on X' is defined as follows.

\begin{code}

  _β™―'_ : X' β†’ X' β†’ 𝓀 βŠ” π“₯ ⁺ Μ‡
  (u , _) β™―' (v , _) = βˆƒ \(x : X) β†’ Ξ£ \(y : X) β†’ (x β™― y) Γ— (apart x ≑ u) Γ— (apart y ≑ v)

\end{code}

  Then Ξ· preserves and reflects apartness.

\begin{code}

  Ξ·-preserves-apartness : preserves _β™―_ _β™―'_ Ξ·
  η-preserves-apartness {x} {y} a = ∣ x , y , a , refl , refl ∣

  Ξ·-strongly-extensional : strongly-extensional _β™―_ _β™―'_ Ξ·
  Ξ·-strongly-extensional {x} {y} = βˆ₯βˆ₯-rec (β™―p x y) g
   where
    g : (Ξ£ \(x' : X) β†’ Ξ£ \(y' : X) β†’ (x' β™― y') Γ— (apart x' ≑ apart x) Γ— (apart y' ≑ apart y))
      β†’ x β™― y
    g (x' , y' , a , p , q) = β™―s _ _ (j (β™―s _ _ (i a)))
     where
      i : x' β™― y' β†’ x β™― y'
      i = idtofun _ _ (ap pr₁ (happly p y'))

      j : y' β™― x β†’ y β™― x
      j = idtofun _ _ (ap pr₁ (happly q x))

\end{code}

  Of course, we must check that _β™―'_ is indeed an apartness
  relation. We do this by Ξ·-induction. These proofs by induction need
  routine proofs that some things are propositions. We include the
  following abbreviation `fuv` to avoid some long lines in such
  proofs.

\begin{code}

  fuv : funext (𝓀 βŠ” π“₯ ⁺) (𝓀 βŠ” π“₯ ⁺)
  fuv = fe (𝓀 βŠ” π“₯ ⁺) (𝓀 βŠ” π“₯ ⁺)

  β™―'p : is-prop-valued _β™―'_
  β™―'p _ _ = βˆ₯βˆ₯-is-a-prop

  β™―'i : is-irreflexive _β™―'_
  β™―'i = by-induction
   where
    induction-step : βˆ€ x β†’ Β¬(Ξ· x β™―' Ξ· x)
    induction-step x a = β™―i x (Ξ·-strongly-extensional a)

    by-induction : _
    by-induction = Ξ·-induction (Ξ» x' β†’ Β¬ (x' β™―' x'))
                      (Ξ» _ β†’ Ξ -is-prop (fe (𝓀 βŠ” π“₯ ⁺) 𝓀₀) (Ξ» _ β†’ 𝟘-is-prop))
                      induction-step

  β™―'s : is-symmetric _β™―'_
  β™―'s = by-nested-induction
   where
    induction-step : βˆ€ x y β†’ Ξ· x β™―' Ξ· y β†’ Ξ· y β™―' Ξ· x
    induction-step x y a = Ξ·-preserves-apartness(β™―s x y (Ξ·-strongly-extensional a))

    by-nested-induction : _
    by-nested-induction =
      Ξ·-induction (Ξ» x' β†’ βˆ€ y' β†’ x' β™―' y' β†’ y' β™―' x')
       (Ξ» x' β†’ Ξ -is-prop fuv
                (Ξ» y' β†’ Ξ -is-prop fuv (Ξ» _ β†’ β™―'p y' x')))
       (Ξ» x β†’ Ξ·-induction (Ξ» y' β†’ Ξ· x β™―' y' β†’ y' β™―' Ξ· x)
                (Ξ» y' β†’ Ξ -is-prop fuv (Ξ» _ β†’ β™―'p y' (Ξ· x)))
                (induction-step x))

  β™―'c : is-cotransitive _β™―'_
  β™―'c = by-nested-induction
   where
    induction-step : βˆ€ x y z β†’ Ξ· x β™―' Ξ· y β†’ Ξ· x β™―' Ξ· z ∨ Ξ· y β™―' Ξ· z
    induction-step x y z a = βˆ₯βˆ₯-functor c b
     where
      a' : x β™― y
      a' = Ξ·-strongly-extensional a

      b : x β™― z ∨ y β™― z
      b = β™―c x y z a'

      c : (x β™― z) + (y β™― z) β†’ (Ξ· x β™―' Ξ· z) + (Ξ· y β™―' Ξ· z)
      c (inl e) = inl (Ξ·-preserves-apartness e)
      c (inr f) = inr (Ξ·-preserves-apartness f)

    by-nested-induction : _
    by-nested-induction =
      Ξ·-induction (Ξ» x' β†’ βˆ€ y' z' β†’ x' β™―' y' β†’ (x' β™―' z') ∨ (y' β™―' z'))
       (Ξ» _ β†’ Ξ -is-prop fuv
                (Ξ» _ β†’ Ξ -is-prop fuv
                         (Ξ» _ β†’ Ξ -is-prop fuv (Ξ» _ β†’ βˆ₯βˆ₯-is-a-prop))))
       (Ξ» x β†’ Ξ·-induction (Ξ» y' β†’ βˆ€ z' β†’ Ξ· x β™―' y' β†’ (Ξ· x β™―' z') ∨ (y' β™―' z'))
                (Ξ» _ β†’ Ξ -is-prop fuv
                         (Ξ» _ β†’ Ξ -is-prop fuv (Ξ» _ β†’ βˆ₯βˆ₯-is-a-prop)))
                (Ξ» y β†’ Ξ·-induction (Ξ» z' β†’ Ξ· x β™―' Ξ· y β†’ (Ξ· x β™―' z') ∨ (Ξ· y β™―' z'))
                         (Ξ» _ β†’ Ξ -is-prop fuv (Ξ» _ β†’ βˆ₯βˆ₯-is-a-prop))
                         (induction-step x y)))

  β™―'a : is-apartness _β™―'_
  β™―'a = (β™―'p , β™―'i , β™―'s , β™―'c)

\end{code}

  The tightness of _β™―'_ cannot by proved by induction by reduction to
  properties of _β™―_, as above, because _β™―_ is not (necessarily)
  tight. We need to work with the definitions of X' and _β™―'_ directly.

\begin{code}

  β™―'t : is-tight _β™―'_
  β™―'t (u , e) (v , f) n = βˆ₯βˆ₯-rec X'-is-set (Ξ» Οƒ β†’ βˆ₯βˆ₯-rec X'-is-set (h Οƒ) f) e
   where
    h : (Ξ£ \(x : X) β†’ apart x ≑ u) β†’ (Ξ£ \(y : X) β†’ apart y ≑ v) β†’ (u , e) ≑ (v , f)
    h (x , p) (y , q) = to-Ξ£-≑ (t , βˆ₯βˆ₯-is-a-prop _ _)
     where
      remark : (βˆƒ \(x : X) β†’ Ξ£ \(y : X) β†’ (x β™― y) Γ— (apart x ≑ u) Γ— (apart y ≑ v)) β†’ 𝟘
      remark = n

      r : x β™― y β†’ 𝟘
      r a = n ∣ x , y , a , p , q ∣

      s : apart x ≑ apart y
      s = apart-lemma x y r

      t : u ≑ v
      t = p ⁻¹ βˆ™ s βˆ™ q

\end{code}

  The tightness of _β™―'_ gives that Ξ· maps equivalent elements to equal
  elements, and its irreflexity gives that elements with the same Ξ·
  image are equivalent.

\begin{code}

  Ξ·-equiv-equal : {x y : X} β†’ x ~ y β†’ Ξ· x ≑ Ξ· y
  Ξ·-equiv-equal = β™―'t _ _ ∘ contrapositive Ξ·-strongly-extensional

  Ξ·-equal-equiv : {x y : X} β†’ Ξ· x ≑ Ξ· y β†’ x ~ y
  Ξ·-equal-equiv {x} {y} p a = β™―'i (Ξ· y) (transport (Ξ» - β†’ - β™―' Ξ· y) p (Ξ·-preserves-apartness a))

\end{code}

  We now show that the above data provide the tight reflection, or
  universal strongly extensional map from X to tight apartness types,
  where unique existence is expressed by by saying that a Ξ£ type is a
  singleton, as usual in univalent mathematics and homotopy type
  theory. Notice the use of Ξ·-induction to avoid dealing directly with
  the details of the constructions performed above.

\begin{code}

  tight-reflection : βˆ€ {𝓣} (A : 𝓦 Μ‡ ) (_♯ᴬ_ : A β†’ A β†’ 𝓣 Μ‡)
                   β†’ is-apartness _♯ᴬ_
                   β†’ is-tight _♯ᴬ_
                   β†’ (f : X β†’ A)
                   β†’ strongly-extensional _β™―_ _♯ᴬ_ f
                   β†’ βˆƒ! \(f' : X' β†’ A) β†’ f' ∘ Ξ· ≑ f
  tight-reflection {𝓦} {𝓣} A  _♯ᴬ_  ♯ᴬa  ♯ᴬt  f  se = ic
   where
    iss : is-set A
    iss = tight-is-set (fe 𝓦 𝓀₀) _♯ᴬ_ ♯ᴬa ♯ᴬt

    i : {x y : X} β†’ x ~ y β†’ f x ≑ f y
    i = ♯ᴬt _ _ ∘ contrapositive se

    Ο† : (x' : X') β†’ is-prop (Ξ£ \a β†’ βˆƒ \x β†’ (Ξ· x ≑ x') Γ— (f x ≑ a))
    Ο† = Ξ·-induction _ Ξ³ induction-step
      where
       induction-step : (y : X) β†’ is-prop (Ξ£ \a β†’ βˆƒ \x β†’ (Ξ· x ≑ Ξ· y) Γ— (f x ≑ a))
       induction-step x (a , d) (b , e) = to-Ξ£-≑ (p , βˆ₯βˆ₯-is-a-prop _ _)
        where
         h : (Ξ£ \x' β†’ (Ξ· x' ≑ Ξ· x) Γ— (f x' ≑ a))
           β†’ (Ξ£ \y' β†’ (Ξ· y' ≑ Ξ· x) Γ— (f y' ≑ b))
           β†’ a ≑ b
         h (x' , r , s) (y' , t , u) = s ⁻¹ βˆ™ i (Ξ·-equal-equiv (r βˆ™ t ⁻¹)) βˆ™ u

         p : a ≑ b
         p = βˆ₯βˆ₯-rec iss (Ξ» Οƒ β†’ βˆ₯βˆ₯-rec iss (h Οƒ) e) d

       Ξ³ : (x' : X') β†’ is-prop (is-prop (Ξ£ \a β†’ βˆƒ \x β†’ (Ξ· x ≑ x') Γ— (f x ≑ a)))
       Ξ³ x' = being-a-prop-is-a-prop (fe (𝓀 βŠ” (π“₯ ⁺) βŠ” 𝓦) (𝓀 βŠ” (π“₯ ⁺) βŠ” 𝓦))

    k : (x' : X') β†’ Ξ£ \(a : A) β†’ βˆƒ \(x : X) β†’ (Ξ· x ≑ x') Γ— (f x ≑ a)
    k = Ξ·-induction _ Ο† induction-step
     where
      induction-step : (y : X) β†’ Ξ£ \a β†’ βˆƒ \x β†’ (Ξ· x ≑ Ξ· y) Γ— (f x ≑ a)
      induction-step x = f x , ∣ x , refl , refl ∣

    f' : X' β†’ A
    f' x' = pr₁(k x')

    r : f' ∘ Ξ· ≑ f
    r = dfunext (fe 𝓀 𝓦) h
     where
      g : (y : X) β†’ βˆƒ \x β†’ (Ξ· x ≑ Ξ· y) Γ— (f x ≑ f' (Ξ· y))
      g y = prβ‚‚(k(Ξ· y))

      j : (y : X) β†’ (Ξ£ \x β†’ (Ξ· x ≑ Ξ· y) Γ— (f x ≑ f' (Ξ· y))) β†’ f'(Ξ· y) ≑ f y
      j y (x , p , q) = q ⁻¹ βˆ™ i (Ξ·-equal-equiv p)

      h : (y : X) β†’ f'(Ξ· y) ≑ f y
      h y = βˆ₯βˆ₯-rec iss (j y) (g y)

    c : (Οƒ : Ξ£ \(f'' : X' β†’ A) β†’ f'' ∘ Ξ· ≑ f) β†’ (f' , r) ≑ Οƒ
    c (f'' , s) = to-Ξ£-≑ (t , v)
     where
      w : βˆ€ x β†’ f'(Ξ· x) ≑ f''(Ξ· x)
      w = happly (r βˆ™ s ⁻¹)

      t : f' ≑ f''
      t = dfunext (fe (𝓀 βŠ” π“₯ ⁺) 𝓦) (Ξ·-induction _ (Ξ» _ β†’ iss) w)

      u : f'' ∘ Ξ· ≑ f
      u = transport (Ξ» - β†’ - ∘ Ξ· ≑ f) t r

      v : u ≑ s
      v = Ξ -is-set (fe 𝓀 𝓦) (Ξ» _ β†’ iss) u s

    ic : βˆƒ! \(f' : X' β†’ A) β†’ f' ∘ Ξ· ≑ f
    ic = (f' , r) , c

\end{code}

  The following is an immediate consequence of the tight reflection,
  by the usual categorical argument, using the fact that the identity
  map is strongly extensional (with the identity function as the
  proof). Notice that our construction of the reflection produces a
  result in a universe higher than those where the starting data are,
  to avoid impredicativity (aka propositional resizing). Nevertheless,
  the usual categorical argument is applicable.

  A direct proof that doesn't rely on the tight reflection is equally
  short in this case, and is also included.

  What the following construction says is that if _β™―_ is tight, then
  any element of X is uniquely determined by the set of elements apart
  from it.

\begin{code}

  tight-Ξ·-equiv-abstract-nonsense : is-tight _β™―_ β†’ X ≃ X'
  tight-Ξ·-equiv-abstract-nonsense β™―t = Ξ· , (ΞΈ , happly pβ‚„) , (ΞΈ , happly pβ‚€)
   where
    u : βˆƒ! \(ΞΈ : X' β†’ X) β†’ ΞΈ ∘ Ξ· ≑ id
    u = tight-reflection X _β™―_ β™―a β™―t id id

    v : βˆƒ! \(ΞΆ : X' β†’ X') β†’ ΞΆ ∘ Ξ· ≑ Ξ·
    v = tight-reflection X' _β™―'_ β™―'a β™―'t Ξ· Ξ·-strongly-extensional

    ΞΈ : X' β†’ X
    ΞΈ = pr₁(pr₁ u)

    ΞΆ : X' β†’ X'
    ΞΆ = pr₁(pr₁ v)

    Ο† : (ΞΆ' : X' β†’ X') β†’ ΞΆ' ∘ Ξ· ≑ Ξ· β†’ ΞΆ ≑ ΞΆ'
    Ο† ΞΆ' p = ap pr₁ (prβ‚‚ v (ΞΆ' , p))

    pβ‚€ : ΞΈ ∘ Ξ· ≑ id
    pβ‚€ = prβ‚‚(pr₁ u)

    p₁ : Ξ· ∘ ΞΈ ∘ Ξ· ≑ Ξ·
    p₁ = ap (_∘_ Ξ·) pβ‚€

    pβ‚‚ : ΞΆ ≑ Ξ· ∘ ΞΈ
    pβ‚‚ = Ο† (Ξ· ∘ ΞΈ) p₁

    p₃ : ΞΆ ≑ id
    p₃ = Ο† id refl

    pβ‚„ : Ξ· ∘ ΞΈ ≑ id
    pβ‚„ = pβ‚‚ ⁻¹ βˆ™ p₃

  tight-Ξ·-equiv-direct : is-tight _β™―_ β†’ X ≃ X'
  tight-Ξ·-equiv-direct t = (Ξ· , vv-equivs-are-equivs Ξ· cm)
   where
    lc : left-cancellable Ξ·
    lc {x} {y} p = i h
     where
      i : Β¬ (Ξ· x β™―' Ξ· y) β†’ x ≑ y
      i = t x y ∘ contrapositive (η-preserves-apartness {x} {y})

      h : Β¬(Ξ· x β™―' Ξ· y)
      h a = β™―'i (Ξ· y) (transport (Ξ» - β†’ - β™―' Ξ· y) p a)

    e : is-embedding Ξ·
    e =  lc-maps-into-sets-are-embeddings Ξ· lc X'-is-set

    cm : is-vv-equiv Ξ·
    cm = prβ‚‚ (c-es Ξ·) (e , Ξ·-surjection)

\end{code}

TODO.

* The tight reflection has the universal property of the quotient by
  _~_. Conversely, the quotient by _~_ gives the tight reflection.

* The tight reflection of β™―β‚‚ has the universal property of the totally
  separated reflection.