Martin Escardo, 24th November 2025.
It is well known that in a boolean elementary (1-)topos, every algebra
of the lifting (aka partial-map classifier) monad is free, and the
proof is easy [1][2].
We show that the converse holds, so that every algebra is free if and
only if the topos is boolean (that is, the principle of excluded middle holds).
The object Ω of truth values is an algebra in (at least) two ways,
with structure map ⨆ = ∃ and ⨆ = ∀.
In all toposes, the structure map ⨆ = ∃ exhibits Ω as freely generated
by ⊤ : Ω.
In a boolean topos, the structure map ⨆ = ∀ exhibits Ω as freely
generated by ⊥ : Ω.
Moreover, the converse is true. If the structure map ⨆ = ∀ exhibits Ω
as freely generated by ⊥ : Ω, then the topos is boolean.
We may wonder whether, in an arbitrary topos, the object Ω with the
structure map ⨆ = ∀ is freely generated by *any* object G of generators.
We show that if this is the case, then
1. the insertion of generators ι : G → Ω is constant with value ⊥,
2. the principle of excluded middle holds, and
3. G ≃ 𝟙.
Jon Sterling [1] previously conjectured that the same would be the
case for the lifting monad in the category of dcpos [3], namely that
there are some toposes in which there is an algebra of the lifting
monad in the category of dcpos that is not free.
We haven't (yet) formalized this here, but we offer an argument to
prove Sterling's conjecture, based on the above claims (which are
formalized below).
Anders Kock [2] proved that any algebra in the category of sets is
bounded-complete (every upper bounded set has a least upper bound).
Because the lifting algebra Ω with structure map ∀ has a largest
element, namely ⊥, it is a sup-lattice, and, in particular, directed
complete.
Regarding continuity, the structure map is always supremum (after
Kock), and suprema formation always preserve suprema, including
directed ones.
Hence the answer for the category of sets also gives an answer for the
category of dcpos in any elementary topos.
So the above discussion settles Sterling's conjecture positively, by
providing an example of a dcpo lifting algebra which is not always
free.
TODO. It would be good to formalize this here in TypeTopology.
[1] Jon Sterling. Tensorial structure of the lifting doctrine in
constructive domain theory. Originally 28 Dec 2023, last revised 30
Jan 2025. https://doi.org/10.48550/arXiv.2312.17023
[2] Anders Kock. Algebras for the partial-map classifier monad. In:
Carboni, A., Pedicchio, M.C., Rosolini, G. (eds) Category
Theory. LNM, vol 1488.
https://doi.org/10.1007/BFb0084225
https://tildeweb.au.dk/au76680/jonna5.pdf
[3] Anders Kock. The constructive lift monad.
BRICS Report Series (Aarhus), ISSN 0909-0878 (1995)
http://tildeweb.au.dk/au76680/CLM.pdf
\begin{code}
{-# OPTIONS --safe --without-K #-}
\end{code}
We import the following unused module, deliberately without opening
it, for browsing purposes, where the original ideas presented here
were obtained in a tortuous way, with more information than necessary
to obtain the results, which may nevertheless be interesting for other
purposes.
\begin{code}
import Lifting.AnAlgebraWhichIsNotAlwaysFree-blackboard
\end{code}
We now import what is necessary to give the types for the module
parameters.
\begin{code}
open import MLTT.Spartan
open import UF.FunExt
open import UF.Sets
open import UF.Subsingletons
open import UF.SubtypeClassifier renaming (Ω to Ω-of-universe ;
⊥ to ⊥Ω ;
⊤ to ⊤Ω)
\end{code}
We work with an arbitrary type universe 𝓣, and assume function
extensionality and propositional extensionality, which are available
in any 1-topos.
We also work with a hypothetical set G of generators, and an inclusion
of generators ι, which will, by assumption, exhibit Ω with the
structure map ⨆ = ∀ as a free algebra, but we postpone this assumption
as much as possible.
\begin{code}
module Lifting.AnAlgebraWhichIsNotAlwaysFree
(fe : Fun-Ext)
(pe : Prop-Ext)
(𝓣 : Universe)
where
open import Lifting.Algebras 𝓣
open import Lifting.Construction 𝓣
open import Lifting.EmbeddingDirectly 𝓣
open import Lifting.Identity 𝓣
open import Lifting.TwoAlgebrasOnOmega 𝓣 fe pe
renaming (Π-alg-on-Ω to Ω∀ ; Σ-alg-on-Ω to Ω∃)
open import UF.ClassicalLogic
open import UF.Embeddings
open import UF.Equiv
open import UF.Logic
open import UF.SubtypeClassifier-Properties
open Implication fe renaming (¬ₚ_ to ⇁_)
open Universal fe
\end{code}
Some abbreviations now.
\begin{code}
private
𝓣⁺ = 𝓣 ⁺
Ω : 𝓣⁺ ̇
Ω = Ω-of-universe 𝓣
fe' : FunExt
fe' 𝓤 𝓥 = fe {𝓤} {𝓥}
\end{code}
To achieve our objectives stated above, we will soon assume that
Ω equipped with the structure map ∀ is indeed freely generated by G
with insertion of generators ι, which implies that h is an
equivalence. But we can prove a few things before we assume that.
We have the algebra 𝓛 G freely generated by G, with insertion of
generators η : G → 𝓛 G, and in particular a unique algebra
homomorphism h : 𝓛 G → Ω, for Ω equipped with the ∀ lifting structure,
extending ι along η.
η
G ───────→ 𝓛 G
╲ │
╲ │
╲ │
ι ╲ h │
╲ │
╲ │
╲ │
╲ ↓
➘ Ω.
\begin{code}
module Ω∀-free-gives-EM
(G : 𝓣 ̇ )
(G-is-set : is-set G)
(ι : G → Ω-of-universe 𝓣)
where
open free-algebras-in-the-category-of-sets pe fe G G-is-set
𝓛G : 𝓛-alg (𝓛 G)
𝓛G = canonical-free-algebra
h : 𝓛 G → Ω
h = 𝓛-extension (Ω-is-set fe pe) Ω∀ ι
h-explicitly : (l@(P , φ , i) : 𝓛 G) → h l ＝ (Ɐ a ꞉ P , ι (φ a))
h-explicitly _ = by-definition
h-is-hom : is-hom 𝓛G Ω∀ h
h-is-hom = 𝓛-extension-is-hom (Ω-is-set fe pe) Ω∀ ι
h-extends-ι : h ∘ η ∼ ι
h-extends-ι = 𝓛-extension-extends (Ω-is-set fe pe) Ω∀ ι
h-at-⊥-is-⊤ : h ⊥ ＝ ⊤Ω
h-at-⊥-is-⊤ = h ⊥ ＝⟨by-definition⟩
h (𝟘 , unique-from-𝟘 , 𝟘-is-prop) ＝⟨ h-explicitly ⊥ ⟩
(Ɐ a ꞉ 𝟘 , ι (unique-from-𝟘 a)) ＝⟨ I ⟩
(𝟙 , 𝟙-is-prop) ＝⟨by-definition⟩
⊤Ω ∎
where
I = Ω-extensionality pe fe (λ _ → ⋆) (λ (_ : 𝟙) (a : 𝟘) → 𝟘-elim a)
\end{code}
Now we assume that ∀Ω is freely generated by G with insertion of
generators ι, from which the principle of excluded will follow.
\begin{code}
module _ (Ω∀-is-free : is-free-𝓛-alg Ω∀ G ι) where
\end{code}
All we need to reach our desired conclusions is that the map h is an
equivalence, and so our assumption is slightly stronger than needed.
To show that h is an equivalence from this assumption, consider the
diagram below, where 𝓛 G is freely generated by G with insertion of
generators η, and Ω equipped with ∀ is freely generated by G with
insertion of generators ι. So the conclusion is a standard categorical
argument.
η
G ───────→ 𝓛 G
╲ │ ↑
╲ │ │
╲ │ │
ι ╲ h │ │ h⁻¹
╲ │ │
╲ │ │
╲ │ │
╲ ↓ │
➘ Ω.
Both 𝓛 G and Ω satisfy the universal property indicated in the above
diagram, with h being the unique homomorphism extending ι along η, and
h⁻¹ being the unique homomorphism extending η along ι.
\begin{code}
h-is-equiv : is-equiv h
h-is-equiv = unique-hom-is-equiv G
(𝓛-is-set fe fe pe G-is-set) (Ω-is-set fe pe) G-is-set
η ι 𝓛G Ω∀ 𝓛-is-free Ω∀-is-free
𝕙 : 𝓛 G ≃ Ω
𝕙 = h , h-is-equiv
h⁻¹ : Ω → 𝓛 G
h⁻¹ = ⌜ 𝕙 ⌝⁻¹
\end{code}
Using this, we in turn conclude that our assumed insertion of
generators ι : G → Ω is constantly ⊥.
The trick is, given a generator g : G, to consider the partial element
l : 𝓛 G defined by
l = (ι g holds , (λ _ → g) , _),
which will prove to be ⊥ : 𝓛 G, and to consider the partial element φ
of 𝓛 G with domain of definition `ι g holds` and constant value `η g`
for that purpose.
\begin{code}
ι-is-constantly-⊥ : (g : G) → ι g ＝ ⊥Ω
ι-is-constantly-⊥ g = III
where
i : is-prop (ι g holds)
i = holds-is-prop (ι g)
φ : ι g holds → 𝓛 G
φ _ = η g
I = h (⨆ i φ) ＝⟨ h-is-hom (ι g holds) i φ ⟩
(Ɐ a ꞉ ι g holds , h (φ a)) ＝⟨by-definition⟩
(Ɐ _ ꞉ ι g holds , h (η g)) ＝⟨by-definition⟩
ι g ⇒ h (η g) ＝⟨ ap (ι g ⇒_) (h-extends-ι g) ⟩
ι g ⇒ ι g ＝⟨ anything-implies-itself-is-⊤ pe (ι g) ⟩
⊤Ω ＝⟨ h-at-⊥-is-⊤ ⁻¹ ⟩
h ⊥ ∎
II = (ι g holds , (λ _ → g) , i) ＝⟨ II₀ ⟩
((ι g holds × 𝟙) , (λ _ → g) , _) ＝⟨by-definition⟩
⨆ i φ ＝⟨ equivs-are-lc h h-is-equiv I ⟩
⊥ ∎
where
II₀ = from-⋍ pe fe fe (((λ p → p , ⋆) , pr₁) , (λ _ → by-definition))
III : ι g ＝ ⊥Ω
III = to-Ω-＝ fe (ap is-defined II)
\end{code}
And from this we get the following characterization of h. For this
purpose, recall that is-def l is the domain of definition p = (P , i) : Ω
of the partial element l = (P , φ , i). In particular, notice that the
value of h at the argument l doesn't depend on φ : P → G. But we will
see that G ≃ 𝟙, so that φ doesn't do anything useful anyway.
The only thing going on in the following proof is that ι (φ a) ＝ ⊥Ω,
as proved above. The rest is just bureaucracy.
\begin{code}
h-more-explicitly : (l : 𝓛 G) → h l ＝ ⇁ is-def l
h-more-explicitly l@(P , φ , i) = I
where
I = h l ＝⟨ h-explicitly l ⟩
(Ɐ a ꞉ P , ι (φ a)) ＝⟨ I₀ ⟩
(Ɐ a ꞉ P , ⊥Ω) ＝⟨by-definition⟩
⇁ is-def l ∎
where
I₀ = Ω-extensionality pe fe
(λ f a → idtofun _ _ (ap _holds (ι-is-constantly-⊥ (φ a))) (f a))
(λ ν a → 𝟘-elim (ν a))
\end{code}
We say that a type is negative if it is logically equivalent to a
negated type. We have that a type is negative if and only if it is
¬¬-stable (because three negations imply one). By the above
characterization of h and the fact that h is an equivalence, every
proposition is negative, which means that the principle of excluded
middle holds.
\begin{code}
DNE-holds : (P : 𝓣 ̇) → is-prop P → ¬¬ P → P
DNE-holds P P-is-prop = V
where
p q : Ω
p = (P , P-is-prop)
q = is-def (h⁻¹ p)
Q : 𝓣 ̇
Q = q holds
I = p ＝⟨ (inverses-are-sections' 𝕙 p)⁻¹ ⟩
h (h⁻¹ p) ＝⟨ h-more-explicitly (h⁻¹ p) ⟩
⇁ is-def (h⁻¹ p) ＝⟨by-definition⟩
⇁ q ∎
II : P ＝ (⇁ q) holds
II = ap _holds I
III : P → ¬ Q
III g q = 𝟘-elim (idtofun P (Q → 𝟘) II g q)
IV : ¬ Q → P
IV ν = idtofun (Q → 𝟘) P (II ⁻¹) (λ (b : Q) → 𝟘-elim (ν b))
V : ¬¬ P → P
V = negative-types-are-¬¬-stable P (Q , III , IV)
EM-holds : (P : 𝓣 ̇) → is-prop P → P + ¬ P
EM-holds = DNE-gives-EM fe DNE-holds
\end{code}
This concludes the proof of the main result of this file, namely that
if Ω∀ is freely generated by any set G of generators with insertion of
generators ι : G → Ω, then the topos is boolean.
In principle, the hypothetical G and ι are arbitrary, but we already
know that ι must be constantly ⊥, and so it is not really arbitrary.
We now record that G isn't arbitrary either: we have that G ≃ 𝟙.
\begin{code}
G-is-prop : is-prop G
G-is-prop g₀ g₁ = II
where
I = h (η g₀) ＝⟨ h-extends-ι g₀ ⟩
ι g₀ ＝⟨ ι-is-constantly-⊥ g₀ ⟩
⊥Ω ＝⟨ (ι-is-constantly-⊥ g₁)⁻¹ ⟩
ι g₁ ＝⟨ (h-extends-ι g₁)⁻¹ ⟩
h (η g₁) ∎
II : g₀ ＝ g₁
II = embeddings-are-lc η
(η-is-embedding pe fe fe fe)
(equivs-are-lc h h-is-equiv I)
G-is-nonempty : ¬¬ G
G-is-nonempty G-is-empty = III
where
I : is-prop (𝓛 G)
I (P , φ , i) (Q , ψ , j) =
from-⋍ pe fe fe
(((λ (a : P) → 𝟘-elim (G-is-empty (φ a))) ,
(λ (b : Q) → 𝟘-elim (G-is-empty (ψ b)))) ,
(λ (a : P) → 𝟘-elim (G-is-empty (φ a))))
II : h⁻¹ ⊥Ω ≠ h⁻¹ ⊤Ω
II e = ⊥-is-not-⊤ (equivs-are-lc h⁻¹ ⌜ 𝕙 ⌝⁻¹-is-equiv e)
III : 𝟘
III = II (I (h⁻¹ ⊥Ω) (h⁻¹ ⊤Ω))
G-is-pointed : G
G-is-pointed = DNE-holds G G-is-prop G-is-nonempty
G-is-𝟙 : G ≃ 𝟙 {𝓣}
G-is-𝟙 = singletons-are-equiv-to-𝟙
(pointed-props-are-singletons G-is-pointed G-is-prop)
\end{code}
This shows that the only way Ω∀ can be freely generated is with a set
of generators G ≃ 𝟙 and inclusion of generators ι that is constantly ⊥.
Discussion. For interpreting the above results in a 1-topos, notice
that toposes validate propositional resizing, and so the two universes
𝓣 and 𝓣⁺ collapse to a single one, and in fact no universe is needed,
as the only reason 𝓣⁺ arises is that both Ω and 𝓛 G live in 𝓣⁺, rather
than 𝓣, in the absence of propositional resizing. However, Agda forces
us to work with at least one universe, as opposed to MLTT, although
this is inessential.
Concluding questions. The above gives *one* example of an algebra
which if it's free then excluded middle holds. There must be plenty
more. For example, a product of algebras is an algebra. Is a product
of free algebras also free? As a second example, do the algebras form
an exponential ideal: Is the algebra X → A free if the algebra A is?
These questions are answered positively in the following module:
\begin{code}
import Lifting.ProductsOfFreeAlgebrasAreFree
\end{code}
So, at present, we have only *one* example of an algebra which is not
free in all toposes.
Speculative question. Is there a nice characterization of the type of
all algebra structures on Ω? We have two "extreme" ones, namely ∃ and ∀.
There must be plenty in between. What does the type of all of them
look like?