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

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.