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 #-}

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 "join" operations subject to two
laws:

\begin{code}

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

\end{code}

The intuitive idea is that a "join" operation on X consists of, for
each proposition P, a map (P β†’ X) β†’ X that "puts together" the
elements of a family f : P β†’ X to get an element ∐ f of X.

Unfortunately, we won't be able to write simply ∐ f in Agda notation,
as the witness that P is a proposition can almost never be
automatically inferred and hence has to be written explicitly.

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

\begin{code}

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

𝓛-alg-Law₁ : {X : 𝓀 Μ‡ } β†’ joinop X β†’ 𝓣 ⁺ βŠ” 𝓀 Μ‡
𝓛-alg-Law₁ {𝓀} {X} ∐ =
   (P : 𝓣 Μ‡ ) (Q : P β†’ 𝓣 Μ‡ )
   (i : is-prop P) (j : (p : P) β†’ is-prop (Q p))
   (f : Ξ£ Q β†’ X)
 β†’ ∐ (Ξ£-is-prop i j) f ＝ ∐ i (Ξ» p β†’ ∐ (j p) (Ξ» q β†’ f (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:πŸ™

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


\begin{code}

𝓛-alg : 𝓀 Μ‡ β†’ 𝓣 ⁺ βŠ” 𝓀 Μ‡
𝓛-alg X = Ξ£ ∐ κž‰ joinop 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 joins (unfortunately
overloading is not available):

\begin{code}

⋁ : {X : 𝓀 Μ‡ } β†’ (𝓛 X β†’ X) β†’ joinop X
⋁ s {P} i f = s (P , f , i)

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

∐ : {X : 𝓀 Μ‡ } β†’ 𝓛-alg X β†’ joinop 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 joins. Omitting the
first argument of ⋁, the following says that the morphisms are the
maps h : X β†’ Y with

  h (⋁ f) ＝ ⋁ h (f p)
            p:P

for all f: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) (f : P β†’ X)
                       β†’ h (⋁ s i f) ＝ ⋁ t i (Ξ» p β†’ h (f p)))
𝓛-morphism-charac s t h = qinveq (Ξ» H {P} i f β†’ H (P , f , i))
                                 ((Ξ» {Ο€ (P , f , i) β†’ Ο€ {P} i f}) ,
                                 (Ξ» _ β†’ 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))
                 (f : Ξ£ Q β†’ X)
               β†’ ∐ A (Ξ£-is-prop i j) f
               ＝ ∐ A i (Ξ» p β†’ ∐ A (j p) (Ξ» q β†’ f (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 f β†’ assoc (P , (Ξ» p β†’ Q p , (Ξ» q β†’ f (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 , f , i) = ∐ i f

  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 : 𝓀 Μ‡ } β†’ joinop X β†’ 𝓣 ⁺ βŠ” 𝓀 Μ‡
𝓛-alg-Lawβ‚€' {𝓀} {X} ∐ = (P : 𝓣 Μ‡ )
                         (i : is-prop P)
                         (f : P β†’ X)
                         (p : P)
                       β†’ ∐ i f ＝ f p

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

  s : P ＝ πŸ™ β†’ ∐ {P} i f ＝ ∐ {πŸ™} πŸ™-is-prop (Ξ» (_ : πŸ™) β†’ f 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 f                   ＝⟨ s t ⟩
      ∐ πŸ™-is-prop (f ∘ (Ξ» _ β†’ p)) ＝⟨ ΞΊ (f p) ⟩
      f p                         ∎

𝓛-alg-Lawβ‚€'-givesβ‚€ : {X : 𝓀 Μ‡ }
                     (∐ : joinop 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 : 𝓀 Μ‡ } β†’ joinop X β†’ 𝓣 ⁺ βŠ” 𝓀 Μ‡
𝓛-alg-Law₁' {𝓀} {X} ∐ = (P Q : 𝓣 Μ‡ )
                         (i : is-prop P) (j : is-prop Q)
                         (f : P Γ— Q β†’ X)
                       β†’ ∐ (Γ—-is-prop i j) f ＝ ∐ i (Ξ» p β†’ ∐ j (Ξ» q β†’ f (p , q)))

\end{code}

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

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

One direction of the logical equivalence is trivial:

\begin{code}

𝓛-alg-Law₁-gives₁' : {X : 𝓀 Μ‡ } (∐ : joinop 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 joins, which
is interesting on its own right,

  ∐  f p ＝ ∐  f (k q),
 p:P      q:Q

and also gives self-distributivity of joins:

  ∐   ∐  f (p , q) =   ∐   ∐  f (p , q)
 p:P q:Q              q:Q p:P


\begin{code}

change-of-variables-in-join : {X : 𝓀 Μ‡ } (∐ : joinop X)
                              (P : 𝓣 Μ‡ ) (i : is-prop P)
                              (Q : 𝓣 Μ‡ ) (j : is-prop Q)
                              (h : P β†’ Q) (k : Q β†’ P)
                              (f : P β†’ X)
                            β†’ is-univalent 𝓣
                            β†’ ∐ i f ＝ ∐ j (f ∘ k)

change-of-variables-in-join ∐ P i Q j h k f ua = γ
 where
  cd : (r : Q ＝ P) β†’ ∐ i f ＝ ∐ j (f ∘ Idtofun r)
  cd refl = ap (Ξ» - β†’ ∐ - f) (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 f ＝ ∐ j (f ∘ k)
  Ξ³ = cd (eqtoid ua Q P e) βˆ™ ap (Ξ» - β†’ ∐ j (f ∘ -)) a

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

𝓛-alg-self-distr ∐ P i Q j ua l₁' f =
 ∐ i (Ξ» p β†’ ∐ j (Ξ» q β†’ f (p , q)))                     ＝⟨ a ⟩
 ∐ (Ξ£-is-prop i (Ξ» p β†’ j)) f                           ＝⟨ b ⟩
 ∐ (Ξ£-is-prop j (Ξ» p β†’ i)) (f ∘ (Ξ» t β†’ prβ‚‚ t , pr₁ t)) ＝⟨ c ⟩
 ∐ j (Ξ» q β†’ ∐ i (Ξ» p β†’ f (p , q)))                     ∎
  where
   a = (l₁' P Q i j f)⁻¹
   b = change-of-variables-in-join
        ∐
        (P Γ— Q)
        (Ξ£-is-prop i (Ξ» p β†’ j))
        (Q Γ— P)
        (Ξ£-is-prop j (Ξ» p β†’ i))
        (Ξ» t β†’ prβ‚‚ t , pr₁ t) (Ξ» t β†’ prβ‚‚ t , pr₁ t) f ua
   c = l₁' Q P j i (Ξ» t β†’ f (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 : 𝓀 Μ‡ } (∐ : joinop X)
                    β†’ is-univalent 𝓣
                    β†’ funext 𝓣 𝓀
                    β†’ 𝓛-alg-Law₁' ∐
                    β†’ 𝓛-alg-Law₁ ∐
𝓛-alg-Law₁'-gives₁ {𝓀} {X} ∐ ua fe a P Q i j f = Ξ³
 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

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

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

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

  γ = ∐ {Σ Q} (Σ-is-prop i j) f                                         ＝⟨ b ⟩
      ∐ {Σ Q} (Σ-is-prop i j) (f' ∘ k')                                 ＝⟨ c ⁻¹ ⟩
      ∐ {P Γ— Ξ£ Q} (Γ—-is-prop i (Ξ£-is-prop i j)) f'                      ＝⟨ d ⟩
      ∐ {P} i (Ξ» p β†’ ∐ {Ξ£ Q} (Ξ£-is-prop i j) ((Ξ» Οƒ β†’ f (p , Οƒ)) ∘ k p)) ＝⟨ e ⟩
      ∐ {P} i (Ξ» p β†’ ∐ {Q p} (j p) (Ξ» q β†’ f (p , q)))                   ∎
   where
    b = (ap (∐ {Σ Q} (Σ-is-prop i j)) (dfunext fe H))⁻¹
    c = change-of-variables-in-join
         ∐
         (P Γ— Ξ£ Q)
         (Γ—-is-prop i (Ξ£-is-prop i j))
         (Ξ£ Q)
         (Ξ£-is-prop i j) prβ‚‚ k' f' ua
    d = a P (Ξ£ Q) i (Ξ£-is-prop i j) (Ξ» z β†’ f (pr₁ z , k (pr₁ z) (prβ‚‚ z)))
    e = (ap (∐ {P} i)
          (dfunext fe (Ξ» p β†’ change-of-variables-in-join
                              ∐
                              (Q p)
                              (j p)
                              (Ξ£ Q) (Ξ£-is-prop i j)
                              (h p) (k p) (Ξ» Οƒ β†’ f (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 f x = ∐ (Ξ± x) i (Ξ» p β†’ f 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))
       (f : Ξ£ Q β†’ Ξ  A)
      β†’ ∐· (Ξ£-is-prop i j) f
      ＝ ∐· i (Ξ» p β†’ ∐· (j p) (Ξ» q β†’ f (p , q)))
  l₁ P Q i j f = dfunext fe (Ξ» x β†’ law₁ (Ξ± x) P Q i j (Ξ» Οƒ β†’ f Οƒ 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)) (f : Ξ£ Q β†’ 𝓣 Μ‡ )
    β†’ Ξ£ f ＝ Ξ£ (Ξ» p β†’ Ξ£ (Ξ» q β†’ f (p , q)))
  ΞΉ P Q i j f = 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)) (f : Ξ£ Q β†’ 𝓣 Μ‡ )
    β†’ Ξ  f ＝ Ξ  (Ξ» p β†’ Ξ  (Ξ» q β†’ f (p , q)))
  ΞΉ P Q i j f = eqtoid ua _ _ (curry-uncurry' fe fe)

\end{code}