Martin Escardo, 5th December 2025.

In any 1-topos, products of free lifting algebras are themselves
free. This result seems to be new.

\begin{code}

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

\end{code}

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.

\begin{code}

import Lifting.PowersOfOmegaAreFreeAlgebras

\end{code}

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

\begin{code}

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

\end{code}

The 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 _ = 𝟙.

\begin{code}

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

\end{code}

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.

\begin{code}

𝓐 : 𝓛-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 𝓐 ι

\end{code}

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.

\begin{code}

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
    III₀ : (x : X) → (Σ p ꞉ P , is-defined (ι (φ p) x)) → is-defined (ι (φ (I e)) x)
    III₀ x (p , d) = transport (λ - → is-defined (ι (φ -) x)) (i p (I e)) d

    III₁ : (x : X) → is-defined (ι (φ (I e)) x) → (Σ p ꞉ P , is-defined (ι (φ p) x))
    III₁ x d = I e , d

    III₂ : (x : X) (σ : Σ p ꞉ P , is-defined (ι (φ p) x))
         → value (∑ x {P , i} (λ (p : P) → ι (φ p) x)) σ ＝ value (ι (φ (I e)) x) (III₀ x σ)
    III₂ x (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₀ x (p , d))                            ＝⟨by-definition⟩
     value (ι (φ (I e)) x) (III₀ x (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₀ x (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)

\end{code}

So the product (A , 𝓐) of the free algebras is itself free, with
insertion of generators ι : G → A.

\begin{code}

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
\end{code}