Lifting.PowersOfOmegaAreFreeAlgebras
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.{-# 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 ConjunctionOur 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 Ω.Ωˣ : 𝓣 ⁺ ̇ Ωˣ = X → ΩWe let π range over Ωˣ.Ωˣ-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 Ωˣ-𝓛-algWe 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).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 πWe will show that Ωˣ is freely generated by its set G of positive elements, with insertion of generators the embedding ι of G into Ωˣ.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-propOur first step is to show that Ωˣ is equivalent to 𝓛 G, the canonical algebra freely generated by G with insertion of generators η : G → 𝓛 G.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 ι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.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))To show that h⁻¹ is also a retraction, and that it is a homomorphism, we will use the following two definitional equalities tacitly.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)So Ωˣ is equivalent to the underlying type of a free algebra.Ωˣ-is-𝓛G : Ωˣ ≃ 𝓛 G Ωˣ-is-𝓛G = qinveq h⁻¹ (h , h⁻¹-is-section , h⁻¹-is-retraction)The equivalence is an algebra homomorphism.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)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.Ωˣ-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