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

open import Two-Properties
open import NaturalNumbers-Properties

open import UF-Base
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

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
open import UF-ImageAndSurjection

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

 open PropositionalTruncation pt
 open 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 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 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β‚€
           β†’ 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 ImageAndSurjection pt
 open import 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 (retraction-surjection X h)

\end{code}

See also http://www.cs.bham.ac.uk/~mhe/TypeTopology/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 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 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 23 December 2020, modified 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 i = Ξ³
  where
   A : {𝓀 : Universe} β†’ 𝓀 Μ‡ β†’ 𝓀 ⁺ Μ‡
   A {𝓀} _ = 𝓀 Μ‡

   e : 𝟘 {𝓀₁} ≃ 𝟘 {𝓀₀}
   e = qinveq 𝟘-elim (𝟘-elim , (Ξ» x β†’ 𝟘-elim x) , (Ξ» x β†’ 𝟘-elim x))

   Ξ΄ : (𝓀₁ Μ‡ ) ≃ (𝓀₀ Μ‡ )
   Ξ΄ = i 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 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 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.