Ian Ray. July 25 2026.

Recall, the type Sup-Lattice 𝓤 𝓦 𝓥 consists of a type L : 𝓤 with order in 𝓦 and
joins of size 𝓥, that is we have _≤_ : L → L → Ω 𝓦 and ⋁ : Fam L 𝓥 → L. We will
consider TarskiLFP 𝓤 𝓦 𝓥 to be the following statement:

 Any monotone map f : L → L, where L : Sup-Lattice 𝓤 𝓦 𝓥, has a least fixed
 point.

We can define TarskiGFP 𝓤 𝓦 𝓥 analogously, but TarskiGFP 𝓤 𝓦 𝓥 is actually false
(see the discussion in section 5 of "On Small Types in Univalent Foundations" by
Tom de Jong and Martin Escardo; https://doi.org/10.46298/lmcs-19(2:8)2023)
because Ord 𝓤 : 𝓤⁺ has 𝓤-suprema (in the presence of set quotients) but of
course the identity map has no greatest fixed point as Ord 𝓤 has no greatest
element (a dual argument can be made for TarskiLFP 𝓤 𝓦 𝓥 stated in terms of
inf-lattices by considering (Ord 𝓤)ᵒᵖ, but we restrict attention to sup-lattices
for now). The successor map on Ord 𝓤 is monotone iff LEM holds (see Theorem 8 of
"Connecting Constructive Notions of Ordinals in Homotopy Type Theory" by Nicolai
Kraus, Fredrik Nordvall Forsberg, Chuangjie Xu ;
https://doi.org/10.4230/LIPIcs.MFCS.2021.70). This result is formalized in the
TypeTopology library (see succ-not-necessarily-monotone and succ-monotone from
the file Ordinals.AdditionProperties). Thus, in the presence of LEM, Ord 𝓤 and
the successor map provide a counter-example to TarskiLFP 𝓤 𝓦 𝓥. It is open
whether there is a constructive and/or predicative counter-example to
TarskiLFP 𝓤 𝓦 𝓥.

Alternatively, TarskiLFP 𝓤 𝓤 𝓤 is true, and we recount the standard proof here: 

The point p ≔ ⋀ (Σ x ꞉ L , f(x) ≤ x) is the least fixed point of f : L → L.
It's essential that all sup-lattice data lives in 𝓤 for this infimum to exist.
It remains to show that p is a fixed point, as any other fixed point is also
pre-fixed, and then p is the least such by construction. Let x : L be any
other pre-fixed point, then of course p ≤ x and by monotonicity f(p) ≤ f(x) ≤ x.
So, f(p) is a lower bound of (Σ x ꞉ L , f(x) ≤ x), thus by construction p is
pre-fixed: f(p) ≤ p. For the other direction we first apply monotonicity to the
previous conclusion and conclude that f(p) is itself prefixed: f(f(p)) ≤ f(p).
By construction p ≤ f(p). Finally, by anti-symmetry f(p) ＝ p and we are done.

Unfortunately, in predicative order theory the existence of non-trivial terms
of Sup-Lattice 𝓤 𝓤 𝓤 is equivalent to propositional resizing (see Section 4 from
"On Small Types in Univalent Foundations" by Tom de Jong and Martin Escardo).
Thus, we can only utilize TarskiLFP 𝓤 𝓤 𝓤 in an interesting way by populating
Sup-Lattice 𝓤 𝓤 𝓤 with resizing principles.

Thus, one must modify the statement of TarskiLFP to retain a level of interest
in the area of predicative order theory. One immediate modification we may
consider is to restrict the lattice L to have a 𝓥-small basis. A basis is a type
B : 𝓥 and map β : B → L such that β(b) ≤ x is 𝓥-small for all b : B and x : L
and any x : L is generated by the basis, that is: x ＝ ⋁ ↓ᴮ x, where ↓ᴮ x is the
down-collection of x taken from B: Σ (b : B), β(b) ≤ x. Notice this type is small
by definition of a small-basis so the join exists.

In fact, it is this modification that will be the main focus of the current
file. That is, we call TarskiLFP-small-basis 𝓤 𝓦 𝓥 the following statement:

 Any monotone map f : L → L, where L : Sup-Lattice 𝓤 𝓦 𝓥 has a 𝓥-small basis,
 has a least fixed point.

Note: Ord 𝓤 does not have a 𝓤-small basis.

The predicative status of TarskiLFP-small-basis 𝓤 𝓦 𝓥 is currently open. That is
to say it is not known whether we can prove the above statement in a predicative
setting. But at this time the author and others interested in the field are
doubtful that such a proof exists. In fact, it is believed by the author that
TarskiLFP is in some way a 'predicative taboo' but exactly how strong of a
predicative taboo is also open and a topic of current investigation.

We can add further restrictions to the sup-lattice and monotone map to achieve
a predicative proof of a modified version of TarskiLFP-small-basis 𝓤 𝓦 𝓥 (see
OrderedTypes.PredicativeLFP for details on a type theoretic formalization
inspired by Giovanni Curi's paper "On Tarski's Fixed Point Theorem"). But for
now we put aside predicative concerns and will transition to the topic of this
file. Our goal is to show that TarskiLFP-small-basis 𝓤 𝓦 𝓥 is provable in the
presence of propositional resizing.

One crucial fact used in the traditional argument is that the set of pre-fixed
points is closed under the monotone endomap. Unfortunately, the type of
pre-fixed points is not small, so one is urged to consider the pre-fixed points
taken from the basis: 

                    Σ b ꞉ B , (f (β b) ≤ β b)

which is not small apriori but under appropriate assumptions can be made small.
The real issue is this type is not closed under the monotone endomap, because
the monotone endomap does not necessarily restrict to basis elements. At this
point the author was stuck and moved onto other approaches. For example, using
results from OrderedTypes.PredicativeLFP a proof of TarskiLFP-small-basis 𝓤 𝓦 𝓥
from propositional resizing (in addition to a QIT) can be achieved and is
relegated to the end of this file.

Following a discussion with Carlo Angiuli on the issues associated with a direct
proof of the least fixed point theorem from propositional resizing it was
suggested that we consider closing the basis under the monotone map.
For example something like B × ℕ {𝓥} with map B × ℕ {𝓥} → L given by

                        b ↦ fⁿ (β (b)).

But, this isn't necessarily a basis since fⁿ (β (b)) ≤ x isn't 𝓥-small and even
if it were it would not necessarily be closed under infima; another critical
fact used in the traditional proof. However, the failure of closing the basis
suggested an alternative approach to Carlo, which was subsequently sketched and
explained to the author. We will formalize and explain the proof here.

\begin{code}

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

open import UF.FunExt
open import UF.PropTrunc
open import UF.Subsingletons
open import UF.Size

module OrderedTypes.TarskiLFP-SmallBasis
        (pt : propositional-truncations-exist)
        (fe : Fun-Ext)
        (pe : Prop-Ext)
       where

private
 fe' : FunExt
 fe' 𝓤 𝓥 = fe {𝓤} {𝓥}

open import MLTT.Spartan
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.Logic
open import UF.Powerset-MultiUniverse
open import UF.Subsingletons-FunExt
open import UF.SubtypeClassifier
open import OrderedTypes.InfLattice fe pt
 hiding (⟨_⟩ ; is-monotone-endomap ; order-of ; antisymmetry-of ;
         transitivity-of)
open import OrderedTypes.SupLattice pt fe
open import OrderedTypes.SupLattice-SmallBasis pt fe

open AllCombinators pt fe
open PropositionalTruncation pt
open import Locales.Frame pt fe hiding (⟨_⟩ ; join-of)

open import Slice.Family
open import OrderedTypes.PredicativeLFP pt fe pe

\end{code}

We first consider the following subset S : B → Ω

                  S(b) ≔ (x : L) → (f x ≤ x) → (b ≤ᴮ x).

Using propositional resizing we can resize each S(b) to a proposition in 𝓥 thus
allowing us to take the supremum of its total space. We claim that

                     p ≔ ⋁ (𝕋(resized(S)) , β ∘ pr₁)
                            
is the least fixed point of f. Although the type of pre-fixed points is large
and its infimum does not necessarily exist we can show that p is the greatest
lower bound of all pre-fixed points. With this fact in hand the statement
TarskiLFP-small-basis 𝓤 𝓦 𝓥 follows immediately.

We start by defining the type of pre-fixed points (and observing that it is
large).

\begin{code}

module _ {L : Sup-Lattice 𝓤 𝓦 𝓥} {B : 𝓥 ̇}
         (β : B → ⟨ L ⟩) (h : is-basis L β)
         (f : ⟨ L ⟩ → ⟨ L ⟩)
         (f-mono : is-monotone-endomap L f)
       where

 Pre-Fixed-Points : 𝓤 ⊔ 𝓦 ̇
 Pre-Fixed-Points = Σ x ꞉ ⟨ L ⟩ , ((f x ≤⟨ L ⟩ x) holds)

\end{code}

Now we define a subset of the basis that is below all pre-fixed points.

\begin{code}

 module _ (pr : Propositional-resizing) where

  open is-basis h

  basis-below-pre-fixed : B → 𝓤 ⊔ 𝓦 ̇
  basis-below-pre-fixed b
   = (x : ⟨ L ⟩) → (f x ≤⟨ L ⟩ x) holds → (β b ≤⟨ L ⟩ x) holds

  basis-below-is-prop : (b : B) → is-prop (basis-below-pre-fixed b)
  basis-below-is-prop b
    = Π-is-prop fe (λ x → Π-is-prop fe (λ o → holds-is-prop (β b ≤⟨ L ⟩ x)))

  basis-below-subset : 𝓟 {𝓤 ⊔ 𝓦} B
  basis-below-subset b = (basis-below-pre-fixed b , basis-below-is-prop b)

\end{code}

This subset is also large but with propositional resizing it can be resized.

\begin{code}

  basis-below-is-small : (b : B) → basis-below-pre-fixed b is 𝓥 small
  basis-below-is-small b
   = pr (basis-below-pre-fixed b) (basis-below-is-prop b)

  resized-basis-below : B → 𝓥 ̇
  resized-basis-below b
   = resized (basis-below-pre-fixed b) (basis-below-is-small b)

  resized-basis-below≃basis-below
   : (b : B) → resized-basis-below b ≃ basis-below-pre-fixed b
  resized-basis-below≃basis-below b
   = resizing-condition (basis-below-is-small b)

  basis-below-to-resized-basis-below
   : (b : B) → basis-below-pre-fixed b → resized-basis-below b
  basis-below-to-resized-basis-below b
   = ⌜ (resized-basis-below≃basis-below b) ⌝⁻¹

  resized-basis-below-is-prop : (b : B) → is-prop (resized-basis-below b)
  resized-basis-below-is-prop b
   = equiv-to-prop (resized-basis-below≃basis-below b) (basis-below-is-prop b)

  resized-basis-below-subset : 𝓟 {𝓥} B
  resized-basis-below-subset b
   = (resized-basis-below b , resized-basis-below-is-prop b)

\end{code}

The join of the resized subset is the least fixed point.

\begin{code}

  lfp : ⟨ L ⟩
  lfp = ⋁⟨ L ⟩ 【 β , resized-basis-below-subset 】

  open Joins (order-of L)

  lfp-lub-basis-below
   : (lfp is-lub-of 【 β , basis-below-subset 】) holds
  lfp-lub-basis-below
   = sup-of-small-fam-is-lub L (β ∘ pr₁)
      (𝕋 resized-basis-below-subset , Σ-cong resized-basis-below≃basis-below)

  lfp-upper-bound-basis-below
   : (lfp is-an-upper-bound-of 【 β , basis-below-subset 】) holds
  lfp-upper-bound-basis-below = pr₁ lfp-lub-basis-below

  lfp-least-upper-bound-basis-below
   : ((u , _) : upper-bound (【 β , basis-below-subset 】))
   → (lfp ≤⟨ L ⟩ u) holds
  lfp-least-upper-bound-basis-below = pr₂ lfp-lub-basis-below

\end{code}

To see that this is the least fixed point we must observe that it is the greatest
lower bound of the type of pre-fixed points.

\begin{code}

  open Infs (order-of L)

  lfp-is-a-lower-bound
   : (lfp is-a-lower-bound-of (Pre-Fixed-Points , pr₁)) holds
  lfp-is-a-lower-bound (x , fx≤x)
   = lfp-least-upper-bound-basis-below
      (x , λ (b , basis-below-holds) → basis-below-holds x fx≤x)

  lfp-is-greatest-lower-bound : ((l , _) : lower-bound (Pre-Fixed-Points , pr₁))
                            → (l ≤⟨ L ⟩ lfp) holds
  lfp-is-greatest-lower-bound (l , lb)
   = transitivity-of L l (⋁⟨ L ⟩ (small-↓ᴮ l , small-↓ᴮ-inclusion l)) lfp
      (＝-to-≤ L (is-supᴮ' l))
       (joins-preserve-containment L β
        {λ - → (- ≤ᴮ l , ≤ᴮ-is-prop-valued)} {resized-basis-below-subset}
         (λ b o → basis-below-to-resized-basis-below b (λ x fx≤x
           → transitivity-of L (β b) l x (≤ᴮ-to-≤ o) (lb (x , fx≤x)))))

  lfp-glb-pre-fixed-points
   : (lfp is-glb-of (Pre-Fixed-Points , pr₁)) holds
  lfp-glb-pre-fixed-points = (lfp-is-a-lower-bound , lfp-is-greatest-lower-bound)

\end{code}

NOTE: Observe that we do not use Pre-Fixed-Points in an essential way. This
suggests that in general a subset S b = (x : L) → P x → β b ≤ x can be resized
and its join can be taken to get a least upper bound of the total space Σ P for
any family P : L → Type. This could prove useful in other investigations.

Now it follows rather directly that we have a least fixed point of f.

\begin{code}

 impredicative-Tarski-LFP-small-basis : Propositional-resizing
                                      → has-least-fixed-point L f
 impredicative-Tarski-LFP-small-basis pr
  = (p , antisymmetry-of L I II , III)
  where
   p = lfp pr
   I : (f p ≤⟨ L ⟩ p) holds
   I = lfp-is-greatest-lower-bound pr (f p , λ (x , fx≤x)
         → transitivity-of L (f p) (f x) x
            (f-mono p x (lfp-is-a-lower-bound pr (x , fx≤x))) fx≤x)
   II : (p ≤⟨ L ⟩ f p) holds
   II = lfp-is-a-lower-bound pr (f (p) , f-mono (f p) p I)
   III : (a : ⟨ L ⟩) → f a ＝ a → (p ≤⟨ L ⟩ a) holds
   III a fa＝a = lfp-is-a-lower-bound pr (a , ＝-to-≤ L fa＝a)

\end{code}

When the author was working on OrderedTypes.PredicativeLFP a proof of
TarskiLFP-small-basis 𝓤 𝓦 𝓥 from propositional resizing (and the existence of a
modest QIT) was already apparent, we will now record this observation here
with a brief explanation of how it is factored through the predicative
framework.

In PredicativeLFP we show that any monotone endomap produces a moderately
well-behaved inductive definition. We observe that (small) subsets which are
"closed" under the inductive definition correspond to pre-fixed points of the
monotone endomap. Assuming the existence of a seemingly innocuous QIT we can
then inductively generate a subset 𝓘nd of the basis closed under the inductive
definition. Now, by construction 𝓘nd is not necessarily small, but if it is, it
corresponds to the least fixed point. The remainder of PredicativeLFP explores
conditions on the sup-lattice and monotone endomap that guarantee this
smallness assumption. But with propositional resizing available we are able to
immediately satisfy this condition and as a result we get a proof of
TarskiLFP-small-basis 𝓤 𝓦 𝓥.

\begin{code}
    
module _ {L : Sup-Lattice 𝓤 𝓦 𝓥} {B : 𝓥 ̇}
         (β : B → ⟨ L ⟩) (h : is-basis L β)
         (f : ⟨ L ⟩ → ⟨ L ⟩)
         (f-mono : is-monotone-endomap L f)
       where

 open local-inductive-definitions L β h
 open correspondence-from-locally-small-ϕ L β h
       (ind-def-from-monotone-map f f-mono) (local-from-monotone-map f f-mono)

\end{code}

TODO. Certain QITs can be encoded using impredicativity. Is this the case for
the one assumed in the anonymous module below?

\begin{code}

 module _ (ind-e : inductively-generated-subset-exists L β h
                    (ind-def-from-monotone-map f f-mono))
        where

  open small-𝓘nd-from-exists ind-e
  open trunc-ind-def L β h (ind-def-from-monotone-map f f-mono) ind-e

  impredicative-Tarski-LFP-small-basis-from-PredicativeLFP
   : Propositional-resizing
   → has-least-fixed-point L f
  impredicative-Tarski-LFP-small-basis-from-PredicativeLFP pr
   = transport (has-least-fixed-point L)
      (dfunext fe (local-ind-def-is-section-of-Γ f f-mono))
       Γ-has-least-fixed-point
   where
    open smallness-assumption (λ - → pr (- ∈ 𝓘nd) (holds-is-prop (- ∈ₚ 𝓘nd)))

\end{code}