Martin Escardo, 2nd December 2025.

In any 1-topos, powers of Ω are free lifting algebras. This result
seems to new new.

The same argument directly generalizes to show that products of free
algebras are free, and this generalization is included in the file
ProductsOfFreeAlgebrasAreFree in the parent directory.

\begin{code}

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

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

module Lifting.PowersOfOmegaAreFreeAlgebras
        (fe : Fun-Ext)
        (pe : Prop-Ext)
        (pt : propositional-truncations-exist)
        (𝓣  : Universe)
        (X  : 𝓣 ̇ )
       where

open import Lifting.Construction 𝓣
open import Lifting.Algebras 𝓣
open import Lifting.Identity 𝓣
open import Lifting.TwoAlgebrasOnOmega 𝓣 fe pe
open import UF.Embeddings
open import UF.Equiv
open import UF.Logic
open import UF.Sets
open import UF.Sets-Properties
open import UF.Subsingletons-FunExt
open import UF.Subsingletons-Properties
open import UF.SubtypeClassifier-Properties
open import UF.SubtypeClassifier renaming (Ω to Ω-of-universe)

private
 Ω : 𝓣 ⁺ ̇
 Ω = Ω-of-universe 𝓣

 fe' : FunExt
 fe' 𝓤 𝓥 = fe {𝓤} {𝓥}

open PropositionalTruncation pt
open Conjunction

\end{code}

Our objective is to show that the algebra Ωˣ is free. We know it is
an algebra because it is a product of copies of the (free) algebra Ω.

\begin{code}

Ωˣ : 𝓣 ⁺ ̇
Ωˣ = X → Ω

\end{code}

We let π range over Ωˣ.

\begin{code}

Ωˣ-is-set : is-set Ωˣ
Ωˣ-is-set = Π-is-set fe (λ (_ : X) → Ω-is-set fe pe)

Ωˣ-𝓛-alg : 𝓛-alg Ωˣ
Ωˣ-𝓛-alg = Π-is-alg fe (λ (_ : X) → Ω) (λ (_ : X) → Σ-alg-on-Ω)

∐ : extension-op Ωˣ
∐ = 𝓛-alg-structure-map Ωˣ-𝓛-alg

\end{code}

We now consider a notion of positivity for elements of Ω ˣ (which
agrees with Anders Kock's notion of positivity for this particular
algebra, but we don't need to know this here).

\begin{code}

is-pos : Ωˣ → 𝓣 ̇
is-pos π = ∃ x ꞉ X , π x holds

being-pos-is-prop : (π : Ωˣ) → is-prop (is-pos π)
being-pos-is-prop π = ∃-is-prop

is-Pos : Ωˣ → Ω
is-Pos π = is-pos π , being-pos-is-prop π

\end{code}

We will show that Ωˣ is freely generated by its set G of positive
elements, with insertion of generators the embedding ι of G into Ωˣ.

\begin{code}

G : 𝓣 ⁺ ̇
G = Σ π ꞉ Ωˣ , is-pos π

G-is-set : is-set G
G-is-set = Σ-is-set Ωˣ-is-set (λ (π : Ωˣ) → props-are-sets (being-pos-is-prop π))

ι : G → Ωˣ
ι = pr₁

ι-is-pos : (g : G) → is-pos (ι g)
ι-is-pos = pr₂

ι-is-embedding : is-embedding ι
ι-is-embedding = pr₁-is-embedding being-pos-is-prop

\end{code}

Our first step is to show that Ωˣ is equivalent to 𝓛 G, the canonical
algebra freely generated by G with insertion of generators η : G → 𝓛 G.

\begin{code}

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 Ωˣ-𝓛-alg ι

h-explicitly : (l@(P , φ , i) : 𝓛 G)
             → h l ＝ λ x → ∑ (λ (p : P) → ι (φ p) x)
h-explicitly l = by-definition

h-is-hom : is-hom 𝓛G Ωˣ-𝓛-alg h
h-is-hom = 𝓛-extension-is-hom Ωˣ-is-set Ωˣ-𝓛-alg ι

h-extends-ι : h ∘ η ∼ ι
h-extends-ι = 𝓛-extension-extends Ωˣ-is-set Ωˣ-𝓛-alg ι

\end{code}

Our aim is to fill this diagram with a homomorphism h⁻¹ inverting h so
that Ωˣ is isomorphic to 𝓛 G as a lifting algebra:

       η
  G ────────→ 𝓛 G
   ╲         │  ↑
    ╲        │  │
     ╲       │  │
    ι ╲    h │  │ h⁻¹
       ╲     │  │
        ╲    │  │
         ╲   │  │
          ╲  ↓  │
           ➘  Ωˣ.

The only insight in this file is the definition of h⁻¹. Everything
else is just hard work.

\begin{code}

h⁻¹ : Ωˣ → 𝓛 G
h⁻¹ π = is-pos π , (λ (i : is-pos π) → π , i) , being-pos-is-prop π

h⁻¹-is-section : h ∘ h⁻¹ ∼ id
h⁻¹-is-section π =
 h (h⁻¹ π)                          ＝⟨ h-explicitly (h⁻¹ π) ⟩
 (λ x → ∑ (λ (_ : is-pos π) → π x)) ＝⟨by-definition⟩
 (λ x → is-Pos π ∧ π x)             ＝⟨ I ⟩
 (λ x → π x)                        ＝⟨by-definition⟩
 π                                  ∎
  where
   I = dfunext fe (λ x → Ω-extensionality pe fe
                          pr₂
                          (λ (d : π x holds) → ∣ x , d ∣ , d))

\end{code}

To show that h⁻¹ is also a retraction, and that it is a homomorphism,
we will use the following two definitional equalities tacitly.

\begin{code}

module _
        (l@(P , φ , i) : 𝓛 G)
        (φ : P → Ωˣ)
       where

 NB₀ : is-defined (h⁻¹ (∐ i φ)) ＝ (∃ x ꞉ X , Σ p ꞉ P , φ p x holds)
 NB₀ = by-definition

 NB₁ : is-defined (⨆ i (h⁻¹ ∘ φ)) ＝ (Σ p ꞉ P , ∃ x ꞉ X , φ p x holds)
 NB₁ = by-definition

h⁻¹-is-retraction : h⁻¹ ∘ h ∼ id
h⁻¹-is-retraction l@(P , φ , i) = V
 where
  I : (∃ x ꞉ X , Σ p ꞉ P , ι (φ p) x holds) → P
  I = ∥∥-rec i (λ (x , p , d) → p)

  II : P → ∃ x ꞉ X , Σ p ꞉ P , ι (φ p) x holds
  II p = ∥∥-rec ∃-is-prop (λ (x , d) → ∣ x , p , d ∣) e
   where
    e : ∃ x ꞉ X , ι (φ p) x holds
    e = ι-is-pos (φ p)

  III : {e : ∃ x ꞉ X , Σ p ꞉ P , ι (φ p) x holds}
      → (λ x → ∑ (λ (p : P) → ι (φ p) x)) ＝ ι (φ (I e))
  III {e} = dfunext fe (λ x → to-subtype-＝ (λ _ → being-prop-is-prop fe) (I₀ x))
   where
    I₀ : (x : X) → (Σ p ꞉ P , ι (φ p) x holds) ＝ (ι (φ (I e)) x holds)
    I₀ x = pe (Σ-is-prop i (λ p → holds-is-prop (ι (φ p) x)))
              (holds-is-prop (ι (φ (I e)) x))
              (λ (p , d) → transport (λ - → ι (φ -) x holds) (i p (I e)) d)
              (λ (d : ι (φ (I e)) x holds) → I e , d)

  IV : value (h⁻¹ (h l)) ∼ (λ x → φ (I x))
  IV e = to-subtype-＝ being-pos-is-prop (III {e})

  V : h⁻¹ (h l) ＝ l
  V = from-⋍ pe fe fe ((I , II) , IV)

\end{code}

So Ωˣ is equivalent to the underlying type of a free algebra

\begin{code}

Ωˣ-is-𝓛G : Ωˣ ≃ 𝓛 G
Ωˣ-is-𝓛G = qinveq h⁻¹ (h , h⁻¹-is-section , h⁻¹-is-retraction)

\end{code}

The equivalence is an algebra homomorphism.

\begin{code}

h⁻¹-is-hom : is-hom Ωˣ-𝓛-alg 𝓛G h⁻¹
h⁻¹-is-hom P i φ = IV
 where
  I : (∃ x ꞉ X , Σ p ꞉ P , φ p x holds) → (Σ p ꞉ P , ∃ x ꞉ X , φ p x holds)
  I = ∥∥-rec (Σ-is-prop i λ _ → ∃-is-prop) (λ (x , p , d) → p , ∣ x , d ∣)

  II : (Σ p ꞉ P , ∃ x ꞉ X , φ p x holds) → (∃ x ꞉ X , Σ p ꞉ P , φ p x holds)
  II (p , e) = ∥∥-functor (λ (x , d) → x , p , d) e

  III : value (h⁻¹ (∐ i φ)) ∼ (λ x → value (⨆ i (h⁻¹ ∘ φ)) (I x))
  III e = III₁
   where
    p : P
    p = pr₁ (I e)

    III₀ : ∐ i φ ＝ φ p
    III₀ = 𝓛-alg-Law₀-gives₀' pe fe fe ∐ (𝓛-alg-law₀ Ωˣ-𝓛-alg) P i φ p

    III₁ : (∐ i φ , e) ＝ (φ p , pr₂ (I e))
    III₁ = to-subtype-＝ being-pos-is-prop III₀

  IV : h⁻¹ (∐ i φ) ＝ ⨆ i (h⁻¹ ∘ φ)
  IV = from-⋍ pe fe fe ((I , II) , III)

\end{code}

This shows that Ωˣ equipped with the algebra structure Ωˣ-𝓛-alg is
isomorphic to the free algebra 𝓛 G in the category of algebras, and
hence is itself free.

\begin{code}

Ωˣ-is-free-𝓛-alg : is-free-𝓛-alg Ωˣ-𝓛-alg G ι
Ωˣ-is-free-𝓛-alg = 𝓛-alg-isomorphic-to-free-𝓛-alg-is-itself-free pe fe
                    Ωˣ-is-set
                    G
                    G-is-set
                    ι
                    Ωˣ-𝓛-alg
                    h⁻¹
                    h⁻¹-is-section
                    h⁻¹-is-retraction
                    h⁻¹-is-hom
\end{code}