Martin Escardo 17th December 2018. (This has a connection with injectivity.)

We have a look at the algebras of the lifting monad.

\begin{code}

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

open import MLTT.Spartan

module Lifting.Algebras
        (𝓣 : Universe)
       where

open import UF.Base
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.FunExt
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.UA-FunExt
open import UF.Univalence

open import Lifting.Construction 𝓣
open import Lifting.Identity 𝓣
open import Lifting.Monad 𝓣

\end{code}

An element of 𝓛 (𝓛 X) amounts to a family of partial elements of X
indexed by a proposition:

\begin{code}

double-𝓛-charac : (X : 𝓀 Μ‡ )
                β†’ 𝓛 (𝓛 X) ≃ (Ξ£ P κž‰ 𝓣 Μ‡
                                 , (Ξ£ Q κž‰ (P β†’ 𝓣 Μ‡ )
                                        , ((p : P) β†’ Q p β†’ X)
                                        Γ— ((p : P) β†’ is-prop (Q p)))
                                 Γ— is-prop P)
double-𝓛-charac X = Ξ£-cong (Ξ» P β†’ Γ—-cong (Ξ³ X P) (≃-refl (is-prop P)))
 where
  Ξ³ : (X : 𝓀 Μ‡ ) (P : 𝓣 Μ‡ )
    β†’ (P β†’ 𝓛 X)
    ≃ (Ξ£ Q κž‰ (P β†’ 𝓣 Μ‡ ), ((p : P) β†’ Q p β†’ X) Γ— ((p : P) β†’ is-prop (Q p)))
  Ξ³ X P =
   (P β†’ Ξ£ Q κž‰ 𝓣 Μ‡ , (Q β†’ X) Γ— is-prop Q)                                 β‰ƒβŸ¨ I ⟩
   (Ξ£ Q κž‰ (P β†’ 𝓣 Μ‡ ), ((p : P) β†’ ((Q p β†’ X) Γ— is-prop (Q p))))           β‰ƒβŸ¨ II ⟩
   (Ξ£ Q κž‰ (P β†’ 𝓣 Μ‡ ), ((p : P) β†’ Q p β†’ X) Γ— ((p : P) β†’ is-prop (Q p)))   β– 
    where
     I  = Ξ Ξ£-distr-≃
     II = Ξ£-cong (Ξ» Q β†’ β†’Γ—)

\end{code}

The usual definition of algebra of a monad and construction of free
algebras:

\begin{code}

𝓛-algebra : 𝓀 Μ‡ β†’ 𝓣 ⁺ βŠ” 𝓀 Μ‡
𝓛-algebra X = Ξ£ s κž‰ (𝓛 X β†’ X) , (s ∘ Ξ· ∼ id) Γ— (s ∘ ΞΌ ∼ s ∘ 𝓛̇ s)

free-𝓛-algebra : is-univalent 𝓣 β†’ (X : 𝓀 Μ‡ ) β†’ 𝓛-algebra (𝓛 X)
free-𝓛-algebra ua X = ΞΌ , 𝓛-unit-left∼ ua , 𝓛-assoc∼ ua

\end{code}

We can describe algebras in terms of "extension" operations subject to
two laws:

\begin{code}

extension-op : 𝓀 Μ‡ β†’ 𝓣 ⁺ βŠ” 𝓀 Μ‡
extension-op X = {P : 𝓣 Μ‡ } β†’ is-prop P β†’ (P β†’ X) β†’ X

\end{code}

The intuitive idea is that a "extension" operation extends a partial
element to a total element.

To characterize algebras, the extension operations have two satisfy the
following two laws:

\begin{code}

𝓛-alg-Lawβ‚€ : {X : 𝓀 Μ‡ } β†’ extension-op X β†’ 𝓀 Μ‡
𝓛-alg-Lawβ‚€ {𝓀} {X} ∐ = (x : X) β†’ ∐ πŸ™-is-prop (Ξ» (p : πŸ™) β†’ x) ＝ x

𝓛-alg-Law₁ : {X : 𝓀 Μ‡ } β†’ extension-op X β†’ 𝓣 ⁺ βŠ” 𝓀 Μ‡
𝓛-alg-Law₁ {𝓀} {X} ∐ =
   (P : 𝓣 Μ‡ ) (Q : P β†’ 𝓣 Μ‡ )
   (i : is-prop P) (j : (p : P) β†’ is-prop (Q p))
   (Ο† : Ξ£ Q β†’ X)
 β†’ ∐ (Ξ£-is-prop i j) Ο† ＝ ∐ i (Ξ» p β†’ ∐ (j p) (Ξ» q β†’ Ο† (p , q)))

\end{code}

Omitting the witnesses of proposition-hood, the above two laws can be
written in more standard mathematical notation as follows:

    ∐  x = x
   p:πŸ™

    ∐          Ο† r  =  ∐   ∐     Ο† (p , q)
  r : Ξ£ {P} Q         p:P q:Q(p)


\begin{code}

𝓛-alg : 𝓀 Μ‡ β†’ 𝓣 ⁺ βŠ” 𝓀 Μ‡
𝓛-alg X = Ξ£ ∐ κž‰ extension-op X , 𝓛-alg-Lawβ‚€ ∐ Γ— 𝓛-alg-Law₁ ∐

\end{code}

Before proving that we have an equivalence

  𝓛-algebra X ≃ 𝓛-alg X,

we characterize the algebra morphisms in terms of extensions (unfortunately
overloading is not available):

\begin{code}

private
 ⋁ : {X : 𝓀 Μ‡ } β†’ (𝓛 X β†’ X) β†’ extension-op X
 ⋁ s {P} i Ο† = s (P , Ο† , i)

 βˆΜ‡ : {X : 𝓀 Μ‡ } β†’ 𝓛-algebra X β†’ extension-op X
 βˆΜ‡ (s , _) = ⋁ s

 ∐ : {X : 𝓀 Μ‡ } β†’ 𝓛-alg X β†’ extension-op X
 ∐ (∐ , κ , ι) = ∐

 lawβ‚€ : {X : 𝓀 Μ‡ } (a : 𝓛-alg X) β†’ 𝓛-alg-Lawβ‚€ (∐ a)
 lawβ‚€ (∐ , ΞΊ , ΞΉ) = ΞΊ

 law₁ : {X : 𝓀 Μ‡ } (a : 𝓛-alg X) β†’ 𝓛-alg-Law₁ (∐ a)
 law₁ (∐ , ΞΊ , ΞΉ) = ΞΉ

\end{code}

The algebra morphisms are the maps that preserve extensions. Omitting the
first argument of ⋁, the following says that the morphisms are the
maps h : X β†’ Y with

  h (⋁ Ο†) ＝ ⋁ h (Ο† p)
            p:P

for all Ο† : P β†’ X.

\begin{code}

𝓛-morphism-charac : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                    (s : 𝓛 X β†’ X) (t : 𝓛 Y β†’ Y)
                    (h : X β†’ Y)
                  β†’ (h ∘ s ∼ t ∘ 𝓛̇ h)
                  ≃ ({P : 𝓣 Μ‡ } (i : is-prop P) (Ο† : P β†’ X)
                       β†’ h (⋁ s i Ο†) ＝ ⋁ t i (Ξ» p β†’ h (Ο† p)))
𝓛-morphism-charac s t h = qinveq (Ξ» H {P} i Ο† β†’ H (P , Ο† , i))
                                 ((Ξ» {Ο€ (P , Ο† , i) β†’ Ο€ {P} i Ο†}) ,
                                 (Ξ» _ β†’ refl) ,
                                 (Ξ» _ β†’ refl))

\end{code}

We name the other two projections of 𝓛-alg:

\begin{code}

𝓛-alg-const : {X : 𝓀 Μ‡ } (A : 𝓛-alg X) (x : X)
            β†’ ∐ A πŸ™-is-prop (Ξ» (p : πŸ™) β†’ x) ＝ x
𝓛-alg-const (∐ , ΞΊ , ΞΉ) = ΞΊ

𝓛-alg-iterated : {X : 𝓀 Μ‡ } (A : 𝓛-alg X)
                 (P : 𝓣 Μ‡ ) (Q : P β†’ 𝓣 Μ‡ )
                 (i : is-prop P) (j : (p : P) β†’ is-prop (Q p))
                 (Ο† : Ξ£ Q β†’ X)
               β†’ ∐ A (Ξ£-is-prop i j) Ο†
               ＝ ∐ A i (Ξ» p β†’ ∐ A (j p) (Ξ» q β†’ Ο† (p , q)))
𝓛-alg-iterated (∐ , ΞΊ , ΞΉ) = ΞΉ

\end{code}

We could write a proof of the following characterization of the
𝓛-algebras by composing equivalences as above, but it seems more
direct, and just as clear, to write a direct proof, by construction of
the equivalence and its inverse. This also emphasizes that the
equivalence is definitional, in the sense that the two required
equations hold definitionally.

\begin{code}

𝓛-algebra-gives-alg : {X : 𝓀 Μ‡ } β†’ 𝓛-algebra X β†’ 𝓛-alg X
𝓛-algebra-gives-alg (s , unit , assoc) =
  ⋁ s ,
  unit ,
  (Ξ» P Q i j Ο† β†’ assoc (P , (Ξ» p β†’ Q p , (Ξ» q β†’ Ο† (p , q)) , j p) , i))

𝓛-alg-gives-algebra : {X : 𝓀 Μ‡ } β†’ 𝓛-alg X β†’ 𝓛-algebra X
𝓛-alg-gives-algebra {𝓀} {X} (∐ , unit , ΞΉ) = s , unit , assoc
 where
  s : 𝓛 X β†’ X
  s (P , Ο† , i) = ∐ i Ο†

  assoc : s ∘ ΞΌ ∼ s ∘ 𝓛̇ s
  assoc (P , g , i) = ΞΉ P (pr₁ ∘ g) i
                       (Ξ» p β†’ prβ‚‚ (prβ‚‚ (g p)))
                       (Ξ» r β†’ pr₁ (prβ‚‚ (g (pr₁ r))) (prβ‚‚ r))

𝓛-alg-charac : {X : 𝓀 Μ‡ } β†’ 𝓛-algebra X ≃ 𝓛-alg X
𝓛-alg-charac = qinveq
                𝓛-algebra-gives-alg
                (𝓛-alg-gives-algebra , ((Ξ» _ β†’ refl) , (Ξ» _ β†’ refl)))
\end{code}

We now consider an equivalent of 𝓛-alg-Lawβ‚€ (which is useful e.g. for
type injectivity purposes).

\begin{code}

𝓛-alg-Lawβ‚€' : {X : 𝓀 Μ‡ } β†’ extension-op X β†’ 𝓣 ⁺ βŠ” 𝓀 Μ‡
𝓛-alg-Lawβ‚€' {𝓀} {X} ∐ = (P : 𝓣 Μ‡ )
                         (i : is-prop P)
                         (Ο† : P β†’ X)
                         (p : P)
                       β†’ ∐ i Ο† ＝ Ο† p

𝓛-alg-Lawβ‚€-givesβ‚€' : propext 𝓣
                   β†’ funext 𝓣 𝓣
                   β†’ funext 𝓣 𝓀
                   β†’ {X : 𝓀 Μ‡ }
                     (∐ : extension-op X)
                   β†’ 𝓛-alg-Lawβ‚€ ∐
                   β†’ 𝓛-alg-Lawβ‚€' ∐
𝓛-alg-Lawβ‚€-givesβ‚€' pe fe fe' {X} ∐ ΞΊ P i Ο† p = Ξ³
 where
  r : Ο† ＝ Ξ» (_ : P) β†’ Ο† p
  r = dfunext fe' (Ξ» p' β†’ ap Ο† (i p' p))

  s : P ＝ πŸ™ β†’ ∐ {P} i Ο† ＝ ∐ {πŸ™} πŸ™-is-prop (Ξ» (_ : πŸ™) β†’ Ο† p)
  s refl = apβ‚‚ ∐ (being-prop-is-prop fe i πŸ™-is-prop) r

  t : P ＝ πŸ™
  t = pe i πŸ™-is-prop unique-to-πŸ™ (Ξ» _ β†’ p)

  Ξ³ = ∐ {P} i Ο†                   ＝⟨ s t ⟩
      ∐ πŸ™-is-prop (Ο† ∘ (Ξ» _ β†’ p)) ＝⟨ ΞΊ (Ο† p) ⟩
      Ο† p                         ∎

𝓛-alg-Lawβ‚€'-givesβ‚€ : {X : 𝓀 Μ‡ }
                     (∐ : extension-op X)
                    β†’ 𝓛-alg-Lawβ‚€' ∐
                    β†’ 𝓛-alg-Lawβ‚€ ∐
𝓛-alg-Lawβ‚€'-givesβ‚€ {𝓀} {X} ∐ Ο† x = Ο† πŸ™ πŸ™-is-prop (Ξ» _ β†’ x) ⋆

\end{code}

We now consider a non-dependent version of 𝓛-alg-Law₁, and show that it is
equivalent to 𝓛-alg-Law₁:

\begin{code}

𝓛-alg-Law₁' : {X : 𝓀 Μ‡ } β†’ extension-op X β†’ 𝓣 ⁺ βŠ” 𝓀 Μ‡
𝓛-alg-Law₁' {𝓀} {X} ∐ = (P Q : 𝓣 Μ‡ )
                         (i : is-prop P) (j : is-prop Q)
                         (Ο† : P Γ— Q β†’ X)
                       β†’ ∐ (Γ—-is-prop i j) Ο† ＝ ∐ i (Ξ» p β†’ ∐ j (Ξ» q β†’ Ο† (p , q)))

\end{code}

The difference with 𝓛-alg-Law₁ is that the family Ο† has type P Γ— Q β†’ X
rather than Ξ£ {P} Q β†’ X, and so the modified, logically equivalent law
amounts to

    ∐   ∐   Ο† (p , q) =   ∐        Ο† r
   p:P q:Q              r : P Γ— Q

One direction of the logical equivalence is trivial:

\begin{code}

𝓛-alg-Law₁-gives₁' : {X : 𝓀 Μ‡ } (∐ : extension-op X)
                   β†’ 𝓛-alg-Law₁ ∐ β†’ 𝓛-alg-Law₁' ∐
𝓛-alg-Law₁-gives₁' {𝓀} {X} ∐ a P Q i j = a P (Ξ» _ β†’ Q) i (Ξ» p β†’ j)

\end{code}

To establish the converse we need the following lemma for extensions,
which is interesting on its own right,

  ∐  Ο† p ＝ ∐  Ο† (k q),
 p:P      q:Q

and also gives self-distributivity of extensions:

  ∐   ∐  Ο† (p , q) =   ∐   ∐  Ο† (p , q)
 p:P q:Q              q:Q p:P


\begin{code}

change-of-variables-in-extension
 : {X : 𝓀 Μ‡ } (∐ : extension-op X)
   (P : 𝓣 Μ‡ ) (i : is-prop P)
   (Q : 𝓣 Μ‡ ) (j : is-prop Q)
   (h : P β†’ Q) (k : Q β†’ P)
   (Ο† : P β†’ X)
 β†’ is-univalent 𝓣
 β†’ ∐ i Ο† ＝ ∐ j (Ο† ∘ k)
change-of-variables-in-extension ∐ P i Q j h k Ο† ua
 = Ξ³
 where
  cd : (r : Q ＝ P) β†’ ∐ i Ο† ＝ ∐ j (Ο† ∘ Idtofun r)
  cd refl = ap (Ξ» - β†’ ∐ - Ο†) (being-prop-is-prop (univalence-gives-funext ua) i j)

  e : Q ≃ P
  e = qinveq k (h , ((Ξ» q β†’ j (h (k q)) q) , Ξ» p β†’ i (k (h p)) p))

  a : Idtofun (eqtoid ua Q P e) ＝ k
  a = ap ⌜_⌝ (idtoeq'-eqtoid ua Q P e)

  Ξ³ : ∐ i Ο† ＝ ∐ j (Ο† ∘ k)
  Ξ³ = cd (eqtoid ua Q P e) βˆ™ ap (Ξ» - β†’ ∐ j (Ο† ∘ -)) a

\end{code}

NB. The above is proved without univalence, but with propositional and
functional extensionality in the module InjectiveTypes.Structure.

\begin{code}

𝓛-alg-self-distr : {X : 𝓀 Μ‡ } (∐ : extension-op X)
                   (P : 𝓣 Μ‡ ) (i : is-prop P)
                   (Q : 𝓣 Μ‡ ) (j : is-prop Q)
                 β†’ is-univalent 𝓣
                 β†’ 𝓛-alg-Law₁' ∐
                 β†’ (Ο† : P Γ— Q β†’ X)
                      β†’ ∐ i (Ξ» p β†’ ∐ j (Ξ» q β†’ Ο† (p , q)))
                      ＝ ∐ j (Ξ» q β†’ ∐ i (Ξ» p β†’ Ο† (p , q)))

𝓛-alg-self-distr ∐ P i Q j ua l₁' Ο† =
 ∐ i (Ξ» p β†’ ∐ j (Ξ» q β†’ Ο† (p , q)))                     ＝⟨ a ⟩
 ∐ (Ξ£-is-prop i (Ξ» p β†’ j)) Ο†                           ＝⟨ b ⟩
 ∐ (Ξ£-is-prop j (Ξ» p β†’ i)) (Ο† ∘ (Ξ» t β†’ prβ‚‚ t , pr₁ t)) ＝⟨ c ⟩
 ∐ j (Ξ» q β†’ ∐ i (Ξ» p β†’ Ο† (p , q)))                     ∎
  where
   a = (l₁' P Q i j Ο†)⁻¹
   b = change-of-variables-in-extension
        ∐
        (P Γ— Q)
        (Ξ£-is-prop i (Ξ» p β†’ j))
        (Q Γ— P)
        (Ξ£-is-prop j (Ξ» p β†’ i))
        (Ξ» t β†’ prβ‚‚ t , pr₁ t) (Ξ» t β†’ prβ‚‚ t , pr₁ t) Ο† ua
   c = l₁' Q P j i (Ξ» t β†’ Ο† (prβ‚‚ t , pr₁ t))

\end{code}

Using this we can prove the other direction of the logical equivalence
claimed above:

\begin{code}

𝓛-alg-Law₁'-gives₁ : {X : 𝓀 Μ‡ } (∐ : extension-op X)
                    β†’ is-univalent 𝓣
                    β†’ funext 𝓣 𝓀
                    β†’ 𝓛-alg-Law₁' ∐
                    β†’ 𝓛-alg-Law₁ ∐
𝓛-alg-Law₁'-gives₁ {𝓀} {X} ∐ ua fe a P Q i j Ο† = Ξ³
 where
  h : (p : P) β†’ Q p β†’ Ξ£ Q
  h p q = (p , q)

  k : (p : P) β†’ Ξ£ Q β†’ Q p
  k p (p' , q) = transport Q (i p' p) q

  Ο†' : P Γ— Ξ£ Q β†’ X
  Ο†' (p , p' , q) = Ο† (p , k p (p' , q))

  k' : Ξ£ Q β†’ P Γ— Ξ£ Q
  k' (p , q) = p , p , q

  H : Ο†' ∘ k' ∼ Ο†
  H (p , q) = ap (Ξ» - β†’ Ο† (p , -)) (j p _ _)

  Ξ³ = ∐ {Ξ£ Q} (Ξ£-is-prop i j) Ο†                                         ＝⟨ b ⟩
      ∐ {Ξ£ Q} (Ξ£-is-prop i j) (Ο†' ∘ k')                                 ＝⟨ c ⁻¹ ⟩
      ∐ {P Γ— Ξ£ Q} (Γ—-is-prop i (Ξ£-is-prop i j)) Ο†'                      ＝⟨ d ⟩
      ∐ {P} i (Ξ» p β†’ ∐ {Ξ£ Q} (Ξ£-is-prop i j) ((Ξ» Οƒ β†’ Ο† (p , Οƒ)) ∘ k p)) ＝⟨ e ⟩
      ∐ {P} i (Ξ» p β†’ ∐ {Q p} (j p) (Ξ» q β†’ Ο† (p , q)))                   ∎
   where
    b = (ap (∐ {Σ Q} (Σ-is-prop i j)) (dfunext fe H))⁻¹
    c = change-of-variables-in-extension
         ∐
         (P Γ— Ξ£ Q)
         (Γ—-is-prop i (Ξ£-is-prop i j))
         (Ξ£ Q)
         (Ξ£-is-prop i j) prβ‚‚ k' Ο†' ua
    d = a P (Ξ£ Q) i (Ξ£-is-prop i j) (Ξ» z β†’ Ο† (pr₁ z , k (pr₁ z) (prβ‚‚ z)))
    e = (ap (∐ {P} i)
          (dfunext fe (Ξ» p β†’ change-of-variables-in-extension
                              ∐
                              (Q p)
                              (j p)
                              (Ξ£ Q) (Ξ£-is-prop i j)
                              (h p) (k p) (Ξ» Οƒ β†’ Ο† (p , Οƒ)) ua)))⁻¹
\end{code}

The algebras form an exponential ideal with the pointwise
operations. More generally:

\begin{code}

Ξ -is-alg : funext 𝓀 π“₯
         β†’ {X : 𝓀 Μ‡ } (A : X β†’ π“₯ Μ‡ )
         β†’ ((x : X) β†’ 𝓛-alg (A x)) β†’ 𝓛-alg (Ξ  A)
Ξ -is-alg {𝓀} {π“₯} fe {X} A Ξ± = ∐· , lβ‚€ , l₁
 where
  ∐· : {P : 𝓣 Μ‡ } β†’ is-prop P β†’ (P β†’ Ξ  A) β†’ Ξ  A
  ∐· i Ο† x = ∐ (Ξ± x) i (Ξ» p β†’ Ο† p x)

  lβ‚€ : (Ο† : Ξ  A) β†’ ∐· πŸ™-is-prop (Ξ» p β†’ Ο†) ＝ Ο†
  lβ‚€ Ο† = dfunext fe (Ξ» x β†’ lawβ‚€ (Ξ± x) (Ο† x))

  l₁ : (P : 𝓣 Μ‡ ) (Q : P β†’ 𝓣 Μ‡ )
       (i : is-prop P) (j : (p : P) β†’ is-prop (Q p))
       (Ο† : Ξ£ Q β†’ Ξ  A)
      β†’ ∐· (Ξ£-is-prop i j) Ο†
      ＝ ∐· i (Ξ» p β†’ ∐· (j p) (Ξ» q β†’ Ο† (p , q)))
  l₁ P Q i j Ο† = dfunext fe (Ξ» x β†’ law₁ (Ξ± x) P Q i j (Ξ» Οƒ β†’ Ο† Οƒ x))

\end{code}

This is the case for any monad of a certain kind, but the way we
proved this above using our characterizations of the algebras applies
only to our monad.

The following examples are crucial for injectivity. They say that the
universe is an algebra in at least two ways, with ∐ = Σ and ∐ = Π
respectively.

\begin{code}

universe-is-algebra-Ξ£ : is-univalent 𝓣 β†’ 𝓛-alg (𝓣 Μ‡ )
universe-is-algebra-Ξ£ ua = sum , k , ΞΉ
 where
  sum : {P : 𝓣 Μ‡ } β†’ is-prop P β†’ (P β†’ 𝓣 Μ‡ ) β†’ 𝓣 Μ‡
  sum {P} i = Ξ£

  k : (X : 𝓣 Μ‡ ) β†’ Ξ£ (Ξ» p β†’ X) ＝ X
  k X = eqtoid ua (πŸ™ Γ— X) X πŸ™-lneutral

  ΞΉ : (P : 𝓣 Μ‡ ) (Q : P β†’ 𝓣 Μ‡ ) (i : is-prop P)
      (j : (p : P) β†’ is-prop (Q p)) (Ο† : Ξ£ Q β†’ 𝓣 Μ‡ )
    β†’ Ξ£ Ο† ＝ Ξ£ (Ξ» p β†’ Ξ£ (Ξ» q β†’ Ο† (p , q)))
  ΞΉ P Q i j Ο† = eqtoid ua _ _ Ξ£-assoc

universe-is-algebra-Ξ  : is-univalent 𝓣 β†’ 𝓛-alg (𝓣 Μ‡ )
universe-is-algebra-Ξ  ua = prod , k , ΞΉ
 where
  fe : funext 𝓣 𝓣
  fe = univalence-gives-funext ua

  prod : {P : 𝓣 Μ‡ } β†’ is-prop P β†’ (P β†’ 𝓣 Μ‡ ) β†’ 𝓣 Μ‡
  prod {P} i = Ξ 

  k : (X : 𝓣 Μ‡ ) β†’ Ξ  (Ξ» p β†’ X) ＝ X
  k X = eqtoid ua (πŸ™ β†’ X) X (≃-sym (πŸ™β†’ (univalence-gives-funext ua)))

  ΞΉ : (P : 𝓣 Μ‡ ) (Q : P β†’ 𝓣 Μ‡ ) (i : is-prop P)
      (j : (p : P) β†’ is-prop (Q p)) (Ο† : Ξ£ Q β†’ 𝓣 Μ‡ )
    β†’ Ξ  Ο† ＝ Ξ  (Ξ» p β†’ Ξ  (Ξ» q β†’ Ο† (p , q)))
  ΞΉ P Q i j Ο† = eqtoid ua _ _ (curry-uncurry' fe fe)

\end{code}

Added 6th June 2025. A retract of the underlying type of an algebra
can be given an algebra structure, if the induced idempotent is an
automorphism, in such a way that the section becomes a homomorphism.

\begin{code}

is-hom : {A : 𝓀 Μ‡ } {B : π“₯ Μ‡ } β†’ 𝓛-alg A β†’ 𝓛-alg B β†’ (A β†’ B) β†’ 𝓣 ⁺ βŠ” 𝓀 βŠ” π“₯ Μ‡
is-hom {𝓀} {π“₯} {A} {B} (βˆα΅ƒ , _) (βˆα΅‡ , _) h =
 (P : 𝓣 Μ‡ ) (i : is-prop P) (Ο† : P β†’ A) β†’ h (βˆα΅ƒ i Ο†) ＝ βˆα΅‡ i (h ∘ Ο†)

id-is-hom : {A : 𝓀 Μ‡ } (𝓐 : 𝓛-alg A)
          β†’ is-hom 𝓐 𝓐 id
id-is-hom 𝓐 P i Ο† = refl

∘-is-hom : {A : 𝓀 Μ‡ } {B : π“₯ Μ‡ } {C : 𝓦 Μ‡ }
           (𝓐 : 𝓛-alg A) (𝓑 : 𝓛-alg B) (𝓒 : 𝓛-alg C)
           (h : A β†’ B) (k : B β†’ C)
         β†’ is-hom 𝓐 𝓑 h
         β†’ is-hom 𝓑 𝓒 k
         β†’ is-hom 𝓐 𝓒 (k ∘ h)
∘-is-hom (βˆα΅ƒ , _) (βˆα΅‡ , _) (∐ᢜ , _) h k h-is-hom k-is-hom P i Ο† =
 k (h (βˆα΅ƒ i Ο†))   ＝⟨ ap k (h-is-hom P i Ο†) ⟩
 k (βˆα΅‡ i (h ∘ Ο†)) ＝⟨ k-is-hom P i (h ∘ Ο†) ⟩
 ∐ᢜ i (k ∘ h ∘ Ο†) ∎

open import UF.Sets

being-hom-is-prop : Fun-Ext
                  β†’ {A : 𝓀 Μ‡ } (𝓐 : 𝓛-alg A)
                    {B : π“₯ Μ‡ } (𝓑 : 𝓛-alg B)
                  β†’ is-set B
                  β†’ (h : A β†’ B)
                  β†’ is-prop (is-hom 𝓐 𝓑 h)
being-hom-is-prop fe 𝓐 𝓑 B-is-set h = Π₃-is-prop fe (Ξ» _ _ _ β†’ B-is-set)

⟨_⟩ : {A : 𝓀 Μ‡ } β†’ 𝓛-alg A β†’ 𝓀 Μ‡
⟨_⟩ {𝓀} {A} 𝓐 = A

Hom : {A : 𝓀 Μ‡ } {B : π“₯ Μ‡ } β†’ 𝓛-alg A β†’ 𝓛-alg B β†’ 𝓣 ⁺ βŠ” 𝓀 βŠ” π“₯ Μ‡
Hom 𝓐 𝓑 = Ξ£ h κž‰ (⟨ 𝓐 ⟩ β†’  ⟨ 𝓑 ⟩) , is-hom 𝓐 𝓑 h

open import UF.Retracts

module _
         (A : 𝓀 Μ‡ )
         (B : π“₯ Μ‡ )
         (𝓐@(βˆα΅ƒ , lawᡃ₀ , lawᡃ₁) : 𝓛-alg A)
         ((r , s , rs) : retract B of A)
         (sr-is-hom : is-hom 𝓐 𝓐 (s ∘ r))
         (fe : Fun-Ext)
       where

 private
  βˆα΅‡ : extension-op B
  βˆα΅‡ i Ο† = r (βˆα΅ƒ i (s ∘ Ο†))

  lawᡇ₀ : 𝓛-alg-Lawβ‚€ βˆα΅‡
  lawᡇ₀ b =
   βˆα΅‡ πŸ™-is-prop (Ξ» _ β†’ b)       ＝⟨refl⟩
   r (βˆα΅ƒ πŸ™-is-prop (Ξ» _ β†’ s b)) ＝⟨ ap r (lawᡃ₀ (s b)) ⟩
   r (s b)                      ＝⟨ rs b ⟩
   b                            ∎

\end{code}

Before we know that βˆα΅‡ satisfies the second algebra law, we can show
that the section is a homomorphism. In fact, we use this to prove the
second algebra law.

\begin{code}

  s-is-hom = Ξ» P i Ο† β†’
   s (βˆα΅‡ i Ο†)           ＝⟨refl⟩
   s (r (βˆα΅ƒ i (s ∘ Ο†))) ＝⟨ sr-is-hom P i (s ∘ Ο†) ⟩
   βˆα΅ƒ i (s ∘ r ∘ s ∘ Ο†) ＝⟨ ap (Ξ» - β†’ βˆα΅ƒ i (s ∘ - ∘ Ο†)) (dfunext fe rs) ⟩
   βˆα΅ƒ i (s ∘ Ο†)         ∎

  lawᡇ₁ : 𝓛-alg-Law₁ βˆα΅‡
  lawᡇ₁ P Q i j Ο† =
   βˆα΅‡ (Ξ£-is-prop i j) Ο†                                    ＝⟨refl⟩
   r (βˆα΅ƒ (Ξ£-is-prop i j) (s ∘ Ο†))                          ＝⟨ by-lawᡃ₁ ⟩
   r (βˆα΅ƒ i (Ξ» p β†’ βˆα΅ƒ (j p) (Ξ» q β†’ s (Ο† (p , q)))))         ＝⟨ because-s-is-hom ⟩
   r (βˆα΅ƒ i (Ξ» p β†’ s (r (βˆα΅ƒ (j p) (Ξ» q β†’ s (Ο† (p , q))))))) ＝⟨refl⟩
   βˆα΅‡ i (Ξ» p β†’ βˆα΅‡ (j p) (Ξ» q β†’ Ο† (p , q)))                 ∎
    where
     by-lawᡃ₁ = ap r (lawᡃ₁ P Q i j (s ∘ Ο†))
     because-s-is-hom =
      ap (r ∘ βˆα΅ƒ i)
         ((dfunext fe (Ξ» p β†’ s-is-hom (Q p) (j p) (Ξ» q β†’ Ο† (p , q))))⁻¹)

  𝓑 : 𝓛-alg B
  𝓑 = βˆα΅‡ , lawᡇ₀ , lawᡇ₁

\end{code}

The following are the only public things in this anonymous module.

\begin{code}

 retract-of-algebra : 𝓛-alg B
 retract-of-algebra = 𝓑

 section-is-hom : is-hom retract-of-algebra 𝓐 s
 section-is-hom = s-is-hom

\end{code}

Added 6th September 2025 by Martin Escardo. Use Ξ© to repackage things
more neatly. We use uppercase names to distinguish the repackaged
things.

\begin{code}

module algebra-repackaging where

 open import UF.SubtypeClassifier

 Extension-op : 𝓀 Μ‡ β†’ 𝓣 ⁺ βŠ” 𝓀 Μ‡
 Extension-op X = (P : Ξ© 𝓣) β†’ (P holds β†’ X) β†’ X

 𝓛-Alg-Lawβ‚€ : {X : 𝓀 Μ‡ } β†’ Extension-op X β†’ 𝓀 Μ‡
 𝓛-Alg-Lawβ‚€ {𝓀} {X} ∐ = (x : X) β†’ ∐ ⊀ (Ξ» _ β†’ x) ＝ x

 𝓛-Alg-Law₁ : {X : 𝓀 Μ‡ } β†’ Extension-op X β†’ 𝓣 ⁺ βŠ” 𝓀 Μ‡
 𝓛-Alg-Law₁ {𝓀} {X} ∐ =
    (P : Ξ© 𝓣) (Q : P holds β†’ Ξ© 𝓣)
    (Ο† : (ΣΩ p κž‰ P , Q p) holds β†’ X)
  β†’ ∐ (ΣΩ p κž‰ P , Q p) Ο† ＝ ∐ P (Ξ» p β†’ ∐ (Q p) (Ξ» q β†’ Ο† (p , q)))

 𝓛-Alg : 𝓀 Μ‡ β†’ 𝓣 ⁺ βŠ” 𝓀 Μ‡
 𝓛-Alg X = Ξ£ ∐ κž‰ Extension-op X , 𝓛-Alg-Lawβ‚€ ∐ Γ— 𝓛-Alg-Law₁ ∐

 𝓛-Alg-gives-𝓛-alg : {X : 𝓀 Μ‡ } β†’ 𝓛-Alg X β†’ 𝓛-alg X
 𝓛-Alg-gives-𝓛-alg (∐ , lβ‚€ , l₁) =
  (Ξ» {P} P-is-prop β†’ ∐ (P , P-is-prop)) ,
  lβ‚€ ,
  (Ξ» P Q i j β†’ l₁ (P , i) (Ξ» p β†’ Q p , j p))

\end{code}

But we probably won't use the above repackaging, as we already have
everything written with the original choice of implementation.

Added 8th September 2025 by Martin Escardo. The discussion of free
algebras in the category of sets can be carried out without using
univalence, and only its two consequences, propositional and
functional extensionality. Notice that already the associativity law
for the lifting monad uses univalence.

\begin{code}

is-free-𝓛-alg : {F : 𝓀 Μ‡ } (𝓕 : 𝓛-alg F) (X : π“₯ Μ‡ ) (ΞΉ : X β†’ F) β†’ 𝓀ω
is-free-𝓛-alg 𝓕 X ΞΉ = {𝓦 : Universe}
                       {A : 𝓦 Μ‡ }
                       (i : is-set A)
                       (𝓐 : 𝓛-alg A)
                       (f : X β†’ A)
                     β†’ βˆƒ! (fΜ… , _) κž‰ Hom 𝓕 𝓐 , fΜ… ∘ ΞΉ ∼ f

\end{code}

Notice that above definition says that precomposition with ΞΉ is an
equivalence.

\begin{code}

module free-algebra-eliminators
         {F : 𝓀 Μ‡ }
         (𝓕 : 𝓛-alg F)
         (X : π“₯ Μ‡ )
         (ΞΉ : X β†’ F)
         (𝓕-is-free : is-free-𝓛-alg 𝓕 X ΞΉ)
         {A : 𝓦 Μ‡ }
         (i : is-set A)
         (𝓐 : 𝓛-alg A)
         (f : X β†’ A)
       where

 private
  eu : βˆƒ! (fΜ… , _) κž‰ Hom 𝓕 𝓐 , fΜ… ∘ ΞΉ ∼ f
  eu = 𝓕-is-free i 𝓐 f

 unique-hom : F β†’ A
 unique-hom = pr₁ (βˆƒ!-witness eu)

 unique-hom-is-hom : is-hom 𝓕 𝓐 unique-hom
 unique-hom-is-hom = prβ‚‚ (βˆƒ!-witness eu)

 unique-hom-is-extension : unique-hom ∘ ι ∼ f
 unique-hom-is-extension = βˆƒ!-is-witness eu

 at-most-one-extending-hom : is-prop (Ξ£ (fΜ… , _) κž‰ Hom 𝓕 𝓐 , fΜ… ∘ ΞΉ ∼ f)
 at-most-one-extending-hom = singletons-are-props eu

 at-most-one-extending-hom' : ((h , h-is-hom) (k , k-is-hom) : Hom 𝓕 𝓐)
                            β†’ h ∘ ΞΉ ∼ f
                            β†’ k ∘ ΞΉ ∼ f
                            β†’ h ∼ k
 at-most-one-extending-hom' 𝕙@(h , h-is-hom) π•œ@(k , k-is-hom) p q =
  happly (ap (pr₁ ∘ pr₁) (at-most-one-extending-hom (𝕙 , p) (π•œ , q)))

 the-only-hom-extension : ((h , h-is-hom) : Hom 𝓕 𝓐)
                        β†’ h ∘ ΞΉ ∼ f
                        β†’ h ∼ unique-hom
 the-only-hom-extension 𝕙@(h , h-is-hom) x =
  at-most-one-extending-hom' 𝕙 (βˆƒ!-witness eu) x unique-hom-is-extension

\end{code}

We now construct the canonical free algebra.

\begin{code}

module free-algebras-in-the-category-of-sets
        (pe : Prop-Ext)
        (fe : Fun-Ext)
        {𝓀 : Universe}
        (X : 𝓀 Μ‡ )
        (X-is-set : is-set X)
       where

 ⨆ : extension-op (𝓛 X)
 ⨆ {P} P-is-prop Ο† =
  (Ξ£ p κž‰ P , is-defined (Ο† p)) ,
  (Ξ» (p , d) β†’ value (Ο† p) d) ,
  Ξ£-is-prop P-is-prop (Ξ» p β†’ being-defined-is-prop (Ο† p))

 free : 𝓛-alg (𝓛 X)
 free = ⨆ , lβ‚€ , l₁
  where
   lβ‚€ : 𝓛-alg-Lawβ‚€ ⨆
   lβ‚€ l@(P , Ο† , P-is-prop) =
     from-⋍ pe fe fe (((Ξ» (⋆ , p) β†’ p) , (Ξ» p β†’ ⋆ , p)) , (Ξ» _ β†’ refl))

   l₁ : 𝓛-alg-Law₁ ⨆
   l₁ P Q i j f = from-⋍ pe fe fe
                   (((Ξ» ((p , q) , d) β†’ (p , (q , d))) ,
                     Ξ» (p , (q , d)) β†’ ((p , q), d)) ,
                    (Ξ» _ β†’ refl))

\end{code}

We rely on the following useful lemma, which says that every element
of 𝓛 X is a join of positive elements, as in the case after Anders
Kock (see [1] below), and which is interesting in its own right. The
positive elements of the free algebra 𝓛 X are those of the form Ξ· x,
but we don't need to know this or the definition of positive element
in order to formulate and prove the following.

\begin{code}

 every-element-of-𝓛-is-a-positive-join : (l@(P , Ο† , i) : 𝓛 X)
                                       β†’ l ＝ ⨆ i (Ξ· ∘ Ο†)
 every-element-of-𝓛-is-a-positive-join l@(P , Ο† , i) =
  from-⋍ pe fe fe (((Ξ» (p : P) β†’ p , ⋆) , pr₁) , (Ξ» (_ : P) β†’ refl))

 private
  𝓕 = free

 module _
          {π“₯ : Universe}
          {A : π“₯ Μ‡ }
          (A-is-set : is-set A)
          (𝓐@(∐ , lβ‚€ , l₁) : 𝓛-alg A)
          (f : X β†’ A)
        where

  𝓛-extension : (𝓛 X β†’ A)
  𝓛-extension (P , Ο† , P-is-prop) = ∐ P-is-prop (f ∘ Ο†)

  private
   fΜ… = 𝓛-extension

  𝓛-extension-is-hom : is-hom 𝓕 𝓐 fΜ…
  𝓛-extension-is-hom P i Ο† =
   l₁ P
      (Ξ» p β†’ is-defined (Ο† p))
      i
      (Ξ» p β†’ being-defined-is-prop (Ο† p))
      (Ξ» (p , d) β†’ f (value (Ο† p) d))

  𝓛-extension-extends : fΜ… ∘ Ξ· ∼ f
  𝓛-extension-extends x = lβ‚€ (f x)

  private
   H : 𝓣 ⁺ βŠ” 𝓀 βŠ” π“₯ Μ‡
   H = Ξ£ (h , _) κž‰ Hom 𝓕 𝓐 , h ∘ Ξ· ∼ f

  hom-agreement
   : (((h , _) , _) ((h' , _) , _) : H)
   β†’ h ∼ h'
  hom-agreement
   ((h , h-is-hom) , e) ((h' , h'-is-hom) , e') l@(P , Ο† , i)
   = h l               ＝⟨ I ⟩
     h (⨆ i (Ξ· ∘ Ο†))   ＝⟨ II ⟩
     ∐ i (h  ∘ Ξ· ∘ Ο†)  ＝⟨ III ⟩
     ∐ i (h' ∘ Ξ· ∘ Ο†)  ＝⟨ II' ⟩
     h' (⨆ i (Ξ· ∘ Ο†))  ＝⟨ I' ⟩
     h' l              ∎
    where
      I   = ap h (every-element-of-𝓛-is-a-positive-join l)
      II  = h-is-hom P i (Ξ· ∘ Ο†)
      III = ap (Ξ» - β†’ ∐ i (- ∘ Ο†))
               (dfunext fe (Ξ» (x : X) β†’ h (Ξ· x)  ＝⟨ e x ⟩
                                        f x      ＝⟨ (e' x)⁻¹ ⟩
                                        h' (η x) ∎))
      II' = (h'-is-hom P i (Ξ· ∘ Ο†))⁻¹
      I'  = (ap h' (every-element-of-𝓛-is-a-positive-join l))⁻¹

  homomorphic-𝓛-extensions-form-a-prop : is-prop H
  homomorphic-𝓛-extensions-form-a-prop he he'
   = to-subtype-＝
      (Ξ» h β†’ Ξ -is-prop fe (Ξ» x β†’ A-is-set))
      (to-subtype-＝
        (being-hom-is-prop fe 𝓕 𝓐 A-is-set)
        (dfunext fe (hom-agreement he he')))

  free-algebra-universal-property : is-singleton H
  free-algebra-universal-property
   = pointed-props-are-singletons
      ((fΜ… , 𝓛-extension-is-hom) , 𝓛-extension-extends)
      homomorphic-𝓛-extensions-form-a-prop

\end{code}

Notice that the universal property of the algebra freely generated by
X : 𝓀 with insertion of generators Ξ· : X β†’ 𝓛 X eliminates into any
universe π“₯:

\begin{code}

 𝓛-is-free : is-free-𝓛-alg free X Ξ·
 𝓛-is-free = free-algebra-universal-property

\end{code}

Moved from AnAlgebraWhichIsNotAlwaysFree 29th Nov 2025. If two
algebras A and B are freely generated by the same set of generators,
they are canonically equivalent.

       i
  G ────────→ A
   β•²         β”‚ ↑
    β•²        β”‚ β”‚
     β•²       β”‚ β”‚
    j β•²    h β”‚ β”‚ h⁻¹
       β•²     β”‚ β”‚
        β•²    β”‚ β”‚
         β•²   β”‚ β”‚
          β•²  ↓ β”‚
           ➘  B

The proof is a standard categorical argument. The homomorphism h is
the unique homomorphic extension of j along i, and the homomorphism
h⁻¹ is the unique homomorphisc extension of i along j. But also the
composites h ∘ h⁻¹ : A β†’ A and h⁻¹ ∘ h : B β†’ B are the unique
homomorphisms extending the identity function along i and j
respectively, and so, because the identity functions are respectively
such a homomorphisms, we conclude that both composites agree with the
respective identity functions.

\begin{code}

module _
        {A : 𝓀 Μ‡ }
        {B : π“₯ Μ‡ }
        (G : 𝓦 Μ‡ )
        (A-is-set : is-set A)
        (B-is-set : is-set B)
        (G-is-set : is-set G)
        (i : G β†’ A)
        (j : G β†’ B)
        (Ξ± : 𝓛-alg A)
        (Ξ² : 𝓛-alg B)
        (Ο• : is-free-𝓛-alg Ξ± G i)
        (Ξ³ : is-free-𝓛-alg Ξ² G j)
     where

 module A = free-algebra-eliminators Ξ± G i Ο• B-is-set Ξ² j
 module B = free-algebra-eliminators Ξ² G j Ξ³ A-is-set Ξ± i

 private
  h : A β†’ B
  h = A.unique-hom

  h-is-hom : is-hom Ξ± Ξ² h
  h-is-hom = A.unique-hom-is-hom

  h-extends-j : h ∘ i ∼ j
  h-extends-j = A.unique-hom-is-extension

  h⁻¹ : B β†’ A
  h⁻¹ = B.unique-hom

  h⁻¹-is-hom : is-hom β α h⁻¹
  h⁻¹-is-hom = B.unique-hom-is-hom

  h⁻¹-extends-i : h⁻¹ ∘ j ∼ i
  h⁻¹-extends-i = B.unique-hom-is-extension

  I : is-hom α α (h⁻¹ ∘ h)
  I = ∘-is-hom α β α h h⁻¹ h-is-hom h⁻¹-is-hom

  II : is-hom β β (h ∘ h⁻¹)
  II = ∘-is-hom β α β 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 β†’ h⁻¹ (h (i g)) ＝⟨ ap h⁻¹ (h-extends-j g) ⟩
                h⁻¹ (j g)     ＝⟨ h⁻¹-extends-i g ⟩
                i g           ∎)
         (Ξ» (_ : G) β†’ by-definition)
   where
    open free-algebra-eliminators
          Ξ± G i Ο• A-is-set Ξ± i
  IV : h ∘ h⁻¹ ∼ id
  IV = at-most-one-extending-hom'
        (h ∘ h⁻¹ , II)
        (id , id-is-hom Ξ²)
        (Ξ» g β†’ h (h⁻¹ (j g)) ＝⟨ ap h (h⁻¹-extends-i g) ⟩
               h (i g)     ＝⟨ h-extends-j g ⟩
               j g           ∎)
        (Ξ» (_ : G) β†’ by-definition)
   where
    open free-algebra-eliminators
          Ξ² G j Ξ³ B-is-set Ξ² j

 unique-hom-is-equiv : is-equiv h
 unique-hom-is-equiv = qinvs-are-equivs h (h⁻¹ , III , IV)

\end{code}

Added 23rd Nov 2025. Anders Kock' [1] definition of positive element.

[1] Anders Kock. The constructive lift monad.
    BRICS Report Series (Aarhus), ISSN 0909-0878 (1995)
    http://tildeweb.au.dk/au76680/CLM.pdf

\begin{code}

is-positive : {A : 𝓀 Μ‡ } β†’ 𝓛-alg A β†’ A β†’ 𝓣 ⁺ βŠ” 𝓀 Μ‡
is-positive (⨆ , lβ‚€ , l₁) a =
   (P : 𝓣 Μ‡ )
   (i : is-prop P)
 β†’ ⨆ i (Ξ» (_ : P) β†’ a) ＝ a
 β†’ P

being-positive-is-prop : Fun-Ext
                       β†’ {A : 𝓀 Μ‡ }
                       β†’ (Ξ± : 𝓛-alg A) (a : A)
                       β†’ is-prop (is-positive Ξ± a)
being-positive-is-prop fe Ξ± a = Π₃-is-prop fe (Ξ» _ P-is-prop _ β†’ P-is-prop)

\end{code}