Monad.idr

The Maybe Monad

It is well documented that the Maybe type as defined by data Maybe a = Nothing | Just a is a monad in $\mathcal{S}et$. The following demonstrates that in our categorical framework by first ensuring it’s a well-behaved functor, and then proving that its join and pure method respect the usual monad conditions.

To prove it is a monad we give definitions for join. pure is given by the Just constructor.

MaybeIsMonad : Monad Set MaybeIsFunctor
MaybeIsMonad = MkMonad
  (MkNT
    (\_ => Just)
    (\_, _, m => Refl))
  (MkNT
    (\_ => joinMaybe)
    (\a, b, m => funExt $ \case Nothing => Refl
                                (Just x) => Refl)
    )
  (\_ => funExt joinMaybeMap)
  (\_ => Refl)
  (\_ => funExt joinMapId)