Lifting.ProductsOfFreeAlgebrasAreFree
Martin Escardo, 5th December 2025. In any 1-topos, products of free lifting algebras are themselves free. This result seems to be new.{-# OPTIONS --safe --without-K #-}This file generalizes the following file, in a more or less straightforward way, whose result also seem to be new, which shows that powers of Ω are free lifting algebras.import Lifting.PowersOfOmegaAreFreeAlgebrasTherefore we have decided to remove most of the discussion, to avoid repetition. So readers who wish to understand the motivation for proving this, and how the proof here works, are advised to first look at the above file.open import MLTT.Spartan open import UF.FunExt open import UF.Subsingletons open import UF.PropTrunc open import UF.Sets module Lifting.ProductsOfFreeAlgebrasAreFree (fe : Fun-Ext) (pe : Prop-Ext) (pt : propositional-truncations-exist) (𝓣 𝓤 : Universe) (X : 𝓣 ̇ ) (K : X → 𝓤 ̇ ) (K-is-set : (x : X) → is-set (K x)) whereThe sets K x are the generators for the free algebras of which we will take the product, which replace Ω ≃ 𝓛 𝟙 in the file mentioned above. So, to recover the results of that file, take K _ = 𝟙.open import Lifting.Construction 𝓣 open import Lifting.Algebras 𝓣 open import Lifting.Identity 𝓣 open import UF.Embeddings open import UF.Equiv open import UF.Logic 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 𝓛K : (x : X) → 𝓛-alg (𝓛 (K x)) 𝓛K x = canonical-free-algebra where open free-algebras-in-the-category-of-sets pe fe (K x) (K-is-set x) ∑ : (x : X) {p : Ω} → (p holds → 𝓛 (K x)) → 𝓛 (K x) ∑ x {p} = 𝓛-alg-structure-map (𝓛K x) (holds-is-prop p) A : 𝓣⁺ ⊔ 𝓤 ̇ A = (x : X) → 𝓛 (K x) A-is-set : is-set A A-is-set = Π-is-set fe (λ (x : X) → 𝓛-is-set fe fe pe (K-is-set x))We denote by 𝓐 the lifting structure on the product A of the free algebras 𝓛 (K x). Our objective is to show that A equipped with 𝓐 is a an algebra freely generated by a suitable set G of generators defined below.𝓐 : 𝓛-alg A 𝓐 = Π-is-alg fe (λ x → 𝓛 (K x)) 𝓛K ∐ : extension-op A ∐ = 𝓛-alg-structure-map 𝓐 is-pos : A → 𝓣 ̇ is-pos a = ∃ x ꞉ X , is-defined (a x) being-pos-is-prop : (a : A) → is-prop (is-pos a) being-pos-is-prop a = ∃-is-prop G : 𝓣⁺ ⊔ 𝓤 ̇ G = Σ a ꞉ A , is-pos a G-is-set : is-set G G-is-set = Σ-is-set A-is-set (λ (a : A) → props-are-sets (being-pos-is-prop a)) ι : G → A ι = pr₁ ι-is-pos : (g : G) → is-pos (ι g) ι-is-pos = pr₂ ι-is-embedding : is-embedding ι ι-is-embedding = pr₁-is-embedding being-pos-is-prop open free-algebras-in-the-category-of-sets pe fe G G-is-set 𝓛G : 𝓛-alg (𝓛 G) 𝓛G = canonical-free-algebra h : 𝓛 G → A h = 𝓛-extension A-is-set 𝓐 ι h-explicitly : (l@(P , φ , i) : 𝓛 G) → h l ＝ λ x → ∑ x (λ (p : P) → ι (φ p) x) h-explicitly l = by-definition h-is-hom : is-hom 𝓛G 𝓐 h h-is-hom = 𝓛-extension-is-hom A-is-set 𝓐 ι h-extends-ι : h ∘ η ∼ ι h-extends-ι = 𝓛-extension-extends A-is-set 𝓐 ιIn the remainder of this file we show that h has a two-sided inverse h⁻¹ that is an algebra homomomorphism, from which is follows that the product algebra (A , 𝓐) is freely generated by G.h⁻¹ : A → 𝓛 G h⁻¹ a = is-pos a , (λ (i : is-pos a) → a , i) , being-pos-is-prop a h⁻¹-is-section : h ∘ h⁻¹ ∼ id h⁻¹-is-section a = h (h⁻¹ a) ＝⟨ h-explicitly (h⁻¹ a) ⟩ (λ x → ∑ x (λ (_ : is-pos a) → a x)) ＝⟨ I ⟩ a ∎ where I = dfunext fe (λ x → from-⋍ pe fe fe ((pr₂ , (λ (d : is-defined (a x)) → ∣ x , d ∣ , d)) , (λ _ → refl))) h⁻¹-is-retraction : h⁻¹ ∘ h ∼ id h⁻¹-is-retraction l@(P , φ , i) = V where I : (∃ x ꞉ X , Σ p ꞉ P , is-defined (ι (φ p) x)) → P I = ∥∥-rec i (λ (x , p , h) → p) II : P → ∃ x ꞉ X , Σ p ꞉ P , is-defined(ι (φ p) x) II p = ∥∥-rec ∃-is-prop (λ (x , h) → ∣ x , p , h ∣) e where e : ∃ x ꞉ X , is-defined(ι (φ p) x) e = ι-is-pos (φ p) III : {e : ∃ x ꞉ X , Σ p ꞉ P , is-defined(ι (φ p) x)} → (λ x → ∑ x (λ (p : P) → ι (φ p) x)) ＝ ι (φ (I e)) III {e} = dfunext fe (λ x → from-⋍ pe fe fe ((III₀ x , III₁ x) , III₂ x)) where module _ (x : X) where III₀ : (Σ p ꞉ P , is-defined (ι (φ p) x)) → is-defined (ι (φ (I e)) x) III₀ (p , d) = transport (λ - → is-defined (ι (φ -) x)) (i p (I e)) d III₁ : is-defined (ι (φ (I e)) x) → (Σ p ꞉ P , is-defined (ι (φ p) x)) III₁ d = I e , d III₂ : (σ : Σ p ꞉ P , is-defined (ι (φ p) x)) → value (∑ x {P , i} (λ (p : P) → ι (φ p) x)) σ ＝ value (ι (φ (I e)) x) (III₀ σ) III₂ (p , d) = value (∑ x {P , i} (λ (p : P) → ι (φ p) x)) (p , d) ＝⟨by-definition⟩ value (ι (φ p) x) d ＝⟨by-definition⟩ ν (p , d) ＝⟨ III₂₀ ⟩ ν (I e , III₀ (p , d)) ＝⟨by-definition⟩ value (ι (φ (I e)) x) (III₀ (p , d)) ∎ where ν : (Σ p ꞉ P , is-defined (ι (φ p) x)) → K x ν (p , d) = value (ι (φ p) x) d III₂₀ = ap ν (being-defined-is-prop (∑ x {P , i} (λ (p : P) → ι (φ p) x)) (p , d) (I e , III₀ (p , 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) A-is-𝓛G : A ≃ 𝓛 G A-is-𝓛G = qinveq h⁻¹ (h , h⁻¹-is-section , h⁻¹-is-retraction) h⁻¹-is-hom : is-hom 𝓐 𝓛G h⁻¹ h⁻¹-is-hom P i φ = IV where I : (∃ x ꞉ X , Σ p ꞉ P , is-defined (φ p x)) → (Σ p ꞉ P , ∃ x ꞉ X , is-defined (φ p x)) I = ∥∥-rec (Σ-is-prop i (λ _ → ∃-is-prop)) (λ (x , p , d) → p , ∣ x , d ∣) II : (Σ p ꞉ P , ∃ x ꞉ X , is-defined (φ p x)) → (∃ x ꞉ X , Σ p ꞉ P , is-defined (φ p x)) 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₀ 𝓐) 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)So the product (A , 𝓐) of the free algebras is itself free, with insertion of generators ι : G → A.A-is-free-𝓛-alg : is-free-𝓛-alg 𝓐 G ι A-is-free-𝓛-alg = 𝓛-alg-isomorphic-to-free-𝓛-alg-is-itself-free pe fe A-is-set G G-is-set ι 𝓐 h⁻¹ h⁻¹-is-section h⁻¹-is-retraction h⁻¹-is-hom