{-# OPTIONS --type-in-type
    #-}

open import NeilPrelude

open import Maybe

module MaybeMonad where

mm2ndLaw : {A : Set} → {ma : Maybe A} → maybe nothing just ma ≡ ma
mm2ndLaw {_} {nothing} = refl
mm2ndLaw {_} {just _} = refl

mm3rdLaw : {A B C : Set} → {f : A → Maybe B} → {g : B → Maybe C} → (ma : Maybe A)
            → maybe nothing g (maybe nothing f ma) ≡ maybe nothing (\a → maybe nothing g (f a)) ma
mm3rdLaw nothing = refl
mm3rdLaw (just a) = refl

mm5thLaw : {A B : Set} → (ma : Maybe A) → maybe {A} {Maybe B} nothing (\_ → nothing) ma ≡ nothing
mm5thLaw nothing  = refl
mm5thLaw (just _) = refl

mm7thLaw : {A : Set} → {ma : Maybe A} → maybe nothing just ma ≡ ma
mm7thLaw {_} {nothing} = refl
mm7thLaw {_} {just _} = refl

import MonadPlus
open MonadPlus Maybe (flip (maybe nothing)) just (\ma mb → maybe mb just ma) nothing refl (λ _ → mm2ndLaw) (λ _ → mm3rdLaw) refl mm5thLaw refl mm7thLaw public