Martin Escardo, 24-25 June 2026.

This file answers a question posed in Various.LawvereFPT, 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 for it, 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 W types, and 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.

\begin{code}

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

module Various.LawvereFPT-Generalized where

open import MLTT.Spartan
open import UF.Base hiding (_β‰ˆ_)
open import UF.Equiv
open import UF.Retracts
open import Various.LawvereFPT
open import W.Type

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

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 motivation
in the first place.  We first show 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}

module generalized-Coquand-streamlined where

 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