Lifting.AnAlgebraWhichIsNotAlwaysFree-blackboard

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


{-# OPTIONS --safe --without-K #-}

open import MLTT.Spartan
open import UF.FunExt
open import UF.Subsingletons


We work with an arbitrary universe 𝓣, and assume function
extensionality and propositional extensionality, which are available
in any 1-topos.


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 𝓣


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.


module main-results
        (G : 𝓣 ̇ )
        (G-is-set : is-set G)
        (ι : G → Ω)
       where


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  │
       ╲      │
        ╲     │
         ╲    │
          ╲   ↓
           ➘  Ω.


 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) Ω∀ ι


We already know the following, but here is a simpler proof.


 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)


In order to reach our conclusions, we need to know a convenient
definition of h.


 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)) ∎


With this we easily conclude that h maps ⊥ to ⊤.


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


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


 module assumption
         (Ω∀-is-free : is-free-𝓛-alg Ω∀ G ι)
        where


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


  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


Using this, we in turn conclude that our assumed map ι : G → Ω is
constantly ⊥.


  ι-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)


And from this we conclude that the set G has at most one element.


  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)


It would be nice if we could conclude that G is pointed. All we can
conclude so far, however, is that G is nonempty.


  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⁻¹ ⊤Ω))


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.


  γ : 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)))


Composing γ with h, we get an automorphism of Ω, with the following
explicit description and characterization.


  δ : 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)


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


  δ-involutive : (g : G) → involutive ⌜ δ g ⌝
  δ-involutive g = automorphisms-of-Ω-are-involutive fe pe  ⌜ δ g ⌝ ⌜ δ g ⌝-is-equiv


But the involutivity of δ g says that (⇁⇁ p) = p for all p, which
amounts to the principle of excluded middle.


  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


Because G is nonempty, we conclude that ¬¬ EM holds.


  the-double-negation-of-excluded-middle-holds : ¬¬ EM 𝓣
  the-double-negation-of-excluded-middle-holds =
   ¬¬-functor G-pointed-gives-excluded-middle G-is-nonempty


We also have the following.


  excluded-middle-gives-G-pointed : EM 𝓣 → G
  excluded-middle-gives-G-pointed em = EM-gives-DNE em G G-is-prop G-is-nonempty


So now we know what the hypothetical set G of generators is. It is the
principle of excluded middle!


  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


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.


  𝔾 : Ω
  𝔾 = (G , G-is-prop)

  η' : G → 𝓛 G
  η' g = G , (λ _ → g) , G-is-prop

  η-agrees-with-η' : η ∼ η'
  η-agrees-with-η' g = from-⋍ pe fe fe (((λ _ → g) , (λ _ → ⋆)) , (λ _ → refl))


Now we can use G to produce an element of 𝓛 G.


  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) ∎)


We summarize the main results of this file as follows.


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


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.


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


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:


module _
        (G : 𝓣 ̇ )
        (G-is-set : is-set G)
        (ι : G → Ω)
       where

 private
  Ω∀-is-free = is-free-𝓛-alg Ω∀ G ι


The first question is whether our result is tight.


 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 ι

The second question is whether our result can be improved as follows.


 Question₁ = is-free-𝓛-alg Ω∀ G ι
           → EM 𝓣


That is, any topos in which Ω∀ is free would be necessarily boolean.
(Added 24th November 2025. We answer Question₁ positively below.)


 of-course : Question₀ → Question₁ → (¬¬ EM 𝓣 → EM 𝓣)
 of-course q₀ q₁ nnem = q₁ (q₀ nnem)


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.


Ω∀-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


In the next two proofs there is an annoying universe conversion, to
translate between

ϕ' : (P → 𝟘 {𝓣}) → 𝟘 {𝓣}

and ¬¬ P, which amounts to

ϕ : (P → 𝟘 {𝓤₀}) → 𝟘 {𝓤₀}.


⊥-∀-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


For the following we take p ＝ ⊥Ω in the characterization of the
positivity.


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


Hence the positive elements form a subsingleton.


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' ∎)


And, moreover, any positive element gives excluded middle. Conversely,
excluded middle gives the (only) positive element ⊥Ω.


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


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.


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


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.


 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


We summarize this as follows.


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


In other words,


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