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.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 ∘ Ο†)

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-𝓛-alg_freely-generated-by_with-insertion-of-generators_eliminating-at_
 : {F : 𝓀 Μ‡ } (𝓕 : 𝓛-alg F)
   (X : π“₯ Μ‡ )
   (ΞΉ : X β†’ F)
   (𝓦 : Universe)
 β†’ 𝓣 ⁺ βŠ” 𝓀 βŠ” π“₯ βŠ” 𝓦 ⁺ Μ‡
is-𝓛-alg 𝓕 freely-generated-by X with-insertion-of-generators ΞΉ eliminating-at 𝓦
 = {A : 𝓦 Μ‡ } (i : is-set A) (𝓐 : 𝓛-alg A) (f : X β†’ A)
      β†’ βˆƒ! (fΜ… , _) κž‰ Hom 𝓕 𝓐 , fΜ… ∘ ΞΉ ∼ f

module _ {F : 𝓀 Μ‡ } (𝓕 : 𝓛-alg F)
         (X : π“₯ Μ‡ )
         (ΞΉ : X β†’ F)
         (𝓦 : Universe)
         (𝓕-is-free : is-𝓛-alg 𝓕 freely-generated-by X
                                  with-insertion-of-generators ΞΉ
                                  eliminating-at 𝓦)
         {A : 𝓦 Μ‡ } (i : is-set A) (𝓐 : 𝓛-alg A) (f : X β†’ A)
       where

 unique-hom : F β†’ A
 unique-hom = pr₁ (βˆƒ!-witness (𝓕-is-free i 𝓐 f))

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

 unique-hom-is-extesion : unique-hom ∘ ι ∼ f
 unique-hom-is-extesion = βˆƒ!-is-witness (𝓕-is-free i 𝓐 f)


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

\end{code}

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

We now construct the canonical free algebra.

\begin{code}

 open import Lifting.UnivalentWildCategory 𝓣 X
 open import Lifting.IdentityViaSIP 𝓣

 ⨆ : 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) =
    βŠ‘-anti-lemma pe fe fe
     ((Ξ» (⋆ , p) β†’ p) , (Ξ» _ β†’ refl))
     (Ξ» p β†’ ⋆ , p)

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

 private
  𝓕 = free

 module _
          {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)

  open import UF.Equiv-FunExt

  Ξ·-fib : 𝓛 X β†’ 𝓣 Μ‡
  Ξ·-fib l = Ξ£ x κž‰ X , Ξ· x ⋍· l

  Ξ·-fib-point : (l : 𝓛 X) β†’ Ξ·-fib l β†’ X
  Ξ·-fib-point l = pr₁

  Ξ·-fib-⋍· : (l : 𝓛 X) (Ο• : Ξ·-fib l) β†’ Ξ· (Ξ·-fib-point l Ο•) ⋍· l
  Ξ·-fib-⋍· l = prβ‚‚

  Ξ·-fib-is-prop : (l : 𝓛 X) β†’ is-prop (Ξ·-fib l)
  Ξ·-fib-is-prop l@(P , Ο† , i) (x , a) (x' , a') = III
   where
    I : Ξ· x ⋍· Ξ· x'
    I = ⋍·-trans (Ξ· x) l (Ξ· x') a (⋍·-sym (Ξ· x') l a')

    II : Ξ· x ⋍· Ξ· x' β†’ x ＝ x'
    II (_ , e) = e ⋆

    III : (x , a) ＝ (x' , a')
    III = to-subtype-＝
           (Ξ» x β†’ Ξ£-is-prop
                   (equivalences-with-props-are-props fe P i πŸ™)
                   (Ξ» e β†’ Ξ -is-prop fe (Ξ» ⋆ β†’ X-is-set)))
           (II I)

  Ξ·-fib-lemma : (l@(P , Ο† , i) : 𝓛 X)
              β†’ l ＝ ⨆ (Ξ·-fib-is-prop l) (Ξ· ∘ Ξ·-fib-point l)
  Ξ·-fib-lemma (P , Ο† , i) =
   βŠ‘-anti-lemma pe fe fe
    ((Ξ» p β†’ (Ο† p ,
             logically-equivalent-props-are-equivalent
               πŸ™-is-prop
               i
               (Ξ» ⋆ β†’ p)
               (Ξ» p β†’ ⋆) ,
             (Ξ» _ β†’ refl)) ,
             ⋆) ,
     (Ξ» _ β†’ refl))
    Ξ» ((_ , e , _) , ⋆) β†’ ⌜ e ⌝ ⋆

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

  hom-agreement
   : (((h , _) , _) ((h' , _) , _) : H)
   β†’ h ∼ h'
  hom-agreement
   ((h , i) , e) ((h' , i') , e') l@(P , Ο† , P-is-prop)
   = h l                          ＝⟨ I ⟩
     h (⨆ j (Ξ· ∘ Ξ·-fib-point l))  ＝⟨ II ⟩
     ∐ j (h ∘ η ∘ η-fib-point l)  ＝⟨ III ⟩
     ∐ j (h' ∘ η ∘ η-fib-point l) ＝⟨ II' ⟩
     h' (⨆ j (Ξ· ∘ Ξ·-fib-point l)) ＝⟨ I' ⟩
     h' l                         ∎
     where
      j = Ξ·-fib-is-prop l

      I   = ap h (Ξ·-fib-lemma l)
      II  = i (η-fib l) j (η ∘ η-fib-point l)
      III = ap (Ξ» - β†’ ∐ j (- ∘ Ξ·-fib-point l)) (dfunext fe (Ξ» x β†’ e x βˆ™ e' x ⁻¹))
      II' = (i' (η-fib l) j (η ∘ η-fib-point l))⁻¹
      I'  = ap h' ((η-fib-lemma 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}

 _ : {𝓀 : Universe}
   β†’ is-𝓛-alg free freely-generated-by X
                   with-insertion-of-generators Ξ·
                   eliminating-at 𝓀
 _ = free-algebra-universal-property

\end{code}