Martin Escardo, 5th September 2018.

On Lawvere's Fixed Point Theorem (LFPT).

* http://tac.mta.ca/tac/reprints/articles/15/tr15abs.html
* https://ncatlab.org/nlab/show/Lawvere%27s+fixed+point+theorem
* http://arxiv.org/abs/math/0305282

We give an application to Cantor's theorem for the universe.

We begin with split surjections, or retractions, because they can be
formulated in MLTT, and then move to surjections, which need further
extensions of MLTT, or hypotheses, such as propositional truncation.

Many other things have been added since the above abstract was
written.

\begin{code}

{-# OPTIONS --without-K --exact-split --safe --no-sized-types --no-guardedness --auto-inline #-}

module Various.LawvereFPT where

open import MLTT.Spartan

open import MLTT.Two-Properties
open import Naturals.Properties

open import UF.Base
open import UF.Embeddings
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.Retracts
open import UF.Equiv
open import UF.Miscelanea
open import UF.FunExt
open import UF.Size

designated-fixed-point-property : 𝓤 ̇ → 𝓤 ̇
designated-fixed-point-property X = (f : X → X) → Σ x ꞉ X , x ＝ f x

module retract-version where

\end{code}

The following pointwise weakening of split surjection is sufficient to
prove LFPT and allows us to avoid function extensionality in its
applications:

We will use the decoration "·" for pointwise versions of notions and
constructions (for example, we can read "has-section· r" as saying
that r has a pointwise section).

\begin{code}

has-section· : {A : 𝓤 ̇ } {X : 𝓥 ̇ } → (A → (A → X)) → 𝓤 ⊔ 𝓥 ̇
has-section· r = Σ s ꞉ (codomain r → domain r) , ∀ g a → r (s g) a ＝ g a

section-gives-section· : {A : 𝓤 ̇ }
{X : 𝓥 ̇ }
(r : A → (A → X))
→ has-section r
→ has-section· r
section-gives-section· r (s , rs) = s , λ g a → ap (λ - → - a) (rs g)

section·-gives-section : funext 𝓤 𝓥
→ {A : 𝓤 ̇ }
{X : 𝓥 ̇ }
(r : A → (A → X))
→ has-section· r
→ has-section r
section·-gives-section fe r (s , rs·) = s , λ g → dfunext fe (rs· g)

LFPT· : {A : 𝓤 ̇ }
{X : 𝓥 ̇ }
(r : A → (A → X))
→ has-section· r
→ designated-fixed-point-property X
LFPT· {𝓤} {𝓥} {A} {X} r (s , rs) f = x , p
where
g : A → X
g a = f (r a a)

a : A
a = s g

x : X
x = r a a

p : x ＝ f x
p = x         ＝⟨ refl ⟩
r (s g) a ＝⟨ rs g a ⟩
g a       ＝⟨ refl ⟩
f x       ∎

LFPT : {A : 𝓤 ̇ }
{X : 𝓥 ̇ }
→ retract (A → X) of A
→ designated-fixed-point-property X
LFPT (r , h) = LFPT· r (section-gives-section· r h)

LFPT-≃ : {A : 𝓤 ⊔ 𝓥 ̇ }
{X : 𝓤 ̇ }
→ A ≃ (A → X)
→ designated-fixed-point-property X
LFPT-≃ p = LFPT (≃-gives-▷ p)

LFPT-＝ : {A : 𝓤 ⊔ 𝓥 ̇ } {X : 𝓤 ̇ }
→ A ＝ (A → X)
→ designated-fixed-point-property X
LFPT-＝ p = LFPT (Id-retract-r p)

\end{code}

As a simple application, it follows that negation doesn't have fixed points:

\begin{code}

¬-no-fp : ¬ (Σ X ꞉ 𝓤 ̇ , X ＝ ¬ X)
¬-no-fp {𝓤} (X , p) = pr₁ (γ id)
where
γ : designated-fixed-point-property 𝟘
γ = LFPT-＝ p

\end{code}

We apply LFPT twice to get the following: first every function
𝓤 ̇ → 𝓤 ̇ has a fixed point, from which for any type X we get a type B
with B ＝ (B → X), and hence with (B → X) a retract of B, for which we
apply LFPT again to get that every X → X has a fixed point.

\begin{code}

cantor-theorem-for-universes : (A : 𝓥 ̇ )
(r : A → (A → 𝓤 ̇ ))
→ has-section· r
→ (X : 𝓤 ̇ ) → designated-fixed-point-property X
cantor-theorem-for-universes {𝓥} {𝓤} A r h X = LFPT-＝ {𝓤} {𝓤} p
where
B : 𝓤 ̇
B = pr₁ (LFPT· r h (λ B → B → X))

p : B ＝ (B → X)
p = pr₂ (LFPT· r h (λ B → B → X))

\end{code}

Taking X to be 𝟘 we get a contradiction, i.e. an inhabitant of the
empty type 𝟘 (in fact, we get an inhabitant of any type by considering
the identity function):

\begin{code}

Cantor-theorem-for-universes : (A : 𝓥 ̇ )
(r : A → (A → 𝓤 ̇ ))
→ ¬ has-section· r
Cantor-theorem-for-universes A r h =
𝟘-elim (pr₁ (cantor-theorem-for-universes A r h 𝟘 id))

Cantor-theorem-for-universes-corollary : ¬ (𝓤 ̇ ≃ (𝓤 ̇ → 𝓤 ̇ ))
Cantor-theorem-for-universes-corollary {𝓤} 𝕗 =
Cantor-theorem-for-universes (𝓤 ̇ ) ⌜ 𝕗 ⌝
(section-gives-section· ⌜ 𝕗 ⌝
(equivs-have-sections ⌜ 𝕗 ⌝ (⌜⌝-is-equiv 𝕗)))

\end{code}

The original version of Cantor's theorem was for powersets, which
here are types of maps into the subtype classifier Ω 𝓤 of the universe 𝓤.

Function extensionality is needed in order to define negation
Ω 𝓤 → Ω 𝓤, to show that P → 𝟘 is a proposition.

\begin{code}

open import UF.Subsingletons
open import UF.Subsingletons-FunExt

not-no-fp : (fe : funext 𝓤 𝓤₀) → ¬ (Σ P ꞉ Ω 𝓤 , P ＝ not fe P)
not-no-fp {𝓤} fe (P , p) = ¬-no-fp (P holds , q)
where
q : P holds ＝ ¬ (P holds)
q = ap _holds p

cantor-theorem : funext 𝓤 𝓤₀
→ (A : 𝓥 ̇ )
→ (r : A → (A → Ω 𝓤))
→ ¬ has-section· r
cantor-theorem {𝓤} fe A r (s , rs) = not-no-fp fe not-fp
where
not-fp : Σ B ꞉ Ω 𝓤 , B ＝ not fe B
not-fp = LFPT· r (s , rs) (not fe)

\end{code}

The original LFPT has surjection, rather than retraction, as an
assumption. The retraction version can be formulated and proved in
pure MLTT. To formulate the original version we consider MLTT extended
with propositional truncation, or rather just MLTT with propositional
truncation as an assumption, given as a parameter for the following
module. This time a pointwise weakening of surjection is not enough.

\begin{code}

open import UF.PropTrunc

module surjection-version (pt : propositional-truncations-exist) where

open PropositionalTruncation pt
open import UF.ImageAndSurjection pt

existential-fixed-point-property : 𝓤 ̇ → 𝓤 ̇
existential-fixed-point-property X = (f : X → X) → ∃ x ꞉ X , x ＝ f x

LFPT : {A : 𝓤 ̇ } {X : 𝓥 ̇ } (φ : A → (A → X))
→ is-surjection φ
→ existential-fixed-point-property X
LFPT {𝓤} {𝓥} {A} {X} φ s f = ∥∥-functor γ e
where
g : A → X
g a = f (φ a a)

e : ∃ a ꞉ A , φ a ＝ g
e = s g

γ : (Σ a ꞉ A , φ a ＝ g) → Σ x ꞉ X , x ＝ f x
γ (a , q) = x , p
where
x : X
x = φ a a

p : x ＝ f x
p = x         ＝⟨ refl ⟩
φ a a     ＝⟨ ap (λ - → - a) q ⟩
g a       ＝⟨ refl ⟩
f x       ∎

\end{code}

So in this version of LFPT we have a weaker hypothesis for the
theorem, but we need a stronger language to formulate and prove it,
or else an additional hypothesis of the existence of propositional
truncations.

For the following theorem, we use both the surjection version and the
retraction version of LFPT.

\begin{code}

cantor-theorem-for-universes : (A : 𝓥 ̇ )
(φ : A → (A → 𝓤 ̇ ))
→ is-surjection φ
→ (X : 𝓤 ̇ ) → existential-fixed-point-property X
cantor-theorem-for-universes {𝓥} {𝓤} A φ s X f = ∥∥-functor g t
where
t : ∃ B ꞉ 𝓤 ̇  , B ＝ (B → X)
t = LFPT φ s (λ B → B → X)

g : (Σ B ꞉ 𝓤 ̇ , B ＝ (B → X)) → Σ x ꞉ X , x ＝ f x
g (B , p) = retract-version.LFPT-＝ {𝓤} {𝓤} p f

Cantor-theorem-for-universes : (A : 𝓥 ̇ )
→ (φ : A → (A → 𝓤 ̇ ))
→ ¬ is-surjection φ
Cantor-theorem-for-universes A r h = γ
where
c : ∃ x ꞉ 𝟘 , x ＝ x
c = cantor-theorem-for-universes A r h 𝟘 id

γ : 𝟘
γ = 𝟘-elim (∥∥-rec 𝟘-is-prop pr₁ c)

cantor-theorem : funext 𝓤 𝓤₀
→ (A : 𝓥 ̇ )
(φ : A → (A → Ω 𝓤))
→ ¬ is-surjection φ
cantor-theorem {𝓤} {𝓥} fe A φ s = γ
where
t : ∃ B ꞉ Ω 𝓤 , B ＝ not fe B
t = LFPT φ s (not fe)

γ : 𝟘
γ = ∥∥-rec 𝟘-is-prop (retract-version.not-no-fp fe) t

\end{code}

Another corollary is that the Cantor type (ℕ → 𝟚) and the Baire type
(ℕ → ℕ) are uncountable:

\begin{code}

open import MLTT.Two

cantor-uncountable : ¬ (Σ φ ꞉ (ℕ → (ℕ → 𝟚)), is-surjection φ)
cantor-uncountable (φ , s) = γ
where
t : ∃ n ꞉ 𝟚 , n ＝ complement n
t = LFPT φ s complement

γ : 𝟘
γ = ∥∥-rec 𝟘-is-prop (uncurry complement-no-fp) t

baire-uncountable : ¬ (Σ φ ꞉ (ℕ → (ℕ → ℕ)), is-surjection φ)
baire-uncountable (φ , s) = ∥∥-rec 𝟘-is-prop (uncurry succ-no-fp) t
where
t : ∃ n ꞉ ℕ , n ＝ succ n
t = LFPT φ s succ

\end{code}

The following proofs are originally due to Ingo Blechschmidt during
the Autumn School "Proof and Computation", Fischbachau, 2018, after I
posed the problem of showing that the universe is uncountable to
him. This version is an adaptation jointly developed by the two of us
to use LFPT, also extended to replace "discrete" by "set" at the cost
of "jumping" a universe.

\begin{code}

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

open PropositionalTruncation pt
open import UF.ImageAndSurjection pt
open import TypeTopology.DiscreteAndSeparated

Π-projection-has-section : {X : 𝓤 ̇ } {Y : X → 𝓥 ̇ }
(x₀ : X)
→ is-isolated x₀
→ Π Y
→ has-section (λ (f : Π Y) → f x₀)
Π-projection-has-section {𝓤} {𝓥} {X} {Y} x₀ i g = s , rs
where
s : Y x₀ → Π Y
s y x = Cases (i x)
(λ (p : x₀ ＝ x) → transport Y p y)
(λ (_ : x₀ ≠ x) → g x)

rs : (y : Y x₀) → s y x₀ ＝ y
rs y = ap (λ - → Cases - _ _) a
where
a : i x₀ ＝ inl refl
a = isolated-inl x₀ i x₀ refl

udr-lemma : {A : 𝓤 ̇ } (X : A → 𝓥 ̇ ) (B : 𝓦 ̇ )
(a₀ : A)
→ is-isolated a₀
→ B
→ retract ((a : A) → X a → B) of X a₀
→ designated-fixed-point-property B
udr-lemma X B a₀ i b ρ = γ
where
ρ' : retract (X a₀ → B) of X a₀
ρ' = retracts-compose ρ ((λ f → f a₀) , Π-projection-has-section a₀ i (λ a x → b))

γ : designated-fixed-point-property B
γ = retract-version.LFPT ρ'

universe-discretely-regular' : (A : 𝓤 ̇ ) (X : A → 𝓤 ⊔ 𝓥 ̇ )
→ is-discrete A
→ Σ B ꞉ 𝓤 ⊔ 𝓥 ̇ , ((a : A) → ¬ (X a ≃ B))
universe-discretely-regular' {𝓤} {𝓥} A X d  = γ
where
B : 𝓤 ⊔ 𝓥 ̇
B = (a : A) → X a → 𝟚

φ : (a : A) → ¬ (X a ≃ B)
φ a p = uncurry complement-no-fp (δ complement)
where
ρ : retract B of (X a)
ρ = ≃-gives-▷ p

δ : designated-fixed-point-property 𝟚
δ = udr-lemma X 𝟚 a (d a) ₀ ρ

γ : Σ B ꞉ 𝓤 ⊔ 𝓥 ̇ , ((a : A) → ¬ (X a ≃ B))
γ = B , φ

universe-discretely-regular : {A : 𝓤 ̇ } (X : A → 𝓤 ⊔ 𝓥 ̇ )
→ is-discrete A
→ Σ B ꞉ 𝓤 ⊔ 𝓥 ̇ , ((a : A) → X a ≠ B)
universe-discretely-regular {𝓤} {𝓥} {A} X d = γ
where
δ : (Σ B ꞉ 𝓤 ⊔ 𝓥 ̇ , ((a : A) → ¬ (X a ≃ B)))
→ (Σ B ꞉ 𝓤 ⊔ 𝓥 ̇ , ((a : A) → X a ≠ B))
δ (B , φ) = B , (λ a → contrapositive (idtoeq (X a) B) (φ a))

γ : Σ B ꞉ 𝓤 ⊔ 𝓥 ̇ , ((a : A) → X a ≠ B)
γ = δ (universe-discretely-regular' {𝓤} {𝓥} A X d)

Universe-discretely-regular : {A : 𝓤 ̇ } (X : A → 𝓤 ⊔ 𝓥 ̇ )
→ is-discrete A
→ ¬ is-surjection X
Universe-discretely-regular {𝓤} {𝓥} {A} X d s = ∥∥-rec 𝟘-is-prop n e
where
B : 𝓤 ⊔ 𝓥 ̇
B = pr₁ (universe-discretely-regular {𝓤} {𝓥} {A} X d)

φ : ∀ a → X a ≠ B
φ = pr₂ (universe-discretely-regular {𝓤} {𝓥} {A} X d)

e : ∃ a ꞉ A , X a ＝ B
e = s B

n : ¬ (Σ a ꞉ A , X a ＝ B)
n = uncurry φ

Universe-uncountable : {𝓤 : Universe} → ¬ (Σ X ꞉ (ℕ → 𝓤 ̇ ), is-surjection X)
Universe-uncountable (X , s) = Universe-discretely-regular X ℕ-is-discrete s

\end{code}

A variation, replacing discreteness by set-hood, at the cost of
"jumping a universe level".

\begin{code}

module Blechschmidt' (pt : propositional-truncations-exist) where

open PropositionalTruncation pt
open import UF.ImageAndSurjection pt
open import TypeTopology.DiscreteAndSeparated

Π-projection-has-section : funext 𝓥 ((𝓤 ⊔ 𝓦)⁺)
→ funext (𝓤 ⊔ 𝓦) (𝓤 ⊔ 𝓦)
→ propext (𝓤 ⊔ 𝓦)
→ {A : 𝓤 ̇ }
{X : A → 𝓥 ̇ }
(a₀ : A)
→ is-h-isolated a₀
→ has-section (λ (f : (a : A) → X a → Ω (𝓤 ⊔ 𝓦)) → f a₀)
Π-projection-has-section {𝓥} {𝓤} {𝓦} fe fe' pe {A} {X} a₀ ish = s , rs
where
s : (X a₀ → Ω (𝓤 ⊔ 𝓦)) → ((a : A) → X a → Ω (𝓤 ⊔ 𝓦))
s φ a x = (∃ p ꞉ a ＝ a₀ , φ (transport X p x) holds) , ∥∥-is-prop

rs : (φ : X a₀ → Ω (𝓤 ⊔ 𝓦)) → s φ a₀ ＝ φ
rs φ = dfunext fe γ
where
a : (x₀ : X a₀) → (∃ p ꞉ a₀ ＝ a₀ , φ (transport X p x₀) holds) → φ x₀ holds
a x₀ = ∥∥-rec (holds-is-prop (φ x₀)) f
where
f : (Σ p ꞉ a₀ ＝ a₀ , φ (transport X p x₀) holds) → φ x₀ holds
f (p , h) = transport _holds t h
where
r : p ＝ refl
r = ish p refl

t : φ (transport X p x₀) ＝ φ x₀
t = ap (λ - → φ (transport X - x₀)) r

b : (x₀ : X a₀) → φ x₀ holds → ∃ p ꞉ a₀ ＝ a₀ , φ (transport X p x₀) holds
b x₀ h = ∣ refl , h ∣

γ : (x₀ : X a₀) → (∃ p ꞉ a₀ ＝ a₀ , φ (transport X p x₀) holds) , ∥∥-is-prop ＝ φ x₀
γ x₀ = to-Σ-＝ (pe ∥∥-is-prop (holds-is-prop (φ x₀)) (a x₀) (b x₀) ,
being-prop-is-prop fe' (holds-is-prop _) (holds-is-prop (φ x₀)))

usr-lemma : funext 𝓥 ((𝓤 ⊔ 𝓦)⁺)
→ funext (𝓤 ⊔ 𝓦) (𝓤 ⊔ 𝓦)
→ propext (𝓤 ⊔ 𝓦)
→ {A : 𝓤 ̇ } (X : A → 𝓥 ̇ )
(a₀ : A)
→ is-h-isolated a₀
→ retract ((a : A) → X a → Ω (𝓤 ⊔ 𝓦)) of X a₀
→ designated-fixed-point-property (Ω (𝓤 ⊔ 𝓦))
usr-lemma {𝓥} {𝓤} {𝓦} fe fe' pe {A} X a₀ i ρ = retract-version.LFPT ρ'
where
ρ' : retract (X a₀ → Ω (𝓤 ⊔ 𝓦)) of X a₀
ρ' = retracts-compose ρ ((λ f → f a₀) , Π-projection-has-section {𝓥} {𝓤} {𝓦} fe fe' pe a₀ i)
\end{code}

We now work with the following assumptions:

\begin{code}

module _
(𝓤 𝓥     : Universe)
(fe'      : funext (𝓤 ⁺ ⊔ 𝓥) (𝓤 ⁺))
(fe       : funext 𝓤 𝓤)
(fe₀      : funext 𝓤 𝓤₀)
(pe       : propext 𝓤)
(A        : 𝓤 ̇ )
(A-is-set : is-set A)
(X        : A → 𝓤 ⁺ ⊔ 𝓥 ̇ )
where

\end{code}

We show that such an X cannot be a surjection.

NB. If 𝓥 is 𝓤 or 𝓤', then X : A → 𝓤 ⁺ ̇.

\begin{code}

universe-set-regular' : Σ B ꞉ 𝓤 ⁺ ⊔ 𝓥 ̇ , ((a : A) → ¬ (X a ≃ B))
universe-set-regular' = B , φ
where
B : 𝓤 ⁺ ⊔ 𝓥 ̇
B = (a : A) → X a → Ω 𝓤

φ : (a : A) → ¬ (X a ≃ B)
φ a p = retract-version.not-no-fp fe₀ (γ (not fe₀))
where
ρ : retract B of (X a)
ρ = ≃-gives-▷ p

γ : designated-fixed-point-property (Ω 𝓤)
γ = usr-lemma {(𝓤 ⁺) ⊔ 𝓥} {𝓤} {𝓤} fe' fe pe X a A-is-set ρ

universe-set-regular : Σ B ꞉ 𝓤 ⁺ ⊔ 𝓥 ̇ , ((a : A) → X a ≠ B)
universe-set-regular = γ universe-set-regular'
where
γ : (Σ B ꞉ 𝓤 ⁺ ⊔ 𝓥 ̇ , ((a : A) → ¬ (X a ≃ B)))
→ (Σ B ꞉ 𝓤 ⁺ ⊔ 𝓥 ̇ , ((a : A) → X a ≠ B))
γ (B , φ) = B , (λ a → contrapositive (idtoeq (X a) B) (φ a))

Universe-set-regular : ¬ is-surjection X
Universe-set-regular s = γ
where
B : 𝓤 ⁺ ⊔ 𝓥 ̇
B = pr₁ universe-set-regular

φ : ∀ a → X a ≠ B
φ = pr₂ universe-set-regular

e : ∃ a ꞉ A , X a ＝ B
e = s B

γ : 𝟘
γ = ∥∥-rec 𝟘-is-prop (uncurry φ) e

Universe-set-regular' : ¬ has-section X
Universe-set-regular' h = Universe-set-regular (retractions-are-surjections X h)

\end{code}

Added 12 October 2018. The paper

Thierry Coquand, The paradox of trees in type theory
BIT Numerical Mathematics, March 1992, Volume 32, Issue 1, pp 10–14
https://pdfs.semanticscholar.org/f2f3/30b27f1d7ca99c2550f96581a4400c209ef8.pdf

shows that 𝓤 ̇ : 𝓤 ̇ (aka type-in-type) is inconsistent if 𝓤 is closed
under W types.

We adapt this method of proof to show that there is no type 𝕌 : 𝓤 ̇
with 𝓤 ̇ ≃ 𝕌, without assuming type-in-type.

The construction works in MLTT with empty type 𝟘, identity types, Σ
types, Π types, W types and a universe 𝓤 closed under them. In
particular, extensionality and univalence are not needed. We again use
Lawvere's fixed point theorem.

TODO. It should also be possible to replace the diagonal construction
of Lemma₀ by a second application of LFPT.

\begin{code}

module GeneralizedCoquand where

Lemma₀ : (A : 𝓤 ̇ )
(T : A → 𝓤 ̇ )
(S : 𝓤 ̇ → A)
(ρ : {X : 𝓤 ̇ } → T (S X) → X)
(σ : {X : 𝓤 ̇ } → X → T (S X))
(η : {X : 𝓤 ̇ } (x : X) → ρ (σ x) ＝ x)
→ 𝟘
Lemma₀ {𝓤} A T S ρ σ η = γ
where
open import MLTT.W

𝕎 : 𝓤 ̇
𝕎 = W A T

α : 𝕎 → (𝕎 → 𝓤 ̇ )
α (sup _ φ) = fiber φ

module _ (X : 𝓤 ̇ ) where

H : 𝕎 → 𝓤 ̇
H w = α w w → X

R : 𝕎
R = sup (S (Σ H)) (pr₁ ∘ ρ)

B : 𝓤 ̇
B = α R R

r : B → (B → X)
r (t , p) = transport H p (pr₂ (ρ t))

s : (B → X) → B
s f = σ (R , f) , ap pr₁ (η (R , f))

rs : (f : B → X) → r (s f) ＝ f
rs f = r (s f)                                      ＝⟨ refl ⟩
transport H (ap pr₁ (η Rf)) (pr₂ (ρ (σ Rf))) ＝⟨ i ⟩
transport (H ∘ pr₁) (η Rf)  (pr₂ (ρ (σ Rf))) ＝⟨ ii ⟩
pr₂ Rf                                       ＝⟨ refl ⟩
f                                            ∎
where
Rf : Σ H
Rf = (R , f)

i = (transport-ap H pr₁ (η Rf))⁻¹
ii = apd pr₂ (η Rf)

δ : designated-fixed-point-property X
δ = retract-version.LFPT (r , s , rs)

γ : 𝟘
γ = pr₁ (δ 𝟘 id)

\end{code}

This can be rephrased as follows, where the use of 𝟘-elim is to
coerce the empty type in the universe 𝓤 to the empty type in the
universe 𝓤₀, which is where our negations take values:

\begin{code}

Lemma₁ : (A : 𝓤 ̇ ) (T : A → 𝓤 ̇ ) (S : 𝓤 ̇ → A)
→ ¬ ((X : 𝓤 ̇ ) → retract X of (T (S X)))
Lemma₁ A T S ρ = 𝟘-elim (Lemma₀ A T S
(λ {X} → retraction (ρ X))
(λ {X} → section (ρ X))
(λ {X} → retract-condition (ρ X)))

\end{code}

Because equivalences are retractions, it follows that

\begin{code}

Lemma₂ : (A : 𝓤 ̇ ) (T : A → 𝓤 ̇ ) (S : 𝓤 ̇ → A)
→ ¬ ((X : 𝓤 ̇ ) → T (S X) ≃ X)
Lemma₂ A T S e = Lemma₁ A T S (λ X → ≃-gives-▷ (e X))

\end{code}

And because identitities are equivalences, it follows that

\begin{code}

Lemma₃ : (A : 𝓤 ̇ ) (T : A → 𝓤 ̇ ) (S : 𝓤 ̇ → A)
→ ¬ ((X : 𝓤 ̇ ) → T (S X) ＝ X)
Lemma₃ A T S p = Lemma₂ A T S (λ X → idtoeq (T (S X)) X (p X))

\end{code}

This means that a universe 𝓤 cannot be a retract of any type in 𝓤:

\begin{code}

Lemma₄ : ¬ (Σ A ꞉ 𝓤 ̇ , retract 𝓤 ̇ of A)
Lemma₄ (A , T , S , TS) = Lemma₃ A T S TS

\end{code}

In particular, the successor universe 𝓤 ⁺ is not a retract of 𝓤:

\begin{code}

corollary : ∀ 𝓤 → ¬ (retract 𝓤 ⁺ ̇ of (𝓤 ̇ ))
corollary 𝓤 ρ = Lemma₄ ((𝓤 ̇ ) , ρ)

\end{code}

Therefore, because equivalences are retractions, no universe 𝓤 can be
equivalent to a type in 𝓤:

\begin{code}

Theorem : ¬ (Σ X ꞉ 𝓤 ̇ , 𝓤 ̇ ≃ X)
Theorem (X , e) = Lemma₄ (X , ≃-gives-◁ e)

\end{code}

And in particular, the successor universe 𝓤 ⁺ is not equivalent to 𝓤:

\begin{code}

Corollary : ¬ (𝓤 ⁺ ̇ ≃ 𝓤 ̇ )
Corollary {𝓤} e = Theorem ((𝓤 ̇ ), e)

\end{code}

Added 23rd December 2020, simplified 26th December after a suggestion by
Mike Shulman.

\begin{code}

global-invariance-under-≃-false :

((A : (𝓤 : Universe) → 𝓤 ̇ → 𝓤 ⁺ ̇ )
(𝓤 𝓥 : Universe)
(X : 𝓤 ̇ ) (Y : 𝓥 ̇ )
→ X ≃ Y → A 𝓤 X ≃ A 𝓥 Y)
→ 𝟘

global-invariance-under-≃-false h = γ
where
A : (𝓤 : Universe) → 𝓤 ̇ → 𝓤 ⁺ ̇
A 𝓤 _ = 𝓤 ̇

e : 𝟘 {𝓤₁} ≃ 𝟘 {𝓤₀}
e = qinveq 𝟘-elim (𝟘-elim , (λ x → 𝟘-elim x) , (λ x → 𝟘-elim x))

δ : (𝓤₁ ̇ ) ≃ (𝓤₀ ̇ )
δ = h A 𝓤₁ 𝓤₀ (𝟘 {𝓤₁}) (𝟘 {𝓤₀}) e

γ : 𝟘 {𝓤₀}
γ = Corollary δ

\end{code}

TODO. Can we change the type of A to {𝓤 : Universe} → 𝓤 ̇ → 𝓤 ̇?

Added 20th December 2020. The following is work in progress, probably
useless.

Further generalization, where we intend to use P = is-set.

\begin{code}

open import MLTT.W

module Coquand-further-generalized (𝓤 𝓥 : Universe)
(P : 𝓤 ̇ → 𝓥 ̇ )
(𝟘-is-P : P 𝟘)

(P-exponential-ideal : (X Y : 𝓤 ̇ ) → P X → P (Y → X))

(Σ-is-P : (X : 𝓤 ̇ ) (Y : X → 𝓤 ̇ )
→ P X
→ ((x : X) → P (Y x))
→ P (Σ Y))

(W-is-P : (X : 𝓤 ̇ ) (Y : X → 𝓤 ̇ )
→ P X
→ P (W X Y))
where

lemma₀ : (A : 𝓤 ̇ )
(A-is-P : P A)
(T : A → 𝓤 ̇ )
(S : (X : 𝓤 ̇ ) (p : P X) → A)
(ρ : {X : 𝓤 ̇ } (p : P X) → T (S X p) → X)
(σ : {X : 𝓤 ̇ } (p : P X) → X → T (S X p))
(η : {X : 𝓤 ̇ } (p : P X) (x : X) → ρ p (σ p x) ＝ x)
→ 𝟘
lemma₀ A A-is-P T S ρ σ η = γ
where
𝕎 :  𝓤 ̇
𝕎 = W A T

α : 𝕎 → (𝕎 → 𝓤 ̇ )
α (sup _ φ) = fiber φ

module _ (X : 𝓤 ̇ ) (X-is-P : P X) where

H : 𝕎 → 𝓤 ̇
H w = α w w → X

p : P (Σ H)
p = Σ-is-P 𝕎 H
(W-is-P A T A-is-P)
(λ w → P-exponential-ideal X (α w w) X-is-P)

R : 𝕎
R = sup (S (Σ H) p) (pr₁ ∘ ρ p)

B : 𝓤 ̇
B = α R R

r : B → (B → X)
r (t , e) = transport H e (pr₂ (ρ p t))

s : (B → X) → B
s f = σ p (R , f) , ap pr₁ (η p (R , f))

rs : (f : B → X) → r (s f) ＝ f
rs f = r (s f)                                            ＝⟨ refl ⟩
transport H (ap pr₁ (η p Rf)) (pr₂ (ρ p (σ p Rf))) ＝⟨ i ⟩
transport (H ∘ pr₁) (η p Rf)  (pr₂ (ρ p (σ p Rf))) ＝⟨ ii ⟩
pr₂ Rf                                             ＝⟨ refl ⟩
f                                                  ∎
where
Rf : Σ H
Rf = (R , f)

i = (transport-ap H pr₁ (η p (Rf)))⁻¹
ii = apd pr₂ (η p Rf)

δ : designated-fixed-point-property X
δ = retract-version.LFPT (r , s , rs)

γ : 𝟘
γ = pr₁ (δ 𝟘 𝟘-is-P id)

lemma₁ : (A : 𝓤 ̇ )
→ P A
→ (T : A → 𝓤 ̇ )
→ (S : (X : 𝓤 ̇ ) → P X → A)
→ ¬ ((X : 𝓤 ̇ ) (p : P X) → retract X of (T (S X p)))
lemma₁ A A-is-P T S ρ = 𝟘-elim
(lemma₀ A A-is-P T S
(λ {X} p → retraction (ρ X p))
(λ {X} p → section (ρ X p))
(λ {X} p → retract-condition (ρ X p)))

lemma₂ : (A : 𝓤 ̇ )
→ P A
→ (T : A → 𝓤 ̇ )
→ (S : (X : 𝓤 ̇ ) → P X → A)
→ ¬ ((X : 𝓤 ̇ ) (p : P X) → T (S X p) ≃ X)
lemma₂ A A-is-P T S e = lemma₁ A A-is-P T S (λ X p → ≃-gives-▷ (e X p))

lemma₃ : (A : 𝓤 ̇ )
→ P A
→ (T : A → 𝓤 ̇ )
→ (S : (X : 𝓤 ̇ ) → P X → A)
→ ¬ ((X : 𝓤 ̇ ) (p : P X) → T (S X p) ＝ X)
lemma₃ A A-is-P T S e = lemma₂ A A-is-P T S (λ X p → idtoeq (T (S X p)) X (e X p))

lemma₄ : ¬ (Σ (A , A-is-P) ꞉ Σ P , retract (Σ P) of A)
lemma₄ ((A , A-is-P) , r , s , rs) = lemma₃ A A-is-P T S TS
where
T : A → 𝓤 ̇
T a = pr₁ (r a)

T-is-P-valued : (a : A) → P (T a) -- Not used.
T-is-P-valued a = pr₂ (r a)       -- So the hypothesis is stronger
-- then necessary.
S : (X : 𝓤 ̇ ) → P X → A
S X p = s (X , p)

TS : (X : 𝓤 ̇ ) (p : P X) → T (S X p) ＝ X
TS X p = ap pr₁ (rs (X , p))

theorem : ¬ (Σ (A , A-is-P) ꞉ Σ P , Σ P ≃ A)
theorem (σ , e) = lemma₄ (σ , ≃-gives-◁ e)

\end{code}

Example:

We already know the following, because the type of sets is not a set
by univalence. But notice that the following assumes only function
extensionality:

\begin{code}

open import MLTT.W-Properties

silly-theorem : funext 𝓤 𝓤 → ¬ (Σ A ꞉ 𝓤 ̇ , is-set A × (hSet 𝓤 ≃ A))
silly-theorem {𝓤} fe (A , A-is-set , e) =
Coquand-further-generalized.theorem
𝓤
𝓤
is-set
𝟘-is-set
(λ X Y X-is-set → Π-is-set fe (λ _ → X-is-set))
(λ X Y → Σ-is-set)
(λ X X-is-set → W-is-set fe)
((A , A-is-set) , e)

\end{code}

The following application is even sillier, because any proposition A
has at most one element, but Ω has at least two elements, and so we
don't need this machinery to prove the following theorem:

\begin{code}

sillier-theorem : funext 𝓤 𝓤 → ¬ (Σ A ꞉ 𝓤 ̇ , is-prop A × (Ω 𝓤 ≃ A))
sillier-theorem {𝓤} fe (A , A-is-prop , e) =
Coquand-further-generalized.theorem
𝓤
𝓤
is-prop
𝟘-is-prop
(λ X Y X-is-prop → Π-is-prop fe (λ _ → X-is-prop))
(λ X Y → Σ-is-prop)
(λ X X-is-set → W-is-prop fe)
((A , A-is-prop) , e)

\end{code}

What we (Bezem, Coquand, Dybjer, Escardo) really want to prove is that

¬ (Σ A ꞉ 𝓤 ̇ , hSet 𝓤 ≃ A), (†)

without requiring that A is a set.

Marc Bezem wants this:

¬ (Σ A ꞉ 𝓤 ̇ , ∥ 𝓤 ∥₀ ≃ A).  (††)

Does it follow from this that

¬ (Σ A ꞉ 𝓤 ̇ , hSet 𝓤 ≃ A)?

What does follow from (††) is that the inclusion hSet 𝓤 → hSet (𝓤 ⁺) is
not an equivalence, which is what we want. So (††) implies (†).

Thierry Coquand asks: does the following help:

\begin{code}

Gylterud : 𝓤 ⁺ ̇
Gylterud {𝓤} = W (hSet 𝓤) pr₁

\end{code}

Intuitively, this is the groupoid of multisets. This occurs in Håkon
Gylterud's PhD thesis (Multisets in Type Theory, 2016).

Tonny Hurkens has a different way to get a contradiction from
type-in-type, that maybe can be adapted to get what we want.

Some of these questions are answered in the module BuraliForti
(December 2020).