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} The ideas presented here were originally obtained in a tortuous way, with more information than necessary to obtain the results, in the module Lifting.AnAlgebraWhichIsNotAlwaysFree-blackboard, which may nevertheless be interesting for other purposes. 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 Lifting.ProductsOfFreeAlgebrasAreFree. 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?