Martin Escardo, 7-8 November 2025, with revisions and additions to
the discussion 16, 20 and 24 November 2025.
----------------------------------------------------------------------------------
**Notice** This file is almost superseded by Lifting.AnAlgebraWhichIsNotAlwaysFree,
which has a stronger result with a simpler proof.
It is still interesting because (1) it has additional information, and
(2) it illustrates how we use TypeTopology as a blackboard to think
about mathematical ideas and develop them.
-----------------------------------------------------------------------------------
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 not all algebras are free in an arbitrary elementary topos.
Two examples where the failure occurs are Johnstone's Topological
Topos and Hyland's Effective Topos. More generally, we show that this
is the case in any topos in which the negation of 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. G is a non-empty subsingleton/proposition/truth value,
2. the insertion of generators ι : G → Ω is constantly ⊥,
3. the double negation of the principle of excluded middle holds, and, moreover,
4. G ≃ (principle of excluded middle).
The proof uses Higgs Involution Theorem.
TODO. But in principle it may still be the case that if Ω equipped
with ∀ is freely generated by a set of generators G, then the
principle of excluded middle holds, in which case (3) above reduces to
G ≃ 𝟙. We leave this as an open problem. (Added 24th November 2025. We
answer the question positively, with a simpler proof, which in
particular doesn't rely on Higgs Involution Theorem.)
Discussion added 16 November 2025.
Jon Sterling [1] previously conjectured that the same is 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 which 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 in TypeTopology.
It is also worth citing Kock's paper [3], which in particular shows
that, in the category of posets, structure maps are adjoint to units
of the monad, and hence are unique when they exist. What happens here
is that Ω has at least two structure maps (namely ∃ and ∀) and hence
two different orders according to [2]. In particular, Ω is a dcpo in
two different ways, each one with a unique structure map making it
into an algebra, both in the category of sets and in the category of
dcpos.
[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 #-}
open import MLTT.Spartan
open import UF.FunExt
open import UF.Subsingletons
\end{code}
We work with an arbitrary universe 𝓣, and assume function
extensionality and propositional extensionality, which are available
in any 1-topos.
\begin{code}
module Lifting.AnAlgebraWhichIsNotAlwaysFree-blackboard
(𝓣 : Universe)
(fe : Fun-Ext)
(pe : Prop-Ext)
where
private
fe' : FunExt
fe' 𝓤 𝓥 = fe {𝓤} {𝓥}
𝓣⁺ = 𝓣 ⁺
open import Higgs.InvolutionTheorem hiding (Ω)
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 Ω∀)
open import UF.ClassicalLogic
open import UF.DiscreteAndSeparated
open import UF.Embeddings
open import UF.Equiv
open import UF.Logic
open import UF.Sets
open import UF.Subsingletons-FunExt
open import UF.SubtypeClassifier renaming (Ω to Ω-of-universe ;
⊥ to ⊥Ω ;
⊤ to ⊤Ω)
open import UF.SubtypeClassifier-Properties
open Implication fe renaming (¬ₚ_ to ⇁_ ; ¬¬ₚ_ to ⇁⇁_)
open Universal fe
private
Ω : 𝓣⁺ ̇
Ω = Ω-of-universe 𝓣
\end{code}
We 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.
\begin{code}
module main-results
(G : 𝓣 ̇ )
(G-is-set : is-set G)
(ι : G → Ω)
where
\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 → Ω extending ι along η.
η
G ───────→ 𝓛 G
╲ │
╲ │
╲ │
ι ╲ h │
╲ │
╲ │
╲ │
╲ ↓
➘ Ω.
\begin{code}
open free-algebras-in-the-category-of-sets pe fe G G-is-set
h : 𝓛 G → Ω
h = 𝓛-extension (Ω-is-set fe pe) Ω∀ ι
h-explicitly : h ∼ λ (P , φ , i) → Ɐ a ꞉ P , ι (φ a)
h-explicitly _ = refl
𝓛G : 𝓛-alg (𝓛 G)
𝓛G = canonical-free-algebra
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) Ω∀ ι
\end{code}
We already know the following, but here is a simpler proof.
\begin{code}
every-element-of-𝓛-is-a-join : (l@(P , φ , i) : 𝓛 G) → l ＝ ⨆ i (λ (_ : P) → l)
every-element-of-𝓛-is-a-join l@(P , φ , i) =
from-⋍ pe fe fe
(((λ (a : P) → (a , a)) , pr₁) , λ (_ : P) → refl)
\end{code}
In order to reach our conclusions, we need to know a convenient
definition of h.
\begin{code}
useful-characterization-of-h : (l@(P , φ , i) : 𝓛 G)
→ h l ＝ ((P , i) ⇒ (Ɐ p ꞉ P , ι (φ p)))
useful-characterization-of-h l@(P , φ , i) =
h l ＝⟨ ap h (every-element-of-𝓛-is-a-join l) ⟩
h (⨆ i (λ _ → l)) ＝⟨ h-is-hom P i (λ _ → l) ⟩
(P , i) ⇒ (Ɐ p ꞉ P , ι (φ p)) ∎
\end{code}
With this we easily conclude that h maps ⊥ to ⊤.
\begin{code}
h-at-⊥-is-⊤ : h ⊥ ＝ ⊤Ω
h-at-⊥-is-⊤ =
h ⊥ ＝⟨ useful-characterization-of-h ⊥ ⟩
⊥Ω ⇒ (Ɐ q ꞉ 𝟘 , ι (unique-from-𝟘 q)) ＝⟨ I ⟩
⊤Ω ∎
where
I = ⊥⇒anything-is-⊤ pe (Ɐ q ꞉ 𝟘 , ι (unique-from-𝟘 q))
\end{code}
Notice that we didn't need to assume that Ω equipped with the
structure map ∀ is freely generated in order to conclude the above.
Now we assume, for the sake of eventually concluding that the double
negation of the principle of excluded middle holds, that Ω equipped
with the structure map ∀ is freely generated by G with insertion of
generators ι.
\begin{code}
module assumption
(Ω∀-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 Ω 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}
module E = free-algebra-eliminators
Ω∀ G ι Ω∀-is-free (𝓛-is-set fe fe pe G-is-set)
𝓛G η
h⁻¹ : Ω → 𝓛 G
h⁻¹ = E.unique-hom
h-is-equiv : is-equiv h
h-is-equiv = qinvs-are-equivs h (h⁻¹ , III , IV)
where
h⁻¹-is-hom : is-hom Ω∀ 𝓛G h⁻¹
h⁻¹-is-hom = E.unique-hom-is-hom
h⁻¹-extends-η : h⁻¹ ∘ ι ∼ η
h⁻¹-extends-η = E.unique-hom-is-extension
I : is-hom 𝓛G 𝓛G (h⁻¹ ∘ h)
I = ∘-is-hom 𝓛G Ω∀ 𝓛G h h⁻¹ h-is-hom h⁻¹-is-hom
II : is-hom Ω∀ Ω∀ (h ∘ h⁻¹)
II = ∘-is-hom Ω∀ 𝓛G Ω∀ h⁻¹ h h⁻¹-is-hom h-is-hom
III : h⁻¹ ∘ h ∼ id
III = at-most-one-extending-hom'
(h⁻¹ ∘ h , I)
(id , id-is-hom 𝓛G)
(λ l → h⁻¹ (h (η l)) ＝⟨ ap h⁻¹ (h-extends-ι l) ⟩
h⁻¹ (ι l) ＝⟨ h⁻¹-extends-η l ⟩
η l ∎)
(λ _ → refl)
where
open free-algebra-eliminators 𝓛G G η
𝓛-is-free (𝓛-is-set fe fe pe G-is-set) 𝓛G η
IV : h ∘ h⁻¹ ∼ id
IV = at-most-one-extending-hom'
(h ∘ h⁻¹ , II)
(id , id-is-hom Ω∀)
(λ p → h (h⁻¹ (ι p)) ＝⟨ ap h (h⁻¹-extends-η p) ⟩
h (η p) ＝⟨ h-extends-ι p ⟩
ι p ∎)
(λ _ → refl)
where
open free-algebra-eliminators
Ω∀ G ι Ω∀-is-free (Ω-is-set fe pe) Ω∀ ι
𝕙 : 𝓛 G ≃ Ω
𝕙 = h , h-is-equiv
\end{code}
Using this, we in turn conclude that our assumed map ι : G → Ω is
constantly ⊥.
\begin{code}
ι-is-constantly-⊥ : (g : G) → ι g ＝ ⊥Ω
ι-is-constantly-⊥ g = III
where
P : 𝓣 ̇
P = ι g holds
i : is-prop P
i = holds-is-prop (ι g)
ϕ : P → 𝓛 G
ϕ _ = η g
l : 𝓛 G
l = (P , (λ (_ : P) → g) , i)
I = h (⨆ i ϕ) ＝⟨ h-is-hom P i ϕ ⟩
ι g ⇒ h (η g) ＝⟨ ap (ι g ⇒_) (h-extends-ι g) ⟩
ι g ⇒ ι g ＝⟨ anything-implies-itself-is-⊤ pe (ι g) ⟩
⊤Ω ＝⟨ h-at-⊥-is-⊤ ⁻¹ ⟩
h ⊥ ∎
II = l ＝⟨ from-⋍ pe fe fe (((λ p → p , ⋆) , pr₁) , (λ _ → refl)) ⟩
⨆ i ϕ ＝⟨ equivs-are-lc h h-is-equiv I ⟩
⊥ ∎
III : ι g ＝ ⊥Ω
III = to-Ω-＝ fe (ap is-defined II)
\end{code}
And from this we conclude that the set G has at most one element.
\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)
\end{code}
It would be nice if we could conclude that G is pointed. All we can
conclude so far, however, is that G is nonempty.
\begin{code}
G-is-nonempty : ¬¬ G
G-is-nonempty u = III
where
I : is-prop (𝓛 G)
I (P , φ , i) (Q , ψ , j) = from-⋍ pe fe fe
(((λ p → 𝟘-elim (u (φ p))) ,
(λ q → 𝟘-elim (u (ψ q)))) ,
(λ p → 𝟘-elim (u (φ p))))
II : h⁻¹ ⊥Ω ≠ h⁻¹ ⊤Ω
II e = ⊥-is-not-⊤ (equivs-are-lc h⁻¹ ⌜ 𝕙 ⌝⁻¹-is-equiv e)
III : 𝟘
III = II (I (h⁻¹ ⊥Ω) (h⁻¹ ⊤Ω))
\end{code}
We already have an equivalence h⁻¹ : Ω → 𝓛 G, but now we look at
another one, which is in essence the canonical equivalence Ω ≃ 𝓛 𝟙. We
don't know that G ≃ 𝟙, but if we are given a point of G, we do know
this, as we already know that G is a proposition.
\begin{code}
γ : G → Ω ≃ 𝓛 G
γ g = qinveq v (u , (λ (_ : Ω) → refl) , vu)
where
u : 𝓛 G → Ω
u (P , φ , i) = (P , i)
v : Ω → 𝓛 G
v (P , i) = P , (λ _ → g) , i
vu : v ∘ u ∼ id
vu (P , φ , i) = from-⋍ pe fe fe ((id , id) , (λ p → G-is-prop g (φ p)))
\end{code}
Composing γ with h, we get an automorphism of Ω, with the following
explicit description and characterization.
\begin{code}
δ : G → Ω ≃ Ω
δ g = γ g ● 𝕙
δ-explicitly : (g : G) (p : Ω) → ⌜ δ g ⌝ p ＝ (p ⇒ ι g)
δ-explicitly g p = refl
δ-charac : (g : G) → (p : Ω) → ⌜ δ g ⌝ p ＝ ⇁ p
δ-charac g p = transport
(λ - → ⌜ δ g ⌝ p ＝ (p ⇒ -))
(ι-is-constantly-⊥ g)
(δ-explicitly g p)
\end{code}
That is, the map δ g is negation.
We now apply Higgs Involution Theorem to conclude that δ g is an
involution, as is any automorphism of Ω.
\begin{code}
δ-involutive : (g : G) → involutive ⌜ δ g ⌝
δ-involutive g = automorphisms-of-Ω-are-involutive fe pe ⌜ δ g ⌝ ⌜ δ g ⌝-is-equiv
\end{code}
But the involutivity of δ g says that (⇁⇁ p) = p for all p, which
amounts to the principle of excluded middle.
\begin{code}
G-pointed-gives-excluded-middle : G → EM 𝓣
G-pointed-gives-excluded-middle g = III
where
I : (p : Ω) → (⇁⇁ p) ＝ p
I p =
⇁⇁ p ＝⟨ (δ-charac g (p ⇒ ⊥Ω))⁻¹ ⟩
⌜ δ g ⌝ (⇁ p) ＝⟨ ap ⌜ δ g ⌝ ((δ-charac g p)⁻¹) ⟩
⌜ δ g ⌝ (⌜ δ g ⌝ p) ＝⟨ δ-involutive g p ⟩
p ∎
II : (P : 𝓣 ̇ ) → is-prop P → ¬¬ P → P
II P i ϕ = idtofun _ _ (ap _holds (I (P , i))) ϕ'
where
ϕ' : (P → 𝟘 {𝓣}) → 𝟘 {𝓣}
ϕ' u = 𝟘-elim (ϕ (λ p → 𝟘-elim (u p)))
III : (P : Set 𝓣) → is-prop P → P + ¬ P
III = DNE-gives-EM fe II
\end{code}
Because G is nonempty, we conclude that ¬¬ EM holds.
\begin{code}
the-double-negation-of-excluded-middle-holds : ¬¬ EM 𝓣
the-double-negation-of-excluded-middle-holds =
¬¬-functor G-pointed-gives-excluded-middle G-is-nonempty
\end{code}
We also have the following.
\begin{code}
excluded-middle-gives-G-pointed : EM 𝓣 → G
excluded-middle-gives-G-pointed em = EM-gives-DNE em G G-is-prop G-is-nonempty
\end{code}
So now we know what the hypothetical set G of generators is. It is the
principle of excluded middle!
\begin{code}
G-is-EM : G ≃ EM 𝓣
G-is-EM = logically-equivalent-props-are-equivalent
G-is-prop
(EM-is-prop fe')
G-pointed-gives-excluded-middle
excluded-middle-gives-G-pointed
\end{code}
This concludes the proof of all claims made above.
We originally developed some of the above ideas on paper, and then
more ideas here in Agda. Before summarizing explicitly our main result
and corollary, given below, we record some leftovers , which ended up
not being used in the proof of the above above claims, but which may
be interesting in their own right, and may be useful (or not) for
answering the questions below.
\begin{code}
𝔾 : Ω
𝔾 = (G , G-is-prop)
η' : G → 𝓛 G
η' g = G , (λ _ → g) , G-is-prop
η-agrees-with-η' : η ∼ η'
η-agrees-with-η' g = from-⋍ pe fe fe (((λ _ → g) , (λ _ → ⋆)) , (λ _ → refl))
\end{code}
Now we can use G to produce an element of 𝓛 G.
\begin{code}
l₀ : 𝓛 G
l₀ = G , id , G-is-prop
h-at-l₀-explicitly : h l₀ ＝ ∀[꞉]-syntax (l₀ .pr₁) (λ a → ι (l₀ .pr₂ .pr₁ a))
h-at-l₀-explicitly = h-explicitly l₀
l₀-is-not-⊥ : l₀ ≠ ⊥
l₀-is-not-⊥ e = G-is-nonempty (λ g → 𝟘-elim (idtofun _ _ I g))
where
I : G ＝ 𝟘
I = ap is-defined e
h-at-l₀ : h l₀ ＝ (Ɐ g ꞉ G , ι g)
h-at-l₀ = h-explicitly l₀
h-at-l₀' : h l₀ ＝ ⊥Ω
h-at-l₀' = false-gives-equal-⊥ pe fe _ (holds-is-prop _) I
where
I : ¬ ((Ɐ g ꞉ G , ι g) holds)
I f = G-is-nonempty G-is-empty
where
G-is-empty : ¬ G
G-is-empty g = ⊥-doesnt-hold (transport _holds (ι-is-constantly-⊥ g) II)
where
II : ι g holds
II = f g
l₀-partial-charac : (g : G) → l₀ ＝ η g
l₀-partial-charac g =
equivs-are-lc h h-is-equiv
(h l₀ ＝⟨ h-at-l₀' ⟩
⊥Ω ＝⟨ (ι-is-constantly-⊥ g)⁻¹ ⟩
ι g ＝⟨ (h-extends-ι g)⁻¹ ⟩
h (η g) ∎)
\end{code}
We summarize the main results of this file as follows.
\begin{code}
consequences-of-Ω∀-being-freely-generated
: (G : 𝓣 ̇ )
(G-is-set : is-set G)
(ι : G → Ω)
(Ω∀-is-free : is-free-𝓛-alg Ω∀ G ι)
→ ¬¬ EM 𝓣
× is-prop G
× ¬ is-empty G
× ((g : G) → ι g ＝ ⊥Ω)
× (G ≃ EM 𝓣)
consequences-of-Ω∀-being-freely-generated G G-is-set ι Ω∀-is-free
= the-double-negation-of-excluded-middle-holds ,
G-is-prop ,
G-is-nonempty ,
ι-is-constantly-⊥ ,
G-is-EM
where
open main-results G G-is-set ι
open assumption Ω∀-is-free
\end{code}
Notice that there is some redundancy in the conclusions.
In the introduction to this file, we claimed that if Ω equipped with
the lifting structure ∀ is freely generated by ⊥ : Ω, then the topos
is boolean. This is a particular case of the above development.
\begin{code}
corollary : is-free-𝓛-alg Ω∀ 𝟙 (λ ⋆ → ⊥Ω) → EM 𝓣
corollary Ω∀-is-freely-generated-by-⊥
= G-pointed-gives-excluded-middle ⋆
where
open main-results 𝟙 𝟙-is-set (λ ⋆ → ⊥Ω)
open assumption Ω∀-is-freely-generated-by-⊥
\end{code}
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.
We conclude with some questions, under the following assumptions:
\begin{code}
module _
(G : 𝓣 ̇ )
(G-is-set : is-set G)
(ι : G → Ω)
where
private
Ω∀-is-free = is-free-𝓛-alg Ω∀ G ι
\end{code}
The first question is whether our result is tight.
\begin{code}
Question₀ = ¬¬ EM 𝓣
→ is-free-𝓛-alg Ω∀ G ι
Question₀-variation₀ = ¬¬ EM 𝓣
→ G ≃ EM 𝓣
→ is-free-𝓛-alg Ω∀ G ι
Question₀-variation₁ = ¬¬ EM 𝓣
→ G ≃ EM 𝓣
→ ((g : G) → ι g ＝ ⊥Ω)
→ is-free-𝓛-alg Ω∀ G ι
\end{code}
The second question is whether our result can be improved as follows.
\begin{code}
Question₁ = is-free-𝓛-alg Ω∀ G ι
→ EM 𝓣
\end{code}
That is, any topos in which Ω∀ is free would be necessarily boolean.
(Added 24th November 2025. We answer Question₁ positively below.)
\begin{code}
of-course : Question₀ → Question₁ → (¬¬ EM 𝓣 → EM 𝓣)
of-course q₀ q₁ nnem = q₁ (q₀ nnem)
\end{code}
But there are toposes in which ¬¬ EM holds but EM fails (an example,
communicated to me by Andrew Swan, is the Sierpinski topos (*)), so the
two questions can't have a positive answer simultaneously in an
arbitrary topos.
(*) Luna Strah provided the following proof: EM in the topos of
sheaves over a topological space is the interior of the intersection
of all dense opens, which is the dense open set {1} for the Sierpinski
space, where 1 is the top point in the specialization order, and so
¬¬ EM is validated in the Sierpinski topos, but EM is not.
Added 21st November 2025.
Regarding (4) above, namely
4. G ≃ (principle of excluded middle),
Anders Kock proved in [3] above that if a lifting algebra is free,
then it is freely generated by its positive elements.
For Ω equipped with ∀ as its lifting structure, an element q : Ω is
positive iff ((p → q) → q) → p for all p : Ω.
It follows from this that:
(i) ⊥ is positive iff the principle of excluded middle (EM) holds.
(ii) If q : Ω is positive then q ＝ ⊥.
(iii) The set of positive elements is a subsingleton, which is
inhabited iff EM holds, that is,
(set of positive elements) ≃ (principle of excluded middle).
Added 24th November. Here is this proof written in Agda.
\begin{code}
Ω∀-positivity-charac→ : (q : Ω)
→ is-positive Ω∀ q
→ ((p : Ω) → (((p ⇒ q) ⇒ q) ⇒ p) holds)
Ω∀-positivity-charac→ q@(Q , Q-is-prop) q-is-pos p@(P , P-is-prop) = III
where
I : ((P → Q) , _) ＝ q → P
I = q-is-pos P P-is-prop
II : ((P → Q) → Q) → (P → Q) ＝ Q
II φ = pe (Π-is-prop fe (λ _ → Q-is-prop))
Q-is-prop
φ
(λ (b : Q) (a : P) → b)
III : ((P → Q) → Q) → P
III φ = I (to-Ω-＝ fe (II φ))
Ω∀-positivity-charac← : (q : Ω)
→ ((p : Ω) → (((p ⇒ q) ⇒ q) ⇒ p) holds)
→ is-positive Ω∀ q
Ω∀-positivity-charac← q@(Q , Q-is-prop) ϕ P P-is-prop e = II
where
I : (P → Q) → Q
I = idtofun (P → Q) Q (ap pr₁ e)
II : P
II = ϕ (P , P-is-prop) I
\end{code}
In the next two proofs there is an annoying universe conversion, to
translate between
ϕ' : (P → 𝟘 {𝓣}) → 𝟘 {𝓣}
and ¬¬ P, which amounts to
ϕ : (P → 𝟘 {𝓤₀}) → 𝟘 {𝓤₀}.
\begin{code}
⊥-∀-positive-gives-EM : is-positive Ω∀ ⊥Ω → EM 𝓣
⊥-∀-positive-gives-EM ⊥-is-pos = III
where
I : (P : 𝓣 ̇ ) → is-prop P → ((P → 𝟘 {𝓣}) → 𝟘 {𝓣}) → P
I P P-is-prop = Ω∀-positivity-charac→ ⊥Ω ⊥-is-pos (P , P-is-prop)
II : (P : 𝓣 ̇ ) → is-prop P → ((P → 𝟘 {𝓤₀}) → 𝟘 {𝓤₀}) → P
II P P-is-prop ϕ = I P P-is-prop ϕ'
where
ϕ' : (P → 𝟘 {𝓣}) → 𝟘 {𝓣}
ϕ' = λ (u : P → 𝟘 {𝓣}) → 𝟘-elim (ϕ (λ (a : P) → 𝟘-elim (u a)))
III : (P : 𝓣 ̇ ) → is-prop P → P + ¬ P
III = DNE-gives-EM fe II
EM-gives-⊥-∀-positive : EM 𝓣 → is-positive Ω∀ ⊥Ω
EM-gives-⊥-∀-positive em = III
where
I : (P : 𝓣 ̇ ) → is-prop P → ((P → 𝟘 {𝓤₀}) → 𝟘 {𝓤₀}) → P
I = EM-gives-DNE em
II : (p@(P , P-is-prop) : Ω) → ((P → 𝟘 {𝓣}) → 𝟘 {𝓣}) → P
II (P , P-is-prop) ϕ' = I P P-is-prop ϕ
where
ϕ : (P → 𝟘 {𝓤₀}) → 𝟘 {𝓤₀}
ϕ = λ (u : P → 𝟘 {𝓤₀}) → 𝟘-elim (ϕ' (λ (a : P) → 𝟘-elim (u a)))
III : is-positive Ω∀ ⊥Ω
III = Ω∀-positivity-charac← ⊥Ω II
\end{code}
For the following we take p ＝ ⊥Ω in the characterization of the
positivity.
\begin{code}
∀-positive-gives-equal-⊥ : (q : Ω) → is-positive Ω∀ q → q ＝ ⊥Ω
∀-positive-gives-equal-⊥ q@(Q , Q-is-prop) q-is-pos = II
where
I : ¬ Q
I b = 𝟘-elim I₁
where
I₁ : 𝟘 {𝓣}
I₁ = Ω∀-positivity-charac→ q q-is-pos ⊥Ω (λ (u : 𝟘 → Q) → b)
II : q ＝ ⊥Ω
II = fails-gives-equal-⊥ pe fe q I
\end{code}
Hence the positive elements form a subsingleton.
\begin{code}
the-∀-positive-props-form-a-prop : is-prop (Σ q ꞉ Ω , is-positive Ω∀ q)
the-∀-positive-props-form-a-prop (q , q-is-pos) (q' , q'-is-pos) =
to-subtype-＝
(being-positive-is-prop fe Ω∀)
(q ＝⟨ ∀-positive-gives-equal-⊥ q q-is-pos ⟩
⊥Ω ＝⟨ (∀-positive-gives-equal-⊥ q' q'-is-pos)⁻¹ ⟩
q' ∎)
\end{code}
And, moreover, any positive element gives excluded middle. Conversely,
excluded middle gives the (only) positive element ⊥Ω.
\begin{code}
the-∀-positive-props-form-a-type-equiv-to-EM
: (Σ q ꞉ Ω , is-positive Ω∀ q) ≃ EM 𝓣
the-∀-positive-props-form-a-type-equiv-to-EM
= logically-equivalent-props-are-equivalent
the-∀-positive-props-form-a-prop
(EM-is-prop fe')
(λ (q , q-is-pos) → ⊥-∀-positive-gives-EM
(transport
(is-positive Ω∀)
(∀-positive-gives-equal-⊥ q q-is-pos)
q-is-pos))
(λ em → (⊥Ω , EM-gives-⊥-∀-positive em))
\end{code}
Added 24th November 2025. We answer Question₁ above positively. This
gives a stronger result than what is claimed above, with a simpler and
shorter proof, which in particular doesn't appeal to Higgs Involution
Theorem.
\begin{code}
module stronger-result-with-simpler-proof
(G : 𝓣 ̇ )
(G-is-set : is-set G)
(ι : G → Ω)
(Ω∀-is-free : is-free-𝓛-alg Ω∀ G ι)
where
open main-results G G-is-set ι
open assumption Ω∀-is-free
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 , ⊥Ω) ＝⟨ refl ⟩
⇁ is-def l ∎
where
I₀ = Ω-extensionality pe fe
(λ f a → idtofun (ι (φ a) holds) (⊥Ω holds)
(ap _holds (ι-is-constantly-⊥ (φ a)))
(f a))
(λ (ν : P → 𝟘) (a : P) → 𝟘-elim (ν a))
\end{code}
We say that a proposition is negative if it is logically equivalent to
a negation. A proposition is negative if and only if it is ¬¬-stable
(because three negations imply one). By the above characterization of
h, as h is an equivalence, every proposition is negative, which means
that the principle of excluded middle holds.
\begin{code}
EM-holds : EM 𝓣
EM-holds = DNE-gives-EM fe DNE-holds
where
DNE-holds : (P : 𝓣 ̇) → is-prop P → ¬¬ P → P
DNE-holds P P-is-prop = VI
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) ⟩
⇁ 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 ⁻¹) (λ (a : Q) → 𝟘-elim (ν a))
V : ¬¬ P → ¬ Q
V = three-negations-imply-one ∘ ¬¬-functor III
VI : ¬¬ P → P
VI = IV ∘ V
\end{code}
We summarize this as follows.
\begin{code}
stronger-consequence-of-Ω∀-being-freely-generated
: (G : 𝓣 ̇ )
(G-is-set : is-set G)
(ι : G → Ω)
(Ω∀-is-free : is-free-𝓛-alg Ω∀ G ι)
→ EM 𝓣
stronger-consequence-of-Ω∀-being-freely-generated G G-is-set ι Ω∀-is-free
= EM-holds
where
open stronger-result-with-simpler-proof G G-is-set ι Ω∀-is-free
\end{code}
In other words,
\begin{code}
positive-answer-to-Question₁ : (G : 𝓣 ̇ )
(G-is-set : is-set G)
(ι : G → Ω)
→ Question₁ G G-is-set ι
positive-answer-to-Question₁ G G-is-set ι Ω∀-is-free =
stronger-consequence-of-Ω∀-being-freely-generated G G-is-set ι Ω∀-is-free
\end{code}