feat(library/init): add functor/monad to init folder

library/init/default.lean

@@ -8,3 +8,4 @@ import init.datatypes init.reserved_notation init.tactic init.logic
 import init.relation init.wf init.nat init.wf_k init.prod
 import init.bool init.num init.sigma init.measurable init.setoid init.quot
 import init.funext init.function init.subtype init.classical init.simplifier
+import init.monad

library/init/functor.lean

@@ -0,0 +1,9 @@
+/-
+Copyright (c) Luke Nelson and Jared Roesch. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Luke Nelson and Jared Roesch
+-/
+prelude
+
+structure functor [class] (f : Type → Type) : Type :=
+(map : Π {a b: Type}, (a → b) → f a → f b)

library/init/monad.lean

@@ -0,0 +1,11 @@
+/-
+Copyright (c) Luke Nelson and Jared Roesch. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Luke Nelson and Jared Roesch
+-/
+prelude
+import init.functor
+
+structure monad [class] (m : Type → Type) extends functor m : Type :=
+(return : Π {a:Type}, a → m a)
+(bind   : Π {a b: Type}, m a → (a → m b) → m b)