Maybe is an Equational Lifting Monad

module Monad.Instance.Maybe.EquationalLifting {o ℓ e} {C : Category o ℓ e} (distributive : Distributive C) where
  open Category C
  open MR C
  open HomReasoning
  open Equiv
  open Distributive distributive using (distributeˡ⁻¹; cartesian; cocartesian)
  open import Monad.EquationalLifting cartesian
  open import Categories.Category.Distributive.Properties distributive using (distributeˡ⁻¹-i₁; distributeˡ⁻¹-i₂)
  open Cocartesian cocartesian
  open Cartesian cartesian using (terminal; products)
  open BinaryProducts products renaming (unique to ⟨⟩-unique)
  open Terminal terminal

  open import Monad.Instance.Maybe.Commutative distributive
  open import Monad.Instance.Maybe.Strong distributive

The proof of the equational lifting law is pretty straightforward:

  maybeEqLifting : IsEquationalLiftingMonad (record { strongMonad = maybeStrong ; commutative = maybeCommutative })
  maybeEqLifting {X} = sym (+-unique inj₁ inj₂)
    where
    inj₁ : (((id +₁ !) ∘ distributeˡ⁻¹) ∘ Δ) ∘ i₁ ≈ i₁ ∘ ⟨ i₁ , id ⟩
    inj₁ = begin 
      (((id +₁ !) ∘ distributeˡ⁻¹) ∘ Δ) ∘ i₁                ≈⟨ pullʳ Δ∘ ⟩ 
      ((id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ i₁ , i₁ ⟩             ≈˘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ identityʳ) ⟩ 
      ((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ i₁) ∘ ⟨ i₁ , id ⟩ ≈⟨ pullʳ (pullˡ distributeˡ⁻¹-i₁) ⟩ 
      (id +₁ !) ∘ i₁ ∘ ⟨ i₁ , id ⟩                          ≈⟨ pullˡ (inject₁ ○ identityʳ) ⟩ 
      i₁ ∘ ⟨ i₁ , id ⟩                                      ∎
    inj₂ : (((id +₁ !) ∘ distributeˡ⁻¹) ∘ Δ) ∘ i₂ ≈ i₂ ∘ id
    inj₂ = begin 
      (((id +₁ !) ∘ distributeˡ⁻¹) ∘ Δ) ∘ i₂                ≈⟨ pullʳ Δ∘ ⟩ 
      ((id +₁ !) ∘ distributeˡ⁻¹) ∘ ⟨ i₂ , i₂ ⟩             ≈˘⟨ refl⟩∘⟨ (⁂∘⟨⟩ ○ ⟨⟩-cong₂ identityˡ identityʳ) ⟩ 
      ((id +₁ !) ∘ distributeˡ⁻¹) ∘ (id ⁂ i₂) ∘ ⟨ i₂ , id ⟩ ≈⟨ pullʳ (pullˡ distributeˡ⁻¹-i₂) ⟩ 
      (id +₁ !) ∘ i₂ ∘ ⟨ i₂ , id ⟩                          ≈⟨ pullˡ inject₂ ⟩ 
      (i₂ ∘ !) ∘ ⟨ i₂ , id ⟩                                ≈⟨ pullʳ (sym (!-unique (! ∘ ⟨ i₂ , id ⟩))) ⟩ 
      i₂ ∘ !                                                ≈⟨ refl⟩∘⟨ (!-unique id) ⟩ 
      i₂ ∘ id                                               ∎