Martin Escardo, 7-8 Novemeber 2025.

Not all algebras of the partial-map classifier (aka lifting) monad are free.

In a boolean 1-topos, every algebra of the lifting monad is a free algebra.

John Sterling [1] asked whether this is the case in *all* toposes.

[1] https://doi.org/10.48550/arXiv.2312.17023

We show that it isn't.

For example, it fails in Johnstone's Topological topos. More
generally, we show that it fails 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 ⨆ = ∃ or ⨆ = ∀.

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 double negation of the principle of excluded middle holds, and, moreover,
 3. G ≃ (principle of excluded middle).

So the answer is negative.

The proof uses Higgs Involution Theorem.

\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 give 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 , (λ z → 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}