open import Level
open import Categories.Category.Core
open import Categories.Category.Distributive using (Distributive)
open import Categories.Object.Terminal using (Terminal)

import Categories.Morphism.Reasoning as MR

-- 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 import Category.Distributive.Helper distributive
  open import Monad.EquationalLifting cartesian
  open Terminal terminal

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

  maybeEquationalLifting : EquationalLifting (record { strongMonad = maybeStrong ; commutative = maybeCommutative })
  maybeEquationalLifting {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                                               ∎

  maybeEquationalLiftingMonad : EquationalLiftingMonad
  maybeEquationalLiftingMonad = record { commutativeMonad = maybeCommutativeMonad ; equationalLifting = maybeEquationalLifting }