Martin Escardo 7th November 2018.

(Strong) 'Monad' structure on 𝓛.
Again the proofs are simplified by the use of SIP.

We prove the laws for the various notions of equality because
different ones are more convenient in different situations, and
because they requires different assumptions (function extensionality
or univalence).

\begin{code}

{-# OPTIONS --without-K --exact-split --safe --auto-inline #-}

open import MLTT.Spartan

module Lifting.Monad
        (𝓣 : Universe)
       where

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

open import Lifting.Lifting 𝓣
open import Lifting.IdentityViaSIP 𝓣

\end{code}

Constructions:

\begin{code}

𝓛̇ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ 𝓛 X β†’ 𝓛 Y
𝓛̇ f (P , Ο† , i) = P , f ∘ Ο† , i

_β™― : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ 𝓛 Y) β†’ (𝓛 X β†’ 𝓛 Y)
_β™― f (P , Ο† , i) = (Ξ£ p κž‰ P , is-defined (f (Ο† p))) ,
                    (Ξ» Οƒ β†’ value (f (Ο† (pr₁ Οƒ))) (prβ‚‚ Οƒ)) ,
                    Ξ£-is-prop i (Ξ» p β†’ being-defined-is-prop (f (Ο† p)))

ΞΌ : {X : 𝓀 Μ‡ } β†’ 𝓛 (𝓛 X) β†’ 𝓛 X
ΞΌ = id β™―

\end{code}

We now give the monad laws.

Functoriality holds definitionally:

\begin{code}

𝓛̇-id : {X : 𝓀 Μ‡ }
      β†’ 𝓛̇ id ＝ id
𝓛̇-id {𝓀} {X} = refl {𝓀 βŠ” (𝓣 ⁺)} {𝓛 X β†’ 𝓛 X}

𝓛̇-∘ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {Z : 𝓦 Μ‡ } (f : X β†’ Y) (g : Y β†’ Z)
     β†’ 𝓛̇ (g ∘ f) ＝ 𝓛̇ g ∘ 𝓛̇ f
𝓛̇-∘ f g = refl

\end{code}

And so do the naturality laws if we use appropriate notions of
equality in each case. The second is of course equivalent to identity,
but not definitionally.

\begin{code}

Ξ·-natural : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
          β†’ Ξ· ∘ f ＝ 𝓛̇ f ∘ Ξ·
Ξ·-natural f = refl

Ξ·-natural∼ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
           β†’ Ξ· ∘ f ∼ 𝓛̇ f ∘ Ξ·
η-natural∼ f _ = refl

ΞΌ-natural∼ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
           β†’ 𝓛̇ f ∘ ΞΌ ∼ ΞΌ ∘ 𝓛̇ (𝓛̇ f)
μ-natural∼ f _ = refl

ΞΌ-natural : funext (𝓣 ⁺ βŠ” 𝓀) (𝓣 ⁺ βŠ” π“₯)
          β†’ {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y)
          β†’ 𝓛̇ f ∘ ΞΌ ＝ ΞΌ ∘ 𝓛̇ (𝓛̇ f)
μ-natural fe f = dfunext fe (μ-natural∼ f)

\end{code}

We unit laws amount to the laws P Γ— πŸ™ ≃ P and πŸ™ Γ— P ≃ P:

\begin{code}

𝓛-unit-right⋍ : {X : 𝓀 Μ‡ } (l : 𝓛 X)
              β†’ ΞΌ (𝓛̇ Ξ· l) ⋍ l
𝓛-unit-right⋍ (P , Ο† , i) = e , refl
 where
  e : P Γ— πŸ™ ≃ P
  e = πŸ™-rneutral

𝓛-unit-left⋍ : {X : 𝓀 Μ‡ } (l : 𝓛 X)
             β†’ ΞΌ (Ξ· l) ⋍ l
𝓛-unit-left⋍ (P , Ο†) = e , refl
 where
  e : πŸ™ Γ— P ≃ P
  e = πŸ™-lneutral

𝓛-unit-right∼ : is-univalent 𝓣 β†’ {X : 𝓀 Μ‡ }
              β†’ ΞΌ ∘ 𝓛̇ Ξ· ∼ id
𝓛-unit-right∼ {𝓀} ua {X} l = ⋍-gives-＝ ua (𝓛-unit-right⋍ {𝓀} {X} l)

𝓛-unit-left∼ : is-univalent 𝓣 β†’ {X : 𝓀 Μ‡ }
              β†’ ΞΌ ∘ Ξ· ∼ id
𝓛-unit-left∼ {𝓀} ua {X} l = ⋍-gives-＝ ua (𝓛-unit-left⋍ {𝓀} {X} l)

\end{code}

The associativity of multiplication amounts to the associativity of Ξ£:

\begin{code}

𝓛-assoc⋍ : {X : 𝓀 Μ‡ } (l : 𝓛 (𝓛 (𝓛 X))) β†’ ΞΌ (ΞΌ l) ⋍ ΞΌ (𝓛̇ ΞΌ l)
𝓛-assoc⋍ (P , Ο†) = Ξ£-assoc , refl

𝓛-assoc∼ : is-univalent 𝓣 β†’ {X : 𝓀 Μ‡ } β†’ ΞΌ ∘ ΞΌ ∼ ΞΌ ∘ 𝓛̇ ΞΌ
𝓛-assoc∼ {𝓀} ua {X} l = ⋍-gives-＝ ua (𝓛-assoc⋍ {𝓀} {X} l)

\end{code}

Strengths:

\begin{code}

𝓛-Οƒ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ X Γ— 𝓛 Y β†’ 𝓛 (X Γ— Y)
𝓛-Οƒ (x , m) = 𝓛̇ (Ξ» y β†’ (x , y)) m

𝓛-Ο„ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ 𝓛 X Γ— Y β†’ 𝓛 (X Γ— Y)
𝓛-Ο„ (l , y) = 𝓛̇ (Ξ» x β†’ (x , y)) l

\end{code}

The monad is commutative, with its commutativity amounting to that of
_Γ—_:

\begin{code}

𝓛-comm : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } {l : 𝓛 X Γ— 𝓛 Y}
       β†’ ΞΌ (𝓛̇ 𝓛-Οƒ (𝓛-Ο„ l)) ⋍· ΞΌ (𝓛̇ 𝓛-Ο„ (𝓛-Οƒ l))
𝓛-comm = Γ—-comm , (Ξ» z β†’ refl)

𝓛-m : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ 𝓛 X Γ— 𝓛 Y β†’ 𝓛 (X Γ— Y)
𝓛-m (l , m) = ((Ξ» x β†’ curry 𝓛-Οƒ x m)β™―) l

\end{code}

TODO. Write down and prove the strength laws.

Or we can use the Kleisli-triple presentation of the monad, but the
proofs / constructions are essentially the same:

\begin{code}

Kleisli-Lawβ‚€ : {X : 𝓀 Μ‡ } (l : 𝓛 X) β†’ (Ξ· β™―) l ⋍ l
Kleisli-Lawβ‚€ (P , Ο†) = πŸ™-rneutral , refl

Kleisli-Law₁ : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ 𝓛 Y) (x : X) β†’ (f β™―) (Ξ· x) ⋍ f x
Kleisli-Law₁ f x = πŸ™-lneutral , refl

Kleisli-Lawβ‚‚ : {X : π“₯ Μ‡ } {Y : 𝓦 Μ‡ } {Z : 𝓣 Μ‡ } (f : X β†’ 𝓛 Y) (g : Y β†’ 𝓛 Z) (l : 𝓛 X)
             β†’ (g β™― ∘ f β™―) l ⋍ ((g β™― ∘ f)β™―) l
Kleisli-Lawβ‚‚ f g l = Ξ£-assoc , refl

𝓛̇' : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } β†’ (X β†’ Y) β†’ 𝓛 X β†’ 𝓛 Y
𝓛̇' f = (Ξ· ∘ f)β™―

𝓛̇-agreement : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ } (f : X β†’ Y) (l : 𝓛 X)
             β†’ 𝓛̇' f l ⋍· 𝓛̇ f l
𝓛̇-agreement {𝓀} {π“₯} {X} {Y} f (P , Ο† , i) = πŸ™-rneutral , Ξ» _ β†’ refl

\end{code}