Martin Escardo, 7-8 November 2025, with revisions and additions to
the discussion 16 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 not all algebras are free in an arbitrary elementary topos.

An example where the failure occurs is Johnstone's Topological
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 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 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.

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 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.

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 propostitional extensionality, which are available
in any 1-topos.

\begin{code}

module Lifting.AnAlgebraWhichIsNotAlwaysFree
        (𝓣 : 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
open import UF.Base
open import UF.ClassicalLogic
open import UF.Embeddings
open import UF.Equiv
open import UF.Logic
open import UF.Sets
open import UF.SubtypeClassifier renaming (Ω to Ω-of-universe ;
                                           ⊥ to ⊥Ω ;
                                           ⊤ to ⊤Ω)
open import UF.SubtypeClassifier-Properties

open Implication fe renaming (¬ₚ_ to ⇁_ ; ¬¬ₚ_ 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}

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 η.

\begin{code}

 open free-algebras-in-the-category-of-sets pe fe G G-is-set

 h : 𝓛 G → Ω
 h = 𝓛-extension (Ω-is-set fe pe) Π-algebra-on-Ω ι

 h-explicitly : h ∼ λ (P , φ , i) → Ɐ p ꞉ P , ι (φ p)
 h-explicitly _ = refl

 h-is-hom : is-hom free Π-algebra-on-Ω h
 h-is-hom = 𝓛-extension-is-hom (Ω-is-set fe pe) Π-algebra-on-Ω ι

 h-extends-ι : h ∘ η ∼ ι
 h-extends-ι = 𝓛-extension-extends (Ω-is-set fe pe) Π-algebra-on-Ω ι

\end{code}

To achieve our objectives stated above, we will eventually assume that
h is an equivalence, so that Ω equipped with ⨆ = Π is also freely
generated by G.

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
   (((λ (p : P) → (p , p)) , 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) ⇒ (Ɐ q ꞉ P , ι (φ q)))
 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) ⇒ (Ɐ q ꞉ P , ι (φ q)) ∎

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

Now we assume, for the sake of concluding the double negation of the
principle of excluded middle, that h is an equivalence.

\begin{code}

 module assumption (h-is-equiv : is-equiv h) where

  𝕙 : 𝓛 G ≃ Ω
  𝕙 = h , h-is-equiv

  h⁻¹ : Ω → 𝓛 G
  h⁻¹ = ⌜ 𝕙 ⌝⁻¹

\end{code}

With this assumption, we 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. We conclude with 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.

\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

  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}