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 #-}

module LawvereFPT where

open import SpartanMLTT

\end{code}

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

\begin{code}


open import Two-Properties
open import NaturalNumbers-Properties
open import UF-Retracts
open import UF-Equiv
open import UF-Miscelanea
open import UF-FunExt

module retract-version where

\end{code}

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 : {A : 𝓀 Μ‡ } {X : π“₯ Μ‡ } (r : A β†’ (A β†’ X))
                        β†’ funext 𝓀 π“₯
                        β†’ has-sectionΒ· r β†’ has-section r
 sectionΒ·-gives-section r fe (s , rsΒ·) = s , Ξ» g β†’ dfunext fe (rsΒ· g)

 LFPTΒ· : {A : 𝓀 Μ‡ } {X : π“₯ Μ‡ } (r : A β†’ (A β†’ X))
       β†’ has-sectionΒ· r
       β†’ (f : X β†’ X) β†’ Ξ£ \(x : X) β†’ x ≑ f 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
      β†’ (f : X β†’ X) β†’ Ξ£ \(x : X) β†’ x ≑ f x
 LFPT (r , h) = LFPTΒ· r (section-gives-sectionΒ· r h)

 LFPT-≃ : {A : 𝓀 βŠ” π“₯ Μ‡ } {X : 𝓀 Μ‡ }
        β†’ A ≃ (A β†’ X)
        β†’ (f : X β†’ X) β†’ Ξ£ \(x : X) β†’ x ≑ f x
 LFPT-≃ p = LFPT (equiv-retract-r p)

 LFPT-≑ : {A : 𝓀 βŠ” π“₯ Μ‡ } {X : 𝓀 Μ‡ }
        β†’ A ≑ (A β†’ X)
        β†’ (f : X β†’ X) β†’ Ξ£ \(x : X) β†’ x ≑ f 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
   Ξ³ : (f : 𝟘 β†’ 𝟘) β†’ Ξ£ \(x : 𝟘) β†’ x ≑ f x
   Ξ³ = 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 :
     (𝓀 π“₯ : Universe) (A : π“₯ Μ‡ ) (r : A β†’ (A β†’ 𝓀 Μ‡ ))
   β†’ has-sectionΒ· r
   β†’ (X : 𝓀 Μ‡ ) (f : X β†’ X) β†’ Ξ£ \(x : X) β†’ x ≑ f 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 :
     (𝓀 π“₯ : Universe) (A : π“₯ Μ‡ )
   β†’ (r : A β†’ (A β†’ 𝓀 Μ‡ )) β†’ Β¬(has-sectionΒ· r)
 Cantor-theorem-for-universes 𝓀 π“₯ A r h = 𝟘-elim(pr₁ (cantor-theorem-for-universes 𝓀 π“₯ A r h 𝟘 id))

 \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 : (𝓀 π“₯ : Universe) (A : π“₯ Μ‡ )
                β†’ funext 𝓀 𝓀₀ β†’ (r : A β†’ (A β†’ Ξ© 𝓀)) β†’ Β¬(has-sectionΒ· r)
 cantor-theorem 𝓀 π“₯ A fe 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
open import UF-ImageAndSurjection

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

 open PropositionalTruncation pt
 open ImageAndSurjection pt

 LFPT : {A : 𝓀 Μ‡ } {X : π“₯ Μ‡ } (Ο† : A β†’ (A β†’ X))
      β†’ is-surjection Ο†
      β†’ (f : X β†’ X) β†’ βˆƒ \(x : X) β†’ x ≑ f 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 :
     (𝓀 π“₯ : Universe) (A : π“₯ Μ‡ ) (Ο† : A β†’ (A β†’ 𝓀 Μ‡ ))
   β†’ is-surjection Ο†
   β†’ (X : 𝓀 Μ‡ ) (f : X β†’ X) β†’ βˆƒ \(x : X) β†’ x ≑ f 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 :
     (𝓀 π“₯ : Universe) (A : π“₯ Μ‡ )
   β†’ (Ο† : A β†’ (A β†’ 𝓀 Μ‡ )) β†’ Β¬(is-surjection Ο†)
 Cantor-theorem-for-universes 𝓀 π“₯ A r h = 𝟘-elim(βˆ₯βˆ₯-rec 𝟘-is-prop pr₁ c)
  where
   c : βˆƒ \(x : 𝟘) β†’ x ≑ x
   c = cantor-theorem-for-universes 𝓀 π“₯ A r h 𝟘 id

 cantor-theorem :
     (𝓀 π“₯ : Universe) (A : π“₯ Μ‡ )
   β†’ funext 𝓀 𝓀₀ β†’ (Ο† : A β†’ (A β†’ Ξ© 𝓀)) β†’ Β¬(is-surjection Ο†)
 cantor-theorem 𝓀 π“₯ A fe Ο† s = βˆ₯βˆ₯-rec 𝟘-is-prop (retract-version.not-no-fp fe) t
  where
   t : βˆƒ \(B : Ξ© 𝓀) β†’ B ≑ not fe B
   t = LFPT Ο† s (not fe)

 \end{code}

 Another corollary is that the Cantor type (β„• β†’ 𝟚) and the Baire type
 (β„• β†’ β„•) are uncountable:

 \begin{code}

 open import Two

 cantor-uncountable : Β¬ Ξ£ \(Ο† : β„• β†’ (β„• β†’ 𝟚)) β†’ is-surjection Ο†
 cantor-uncountable (Ο† , s) = βˆ₯βˆ₯-rec 𝟘-is-prop (uncurry complement-no-fp) t
  where
   t : βˆƒ \(n : 𝟚) β†’ n ≑ complement n
   t = LFPT Ο† s complement

 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 LFTP, 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 ImageAndSurjection pt
 open import 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β‚€
           β†’ (f : B β†’ B) β†’ Ξ£ \(b : B) β†’ b ≑ f b
 udr-lemma X B aβ‚€ i b ρ = retract-version.LFPT ρ'
  where
   ρ' : retract (X aβ‚€ β†’ B) of X aβ‚€
   ρ' = retracts-compose ρ ((Ξ» f β†’ f aβ‚€) , Ξ -projection-has-section aβ‚€ i (Ξ» a x β†’ b))

 universe-discretely-regular' :
    (𝓀 π“₯ : Universe) (A : 𝓀 Μ‡ ) (X : A β†’ 𝓀 βŠ” π“₯ Μ‡ )
  β†’ is-discrete A β†’ Ξ£ \(B : 𝓀 βŠ” π“₯ Μ‡ ) β†’ (a : A) β†’ Β¬(X a ≃ B)
 universe-discretely-regular' 𝓀 π“₯ A X d  = B , Ο†
   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)
      ρ = equiv-retract-r p
      Ξ³ : (f : 𝟚 β†’ 𝟚) β†’ Ξ£ \(b : 𝟚) β†’ b ≑ f b
      Ξ³ = udr-lemma X 𝟚 a (d a) β‚€ ρ

 universe-discretely-regular :
    {𝓀 π“₯ : Universe} {A : 𝓀 Μ‡ } (X : A β†’ 𝓀 βŠ” π“₯ Μ‡ )
  β†’ is-discrete A β†’ Ξ£ \(B : 𝓀 βŠ” π“₯ Μ‡ ) β†’ (a : A) β†’ Β¬(X a ≑ B)
 universe-discretely-regular {𝓀} {π“₯} {A} X d =
   Ξ³ (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))

 Universe-discretely-regular : {𝓀 π“₯ : Universe} {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 β†’ X a ≑ B
   e = s B
   n : Β¬(Ξ£ \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 ImageAndSurjection pt
 open import DiscreteAndSeparated

 Ξ -projection-has-section :
    {A : 𝓀 Μ‡ } {X : A β†’ π“₯ Μ‡ }
  β†’ funext π“₯ ((𝓀 βŠ” 𝓦)⁺) β†’ funext (𝓀 βŠ” 𝓦) (𝓀 βŠ” 𝓦) β†’ propext (𝓀 βŠ” 𝓦)
  β†’ (aβ‚€ : A) β†’ is-h-isolated aβ‚€ β†’ has-section (Ξ» (f : (a : A) β†’ X a β†’ Ξ© (𝓀 βŠ” 𝓦)) β†’ f aβ‚€)
 Ξ -projection-has-section {𝓀} {π“₯} {𝓦} {A} {X} fe fe' pe aβ‚€ ish = s , rs
  where
   s : (X aβ‚€ β†’ Ξ© (𝓀 βŠ” 𝓦)) β†’ ((a : A) β†’ X a β†’ Ξ© (𝓀 βŠ” 𝓦))
   s Ο† a x = (βˆƒ \(p : a ≑ aβ‚€) β†’ Ο† (transport X p x) holds) , βˆ₯βˆ₯-is-a-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-a-prop ≑ Ο† xβ‚€
     Ξ³ xβ‚€ = to-Ξ£-≑ (pe βˆ₯βˆ₯-is-a-prop (holds-is-prop (Ο† xβ‚€)) (a xβ‚€) (b xβ‚€) ,
                     being-a-prop-is-a-prop fe' (holds-is-prop _) (holds-is-prop (Ο† xβ‚€)))

 usr-lemma : {A : 𝓀 Μ‡ } (X : A β†’ π“₯ Μ‡ )
           β†’ funext π“₯ ((𝓀 βŠ” 𝓦)⁺) β†’ funext (𝓀 βŠ” 𝓦) (𝓀 βŠ” 𝓦) β†’ propext (𝓀 βŠ” 𝓦)
           β†’ (aβ‚€ : A)
           β†’ is-h-isolated aβ‚€
           β†’ retract ((a : A) β†’ X a β†’ Ξ© (𝓀 βŠ” 𝓦)) of X aβ‚€
           β†’ (f : Ξ© (𝓀 βŠ” 𝓦) β†’ Ξ© (𝓀 βŠ” 𝓦)) β†’ Ξ£ \(p : Ξ© (𝓀 βŠ” 𝓦)) β†’ p ≑ f p
 usr-lemma {𝓀} {π“₯} {𝓦} {A} X fe fe' pe 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   : 𝓀 Μ‡ )
   (X   : A β†’ 𝓀 ⁺ βŠ” π“₯ Μ‡ )
   (iss : is-set A)
   where

\end{code}

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)
       ρ = equiv-retract-r p
       Ξ³ : (f : Ξ© 𝓀 β†’ Ξ© 𝓀) β†’ Ξ£ \(p : Ξ© 𝓀) β†’ p ≑ f p
       Ξ³ = usr-lemma {𝓀} {π“₯ βŠ” 𝓀 ⁺} {𝓀} {A} X fe' fe pe a iss ρ

  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 = βˆ₯βˆ₯-rec 𝟘-is-prop (uncurry Ο†) e
   where
    B : 𝓀 ⁺ βŠ” π“₯ Μ‡
    B = pr₁ universe-set-regular
    Ο† : βˆ€ a β†’ Β¬(X a ≑ B)
    Ο† = prβ‚‚ universe-set-regular
    e : βˆƒ \a β†’ X a ≑ B
    e = s B

\end{code}

See also http://www.cs.bham.ac.uk/~mhe/agda-new/Type-in-Type-False.html

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.

NB. It should also be possible to replace the diagonal construction of
Lemmaβ‚€ by a second application of LFPT (todo).

\begin{code}

module Coquand where

 Lemmaβ‚€ : (𝓀 : Universe)
          (A : 𝓀 Μ‡ )
          (T : A β†’ 𝓀 Μ‡ )
          (S : 𝓀 Μ‡ β†’ A)
          (ρ : {X : 𝓀 Μ‡ } β†’ T (S X) β†’ X)
          (Οƒ : {X : 𝓀 Μ‡ } β†’ X β†’ T (S X))
          (Ξ· : {X : 𝓀 Μ‡ } (x : X) β†’ ρ (Οƒ x) ≑ x)
        β†’ 𝟘
 Lemmaβ‚€ 𝓀 A T S ρ Οƒ Ξ· = pr₁ (Ξ³ 𝟘 id )
  where
   data π•Ž : 𝓀 Μ‡  where
    sup : {a : A} β†’ (T a β†’ π•Ž) β†’ π•Ž

   Ξ± : π•Ž β†’ (π•Ž β†’ 𝓀 Μ‡ )
   Ξ± (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₁ (Ξ· (R , f))) (prβ‚‚ (ρ (Οƒ {Ξ£ H} (R , f))))
                   β‰‘βŸ¨ (transport-ap H pr₁ (Ξ· (R , f)))⁻¹ ⟩
           transport (H ∘ pr₁) (Ξ· (R , f)) (prβ‚‚ (ρ (Οƒ {Ξ£ H} (R , f))))
                   β‰‘βŸ¨ apd prβ‚‚ (Ξ· (R , f)) ⟩
           prβ‚‚ ((R , f) ∢ Ξ£ H)
                   β‰‘βŸ¨ refl ⟩
           f       ∎
    Ξ³ : (f : X β†’ X) β†’ Ξ£ \(x : X) β†’ x ≑ f x
    Ξ³ = retract-version.LFPT (r , s , rs)

\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 β†’ equiv-retract-r (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

 corollary : βˆ€ 𝓀 β†’ Β¬ (retract 𝓀 ⁺ Μ‡ of (𝓀 Μ‡ ))
 corollary 𝓀 ρ = Lemmaβ‚„ (𝓀 ⁺) ((𝓀 Μ‡ ) , ρ)

\end{code}

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

\begin{code}

 Theorem : βˆ€ 𝓀 β†’ Β¬ Ξ£ \(π•Œ : 𝓀 Μ‡ ) β†’ 𝓀 Μ‡ ≃ π•Œ
 Theorem 𝓀 (π•Œ , e) = Lemmaβ‚„ 𝓀 (π•Œ , equiv-retract-l e)

\end{code}