{-# OPTIONS --safe #-}

open import Categories.Category.Core
open import Categories.Category.Cocartesian using (Cocartesian)
open import Categories.Functor hiding (id)
open import Categories.Object.Terminal using (Terminal)
open import Categories.Monad using (Monad)
open import Categories.NaturalTransformation hiding (id)

import Categories.Morphism.Reasoning as MR

module Monad.Instance.Maybe {o ℓ e} {C : Category o ℓ e} (cocartesian : Cocartesian C) (terminal : Terminal C) where
  open Category C
  open MR C
  open HomReasoning
  open Equiv
  open Cocartesian cocartesian
  open Terminal terminal

  maybeFunctor : Endofunctor C
  maybeFunctor = record
    { F₀           = λ X → X + ⊤
    ; F₁           = λ f → f +₁ id
    ; identity     = +-unique id-comm-sym id-comm-sym
    ; homomorphism = sym (+₁∘+₁ ○ +₁-cong₂ refl identity²)
    ; F-resp-≈     = λ eq → +₁-cong₂ eq refl
    }

  open Monad renaming (identityˡ to m-identityˡ; identityʳ to m-identityʳ; assoc to m-assoc; sym-assoc to m-sym-assoc)

  maybeMonad : Monad C
  maybeMonad .F = maybeFunctor
  maybeMonad .η = ntHelper (record { η = λ _ → i₁ 
                                   ; commute = λ _ → sym inject₁ })
  maybeMonad .μ = ntHelper (record { η = λ _ → [ id , i₂ ] 
                                   ; commute = λ _ → []∘+₁ ○ []-cong₂ id-comm-sym (sym inject₂) ○ sym ∘[]})
  maybeMonad .m-assoc = begin 
    [ id , i₂ ] ∘ ([ id , i₂ ] +₁ id)       ≈⟨ []∘+₁ ⟩ 
    [ id ∘ [ id , i₂ ] , i₂ ∘ id ]          ≈˘⟨ []-cong₂ id-comm (inject₂ ○ introʳ refl) ⟩
    [ [ id , i₂ ] ∘ id , [ id , i₂ ] ∘ i₂ ] ≈˘⟨ ∘[] ⟩
    [ id , i₂ ] ∘ [ id , i₂ ]               ∎
  maybeMonad .m-sym-assoc = sym (m-assoc maybeMonad)
  maybeMonad .m-identityˡ = []∘+₁ ○ +-unique refl id-comm-sym
  maybeMonad .m-identityʳ = inject₁