_Appendix: Proving that Maybe is definitely a functor._

Time to dot our i's and cross our t's.

We've defined two functions:

Maybe: Ob(Hask) -> Ob(Hask)
Maybe: Arrows(Hask) -> Arrows(Hask)

Now to show that it's a functor, we need to prove: it maps the endpoints of arrows correctly, it preserves identities, and it respects compositions.

We already showed endpoint preservation: Maybe(f: a -> b): Maybe(a) -> Maybe(b).

Next, let's prove the identity law.

Maybe(id_A)(Nothing) = Nothing
Maybe(id_A)(Just(x)) = Just(id_A(x)) = Just(x)

This shows what we needed: \\(Maybe(id_A\\)) = \\(id_{Maybe(A))}\\)

Now suppose f: a -> b, g: b -> c.

Then g . f: a -> c.

Maybe(g . f): Maybe(a) -> Maybe(c).

Maybe(g . f)(Nothing) = Nothing

Maybe(g . f)(Just(x)) = Just((g . f)(x)) = Just(g(f(x)) = Maybe(g)(Maybe(f)(Just(x))).

Hence, Maybe(g . f) = Maybe(g) . Maybe(f).

That's it, we've proven that Maybe is a _bona fide_ functor.