The Maybe Monad

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

The functor X + 1:

  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
    }

extends to a monad:

  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₁