Martin Escardo, 24-25 June 2026.

This file answers a question posed in Various.LawvereFPT by myself on
12th October 2018, specifically in the module generalized-Coquand,
regarding whether a certain diagonalization construction could be
replaced by a second application of Lawvere's fixed point theorem.

The answer is that no, not directly. However, we can generalize
Lawvere's FPT as follows. In the above file, we defined

  lfix : {A : 𝓀 Μ‡ } {X : π“₯ Μ‡ }
       β†’ (A β†’ (A β†’ X))
       β†’ ((A β†’ X) β†’ A)
       β†’ (X β†’ X) β†’ X
  lfix r s f = r (s (Ξ» a β†’ f (r a a))) (s (Ξ» a β†’ f (r a a)))

and then proved various fixed point properties, including

  lfix-is-fixed-point : {A : 𝓀 Μ‡ } {X : π“₯ Μ‡ }
                        (r : A β†’ (A β†’ X))
                      β†’ (s : (A β†’ X) β†’ A)
                      β†’ s is-sectionΒ·-of r
                      β†’ (f : X β†’ X) β†’ lfix r s f ＝ f (lfix r s f)
and

  LFPT : {A : 𝓀 Μ‡ } {X : π“₯ Μ‡ } (Ο† : A β†’ (A β†’ X))
       β†’ is-surjection Ο†
       β†’ (f : X β†’ X) β†’ βˆƒ x κž‰ X , x ＝ f x

Here we generalize both, by replacing the identity type former _＝_ by
any binary relation _β‰ˆ_ whatsoever, and by replacing the notions of
section and of surjection accordingly.

We apply the former to get a simplified version of the module
generalized-Coquand, whose conclusions include

  Lemmaβ‚„    : Β¬ (Ξ£ U κž‰ 𝓀 Μ‡ , retract 𝓀 Μ‡ of U)
  corollary : βˆ€ 𝓀 β†’ Β¬ (retract 𝓀 ⁺ Μ‡ of (𝓀 Μ‡ ))
  Theorem   : Β¬ (Ξ£ U κž‰ 𝓀 Μ‡ , 𝓀 Μ‡ ≃ U)
  Corollary : Β¬ (𝓀 ⁺ Μ‡ ≃ 𝓀 Μ‡ )

At the moment we don't have any application of the second
generalization.

We work in a Martin-LΓΆf type theory with no HoTT/UF axioms other than
propositional truncation, which isn't needed for the main theorem, but
only for the second version of the fixed point theorem.

James E Hanson came up with essentially the second generalization on 11
May 2026, before us, called (⋆⋆) in his post https://mathoverflow.net/a/511183

  (⋆⋆) For any f:AΓ—Aβ†’B, g:Bβ†’B, and binary relation RβŠ†BΒ², if there is an
       a such that g(f(x,x)) R f(a,x) for all x∈A, then g(f(a,a)) R f(a,a).

Communicated by him to me on 26th June after I publicly distributed this file:
https://mathstodon.xyz/deck/@jameshanson/116816664171797522

\begin{code}

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

module Various.LawvereFPT-Generalized where

open import MLTT.Spartan
open import Various.LawvereFPT

\end{code}

We now develop the first generalization, where the assumptions are
given in two nested anonymous submodules.

\begin{code}

module _ {𝓀 π“₯ 𝓦 : Universe}
         (A      : 𝓀 Μ‡ )
         (X      : π“₯ Μ‡ )
         (_β‰ˆ_    : X β†’ X β†’ 𝓦 Μ‡ )
       where

  private
   𝓕 : 𝓀 βŠ” π“₯ Μ‡
   𝓕 = (A β†’ X) β†’ (A β†’ X)

\end{code}

We define (double) pointwise relationship as follows.

\begin{code}

   _β‰ˆΜ‡_ : 𝓕 β†’ 𝓕 β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 Μ‡
   Ο• β‰ˆΜ‡ ψ = (g : A β†’ X) (a : A) β†’ Ο• g a β‰ˆ ψ g a

  module _ (r  : A β†’ (A β†’ X))
           (s  : (A β†’ X) β†’ A)
           (rs : (r ∘ s) β‰ˆΜ‡ id)
         where

\end{code}

Notice that the proof of the following is the same as the original
proof of the particular case lfix-is-fixed-point, with _＝_ replaced
by _β‰ˆ_.

\begin{code}

   lfix-is-relational-fixed-point : (f : X β†’ X)
                                  β†’ lfix r s f β‰ˆ f (lfix r s f)
   lfix-is-relational-fixed-point f = e
    where
     g : A β†’ X
     g a = f (r a a)

     e : lfix r s f β‰ˆ f (lfix r s f)
     e = rs g (s g)

   relational-LFPT : (f : X β†’ X) β†’ Ξ£ x κž‰ X , x β‰ˆ f x
   relational-LFPT f = lfix r s f , lfix-is-relational-fixed-point f

\end{code}

The above generalizes the original theorem in the strong sense that
its proof is definitionally equal when _β‰ˆ_ is taken to be the identity
type:

\begin{code}

private

 open retract-version

 sanity-check : {A  : 𝓀 Μ‡ } {X  : π“₯ Μ‡ }
              β†’ lfix-is-fixed-point ＝ lfix-is-relational-fixed-point A X _＝_
 sanity-check = by-construction

\end{code}

For the module generalized-Coquand-streamlined below, we use the
following particular case, where B β‰ˆ C is taken to be "C is a retract
of B".

\begin{code}

open import UF.Retracts

LFPT-with-retract-relation
 : {A : 𝓀 Μ‡ }
   (r : A β†’ (A β†’ π“₯ Μ‡ ))
   (s : (A β†’ π“₯ Μ‡ ) β†’ A)
 β†’ ((g : A β†’ π“₯ Μ‡ ) (a : A) β†’ retract g a of (r ∘ s) g a)
 β†’ (f : π“₯ Μ‡ β†’ π“₯ Μ‡ ) β†’ Ξ£ B κž‰ π“₯ Μ‡ , retract f B of B
LFPT-with-retract-relation {𝓀} {π“₯} {A}
 = relational-LFPT A (π“₯ Μ‡ )
    (Ξ» (B C : π“₯ Μ‡ ) β†’ retract C of B)

\end{code}

We now develop the second generalization. In order the have the
existential quantifier available, we need to assume the existence of
propositional truncations.

\begin{code}

open import UF.PropTrunc

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

 open PropositionalTruncation pt

 module _ {𝓀 π“₯ 𝓦 : Universe}
          (A      : 𝓀 Μ‡ )
          (X      : π“₯ Μ‡ )
          (_β‰ˆ_    : X β†’ X β†’ 𝓦 Μ‡ )
        where

\end{code}

We define (single) pointwise equality as follows.

\begin{code}

  private
   _β‰ˆΜ‡_ : (A β†’ X) β†’ (A β†’ X) β†’ 𝓀 βŠ” 𝓦 Μ‡
   Ο• β‰ˆΜ‡ ψ = (a : A) β†’ Ο• a β‰ˆ ψ a

  module _ (Ο† : A β†’ (A β†’ X))
           (s : (g : A β†’ X) β†’ βˆƒ a κž‰ A , Ο† a β‰ˆΜ‡ g)
         where

   relational-surjection-LFPT : (f : X β†’ X) β†’ βˆƒ x κž‰ X , x β‰ˆ f x
   relational-surjection-LFPT f = II
    where
     g : A β†’ X
     g a = f (Ο† a a)

     I : (Ξ£ a κž‰ A , Ο† a β‰ˆΜ‡ g) β†’ Ξ£ x κž‰ X , x β‰ˆ f x
     I (a , q) = Ο† a a , q a

     II : βˆƒ x κž‰ X , x β‰ˆ f x
     II = βˆ₯βˆ₯-functor I (s g)

\end{code}

Again, the proof is literally the same as the original one with the
identity type _＝_ in place of the arbitrary relation _β‰ˆ_.

As discussed above, we don't yet have any application of the second
generalization.

We conclude with an application of the first, which was its original
motivation. The argument assumes W types in our type theory.

\begin{code}

module generalized-Coquand-streamlined where

 open import W.Type
 open import UF.Base
 open import UF.Equiv

\end{code}

We begin by showing that certain assumptions are together impossible,
by using two applications of the fixed point theorem, where the first
one is the generalization and the second one is the original (to show
that no type is logically equivalent to its own negation).

\begin{code}

 Lemmaβ‚€ : (U  : 𝓀 Μ‡ )
          (R  : U β†’ 𝓀 Μ‡ )
          (S  : 𝓀 Μ‡ β†’ U)
          (ρ  : (X : 𝓀 Μ‡ ) β†’ R (S X) β†’ X)
          (Οƒ  : (X : 𝓀 Μ‡ ) β†’ X β†’ R (S X))
          (ρσ : (X : 𝓀 Μ‡ ) β†’ ρ X ∘ Οƒ X ∼ id)
        β†’ 𝟘
 Lemmaβ‚€ {𝓀} U R S ρ Οƒ ρσ = III
  where
   A : 𝓀 Μ‡
   A = W U R

\end{code}

Thus, an element of the type A is of the form

  ssup u Ο†

with u : U and Ο† : R u β†’ A.

\begin{code}

   r : A β†’ (A β†’ 𝓀 Μ‡ )
   r (ssup u Ο†) = fiber Ο†

\end{code}

Notice that, by definition, fiber Ο† a = Ξ£ x κž‰ R u , Ο† x ＝ a.

For g : A β†’ 𝓀, we have that the type Ξ£ a κž‰ A , g a (abbreviated Ξ£ g)
lives in 𝓀, and hence we can apply S to get a point of the type U. We
have that ρ (Ξ£ g) : R (S (Ξ£ g)) β†’ Ξ£ g, and so post-composition with
the first projection gives a function R (S (Ξ£ g)) β†’ A

\begin{code}

   s : (A β†’ 𝓀 Μ‡ ) β†’ A
   s g = ssup (S (Ξ£ g)) (pr₁ ∘ ρ (Ξ£ g))

   rs : (g : A β†’ 𝓀 Μ‡ ) (a : A) β†’ retract g a of r (s g) a
   rs g a = 𝓻 , 𝓼 , 𝓻𝓼
    where
     𝓻 : r (s g) a β†’ g a
     𝓻 (u , e) = transport g e (prβ‚‚ (ρ (Ξ£ g) u))

     𝓼 : g a β†’ r (s g) a
     𝓼 y = Οƒ (Ξ£ g) (a , y) , ap pr₁ (ρσ (Ξ£ g) (a , y))

     𝓻𝓼 : (y : g a) β†’ 𝓻 (𝓼 y) ＝ y
     𝓻𝓼 y =
      𝓻 (𝓼 y)                                                         ＝⟨refl⟩
      transport g (ap pr₁ (ρσ (Ξ£ g) ay)) (prβ‚‚ (ρ (Ξ£ g) (Οƒ (Ξ£ g) ay))) ＝⟨ i ⟩
      transport (g ∘ pr₁) (ρσ (Ξ£ g) ay) (prβ‚‚ (ρ (Ξ£ g) (Οƒ (Ξ£ g) ay)))  ＝⟨ ii ⟩
      prβ‚‚ ay                                                          ＝⟨refl⟩
      y                                                               ∎
       where
        ay : Ξ£ g
        ay = (a , y)

        i  = (transport-ap g pr₁ (ρσ (Ξ£ g) ay))⁻¹
        ii = apd prβ‚‚ (ρσ (Ξ£ g) ay)

   I : Ξ£ B κž‰ 𝓀 Μ‡ , retract Β¬ B of B
   I = LFPT-with-retract-relation r s rs Β¬_

   II : Β¬ (Ξ£ B κž‰ 𝓀 Μ‡ , retract Β¬ B of B)
   II (B , (f , g , _)) = not-equivalent-to-own-negation'' (f , g)

   III : 𝟘
   III = II I

 Lemma₁ : (U : 𝓀 Μ‡ ) (R : U β†’ 𝓀 Μ‡ ) (S : 𝓀 Μ‡ β†’ U)
        β†’ Β¬ ((X : 𝓀 Μ‡ ) β†’ retract X of R (S X))
 Lemma₁ U R S ρ = Lemmaβ‚€ U R S
                   (Ξ» X β†’ retraction (ρ X))
                   (Ξ» X β†’ section (ρ X))
                   (Ξ» X β†’ retract-condition (ρ X))

 Lemmaβ‚‚ : (U : 𝓀 Μ‡ ) (R : U β†’ 𝓀 Μ‡ ) (S : 𝓀 Μ‡ β†’ U)
        β†’ Β¬ ((X : 𝓀 Μ‡ ) β†’ R (S X) ≃ X)
 Lemmaβ‚‚ U R S e = Lemma₁ U R S (Ξ» X β†’ ≃-gives-β–· (e X))

 Lemma₃ : (U : 𝓀 Μ‡ ) (R : U β†’ 𝓀 Μ‡ ) (S : 𝓀 Μ‡ β†’ U)
        β†’ Β¬ ((X : 𝓀 Μ‡ ) β†’ R (S X) ＝ X)
 Lemma₃ U R S p = Lemmaβ‚‚ U R S (Ξ» X β†’ idtoeq (R (S X)) X (p X))

 Lemmaβ‚„ : Β¬ (Ξ£ U κž‰ 𝓀 Μ‡ , retract 𝓀 Μ‡ of U)
 Lemmaβ‚„ (U , R , S , RS) = Lemma₃ U R S RS

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

 Theorem : Β¬ (Ξ£ U κž‰ 𝓀 Μ‡ , 𝓀 Μ‡ ≃ U)
 Theorem (U , e) = Lemmaβ‚„ (U , ≃-gives-◁ e)

 Corollary : Β¬ (𝓀 ⁺ Μ‡ ≃ 𝓀 Μ‡ )
 Corollary {𝓀} e = Theorem ((𝓀 Μ‡ ) , e)

\end{code}

A variation of this argument was used originally by Coquand to show
that type theory with a judgment Type:Type is inconsistent [1]. This
corresponds to the above theorem, which says that no type in a type a
universe is equivalent to the universe. We originally developed this
modification on 12 October 2018 in the file Various.LawvereFPT.

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