diff --git a/_CoqConfig b/_CoqConfig
index 112ca51d..9db2ee8f 100644
--- a/_CoqConfig
+++ b/_CoqConfig
@@ -11,8 +11,13 @@ theories/Basics/CategoryTheory.v
 theories/Basics/CategoryFacts.v
 theories/Basics/CategorySub.v
 theories/Basics/CategoryFunctor.v
+theories/Basics/Applicative.v
+theories/Basics/Functor.v
 theories/Basics/Monad.v
+theories/Basics/MonadId.v
 theories/Basics/MonadState.v
+theories/Basics/MonadEither.v
+theories/Basics/MonadWriter.v
 theories/Basics/CategoryKleisli.v
 theories/Basics/CategoryKleisliFacts.v
 theories/Basics/Function.v
diff --git a/theories/Basics/Applicative.v b/theories/Basics/Applicative.v
new file mode 100644
index 00000000..4df81df2
--- /dev/null
+++ b/theories/Basics/Applicative.v
@@ -0,0 +1,9 @@
+Class Applicative@{d c} (T : Type@{d} -> Type@{c}) :=
+{ pure : forall {A : Type@{d}}, A -> T A
+; ap : forall {A B : Type@{d}}, T (A -> B) -> T A -> T B
+}.
+
+Module ApplicativeNotation.
+  Notation "f <*> x" := (ap f x) (at level 52, left associativity).
+End ApplicativeNotation.
+
diff --git a/theories/Basics/Basics.v b/theories/Basics/Basics.v
index 50c4da15..c066b2ff 100644
--- a/theories/Basics/Basics.v
+++ b/theories/Basics/Basics.v
@@ -9,16 +9,6 @@ From Coq Require
 From Coq Require Import
      RelationClasses.
 
-From ExtLib Require Import
-     Structures.Functor
-     Structures.Monad
-     Data.Monads.StateMonad
-     Data.Monads.ReaderMonad
-     Data.Monads.OptionMonad
-     Data.Monads.EitherMonad.
-
-Import MonadNotation.
-Local Open Scope monad.
 (* end hide *)
 
 (** ** Parametric functions *)
@@ -103,48 +93,63 @@ Section ProdRelInstances.
 
 End ProdRelInstances.
 
-
 (** ** Common monads and transformers. *)
 
-Module Monads.
-
-Definition identity (a : Type) : Type := a.
-
-Definition stateT (s : Type) (m : Type -> Type) (a : Type) : Type :=
-  s -> m (prod s a).
-Definition state (s a : Type) := s -> prod s a.
-
-Definition readerT (r : Type) (m : Type -> Type) (a : Type) : Type :=
-  r -> m a.
-Definition reader (r a : Type) := r -> a.
-
-Definition writerT (w : Type) (m : Type -> Type) (a : Type) : Type :=
-  m (prod w a).
-Definition writer := prod.
-
-Instance Functor_stateT {m s} {Fm : Functor m} : Functor (stateT s m)
-  := {|
-    fmap _ _ f := fun run s => fmap (fun sa => (fst sa, f (snd sa))) (run s)
-    |}.
-
-Instance Monad_stateT {m s} {Fm : Monad m} : Monad (stateT s m)
-  := {|
-    ret _ a := fun s => ret (s, a)
-  ; bind _ _ t k := fun s =>
-      sa <- t s ;;
-      k (snd sa) (fst sa)
-    |}.
-
-End Monads.
-
-(** ** Loop operator *)
-
-(** [iter]: A primitive for general recursion.
-    Iterate a function updating an accumulator [I], until it produces
-    an output [R].
- *)
-Polymorphic Class MonadIter (M : Type -> Type) : Type :=
-  iter : forall {R I: Type}, (I -> M (I + R)%type) -> I -> M R.
+(* Module Monads. *)
+
+(* Definition identity (a : Type) : Type := a. *)
+
+(* Definition eitherT (exc : Type) (m: Type -> Type) (a: Type) : Type := *)
+(*   m (sum exc a). *)
+(* Definition either (exc : Type) (a : Type) : Type := *)
+(*   sum exc a. *)
+
+(* Definition stateT (s : Type) (m : Type -> Type) (a : Type) : Type := *)
+(*   s -> m (prod s a). *)
+(* Definition state (s a : Type) := s -> prod s a. *)
+
+(* Definition readerT (r : Type) (m : Type -> Type) (a : Type) : Type := *)
+(*   r -> m a. *)
+(* Definition reader (r a : Type) := r -> a. *)
+
+(* Definition writerT (w : Type) (m : Type -> Type) (a : Type) : Type := *)
+(*   m (prod w a). *)
+(* Definition writer := prod. *)
+
+(* Instance Functor_stateT {m s} {Fm : Functor m} : Functor (stateT s m) *)
+(*   := {| *)
+(*     fmap _ _ f := fun run s => fmap (fun sa => (fst sa, f (snd sa))) (run s) *)
+(*     |}. *)
+
+(* Instance Monad_stateT {m s} {Fm : Monad m} : Monad (stateT s m) *)
+(*   := {| *)
+(*     ret _ a := fun s => ret (s, a) *)
+(*   ; bind _ _ t k := fun s => *)
+(*       sa <- t s ;; *)
+(*       k (snd sa) (fst sa) *)
+(*     |}. *)
+
+(* Instance Functor_eitherT {m exc} {Fm : Functor m} : Functor (eitherT exc m) *)
+(*   := {| *)
+(*       fmap _ _ f :=  fmap (fun ma => match ma with *)
+(*                                   | inl e => inl e *)
+(*                                   | inr a => inr (f a) *)
+(*                                   end) *)
+(*     |}. *)
+
+(* Program Instance Monad_eitherT {m exc} {Fm : Monad m} : Monad (eitherT exc m) *)
+(*   := {| *)
+(*       ret _ a := ret (inr a) *)
+(*       ; bind _ _ t k := *)
+(*           bind (m := m) t *)
+(*                (fun ma => *)
+(*                   match ma with *)
+(*                   | inl e => ret (inl e) *)
+(*                   | inr a => k a *)
+(*                   end) *)
+(*     |}. *)
+
+(* End Monads. *)
 
 (** *** Transformer instances *)
 
@@ -153,66 +158,66 @@ Polymorphic Class MonadIter (M : Type -> Type) : Type :=
     Quite easily in fact, no [Monad] assumption needed.
  *)
 
-Instance MonadIter_stateT {M S} {MM : Monad M} {AM : MonadIter M}
-  : MonadIter (stateT S M) :=
-  fun _ _ step i => mkStateT (fun s =>
-    iter (fun is =>
-      let i := fst is in
-      let s := snd is in
-      is' <- runStateT (step i) s ;;
-      ret match fst is' with
-          | inl i' => inl (i', snd is')
-          | inr r => inr (r, snd is')
-          end) (i, s)).
-
-Polymorphic Instance MonadIter_stateT0 {M S} {MM : Monad M} {AM : MonadIter M}
-  : MonadIter (Monads.stateT S M) :=
-  fun _ _ step i s =>
-    iter (fun si =>
-      let s := fst si in
-      let i := snd si in
-      si' <- step i s;;
-      ret match snd si' with
-          | inl i' => inl (fst si', i')
-          | inr r => inr (fst si', r)
-          end) (s, i).
-
-Instance MonadIter_readerT {M S} {AM : MonadIter M} : MonadIter (readerT S M) :=
-  fun _ _ step i => mkReaderT (fun s =>
-    iter (fun i => runReaderT (step i) s) i).
-
-Instance MonadIter_optionT {M} {MM : Monad M} {AM : MonadIter M}
-  : MonadIter (optionT M) :=
-  fun _ _ step i => mkOptionT (
-    iter (fun i =>
-      oi <- unOptionT (step i) ;;
-      ret match oi with
-          | None => inr None
-          | Some (inl i) => inl i
-          | Some (inr r) => inr (Some r)
-          end) i).
-
-Instance MonadIter_eitherT {M E} {MM : Monad M} {AM : MonadIter M}
-  : MonadIter (eitherT E M) :=
-  fun _ _ step i => mkEitherT (
-    iter (fun i =>
-      ei <- unEitherT (step i) ;;
-      ret match ei with
-          | inl e => inr (inl e)
-          | inr (inl i) => inl i
-          | inr (inr r) => inr (inr r)
-          end) i).
+(* Instance MonadIter_stateT {M S} {MM : Monad M} {AM : MonadIter M} *)
+(*   : MonadIter (stateT S M) := *)
+(*   fun _ _ step i => mkStateT (fun s => *)
+(*     iter (fun is => *)
+(*       let i := fst is in *)
+(*       let s := snd is in *)
+(*       is' <- runStateT (step i) s ;; *)
+(*       ret match fst is' with *)
+(*           | inl i' => inl (i', snd is') *)
+(*           | inr r => inr (r, snd is') *)
+(*           end) (i, s)). *)
+
+(* Polymorphic Instance MonadIter_stateT0 {M S} {MM : Monad M} {AM : MonadIter M} *)
+(*   : MonadIter (Monads.stateT S M) := *)
+(*   fun _ _ step i s => *)
+(*     iter (fun si => *)
+(*       let s := fst si in *)
+(*       let i := snd si in *)
+(*       si' <- step i s;; *)
+(*       ret match snd si' with *)
+(*           | inl i' => inl (fst si', i') *)
+(*           | inr r => inr (fst si', r) *)
+(*           end) (s, i). *)
+
+(* Instance MonadIter_readerT {M S} {AM : MonadIter M} : MonadIter (readerT S M) := *)
+(*   fun _ _ step i => mkReaderT (fun s => *)
+(*     iter (fun i => runReaderT (step i) s) i). *)
+
+(* Instance MonadIter_optionT {M} {MM : Monad M} {AM : MonadIter M} *)
+(*   : MonadIter (optionT M) := *)
+(*   fun _ _ step i => mkOptionT ( *)
+(*     iter (fun i => *)
+(*       oi <- unOptionT (step i) ;; *)
+(*       ret match oi with *)
+(*           | None => inr None *)
+(*           | Some (inl i) => inl i *)
+(*           | Some (inr r) => inr (Some r) *)
+(*           end) i). *)
+
+(* Instance MonadIter_eitherT {M E} {MM : Monad M} {AM : MonadIter M} *)
+(*   : MonadIter (eitherT E M) := *)
+(*   fun _ _ step i => mkEitherT ( *)
+(*     iter (fun i => *)
+(*       ei <- unEitherT (step i) ;; *)
+(*       ret match ei with *)
+(*           | inl e => inr (inl e) *)
+(*           | inr (inl i) => inl i *)
+(*           | inr (inr r) => inr (inr r) *)
+(*           end) i). *)
 
 (** And the nondeterminism monad [_ -> Prop] also has one. *)
 
-Inductive iter_Prop {R I : Type} (step : I -> I + R -> Prop) (i : I) (r : R)
-  : Prop :=
-| iter_done
-  : step i (inr r) -> iter_Prop step i r
-| iter_step i'
-  : step i (inl i') ->
-    iter_Prop step i' r ->
-    iter_Prop step i r
-.
-
-Polymorphic Instance MonadIter_Prop : MonadIter Ensembles.Ensemble := @iter_Prop.
+(* Inductive iter_Prop {R I : Type} (step : I -> I + R -> Prop) (i : I) (r : R) *)
+(*   : Prop := *)
+(* | iter_done *)
+(*   : step i (inr r) -> iter_Prop step i r *)
+(* | iter_step i' *)
+(*   : step i (inl i') -> *)
+(*     iter_Prop step i' r -> *)
+(*     iter_Prop step i r *)
+(* . *)
+
+(* Polymorphic Instance MonadIter_Prop : MonadIter Ensembles.Ensemble := @iter_Prop. *)
diff --git a/theories/Basics/CategoryKleisli.v b/theories/Basics/CategoryKleisli.v
index 2ec6daec..bcd56126 100644
--- a/theories/Basics/CategoryKleisli.v
+++ b/theories/Basics/CategoryKleisli.v
@@ -18,9 +18,6 @@
 From Coq Require Import
      Morphisms.
 
-From ExtLib Require Import
-     Structures.Monad.
-
 From ITree Require Import
      Basics.Basics
      Basics.CategoryOps
@@ -56,7 +53,7 @@ Section Instances.
 
   Definition map {a b c} (g:b -> c) (ab : Kleisli m a b) : Kleisli m a c :=
      cat ab (pure g).
-  
+
   Global Instance Initial_Kleisli : Initial (Kleisli m) void :=
     fun _ v => match v : void with end.
 
@@ -73,6 +70,15 @@ Section Instances.
     fun _ _ => pure inr.
 
   Global Instance Iter_Kleisli `{MonadIter m} : Iter (Kleisli m) sum :=
-    fun a b => Basics.iter.
+    fun a b => iter.
 
 End Instances.
+
+(* Convenient equation to switch perspective between the monadic and categorical view. *)
+Lemma iter_monad_to_cat:
+  forall {M} {IM: MonadIter M} a b,
+    @Monad.iter M IM a b = @CategoryOps.iter Type (Kleisli M) sum _ b a.
+Proof.
+  reflexivity.
+Qed.
+
diff --git a/theories/Basics/CategoryKleisliFacts.v b/theories/Basics/CategoryKleisliFacts.v
index b312e277..52771a64 100644
--- a/theories/Basics/CategoryKleisliFacts.v
+++ b/theories/Basics/CategoryKleisliFacts.v
@@ -6,9 +6,6 @@ From Coq Require Import
      Morphisms
      RelationClasses.
 
-From ExtLib Require Import
-     Structures.Monad.
-
 From ITree Require Import
      Basics.Basics
      Basics.Category
diff --git a/theories/Basics/Functor.v b/theories/Basics/Functor.v
new file mode 100644
index 00000000..82a0a972
--- /dev/null
+++ b/theories/Basics/Functor.v
@@ -0,0 +1,7 @@
+Polymorphic Class Functor@{d c} (F : Type@{d} -> Type@{c}) : Type :=
+  { fmap : forall {A B : Type@{d}}, (A -> B) -> F A -> F B }.
+
+Module FunctorNotation.
+  Notation "f <$> x" := (@fmap _ _ _ _ f x) (at level 52, left associativity).
+End FunctorNotation.
+
diff --git a/theories/Basics/Monad.v b/theories/Basics/Monad.v
index bbbf7d8a..098cb985 100644
--- a/theories/Basics/Monad.v
+++ b/theories/Basics/Monad.v
@@ -4,9 +4,6 @@
 From Coq Require Import
      Morphisms.
 
-From ExtLib Require Export
-     Structures.Monad.
-
 From ITree Require Import
      Basics.Basics
      Basics.CategoryOps
@@ -14,17 +11,85 @@ From ITree Require Import
 (* end hide *)
 
 Set Primitive Projections.
+Set Universe Polymorphism.
+
+Set Implicit Arguments.
+Set Strict Implicit.
+
+Class Monad@{d c} (m : Type@{d} -> Type@{c}) : Type :=
+{ ret : forall {t : Type@{d}}, t -> m t
+; bind : forall {t u : Type@{d}}, m t -> (t -> m u) -> m u
+}.
 
 Class EqM (m:Type -> Type) : Type :=
   eqm : forall a, m a -> m a -> Prop.
 
 Class EqMProps (m:Type -> Type) `{Monad m} `{EqM m} :=
       eqm_equiv :> forall a, Equivalence (eqm a).
-
+Arguments EqMProps m {_ _}.
 Arguments eqm {m _ _}.
+Declare Scope monad_scope.
 Infix "≈" := eqm (at level 70) : monad_scope.
 
-Section Laws.
+Section monadic.
+
+  Definition liftM@{d c}
+              {m : Type@{d} -> Type@{c}}
+              {M : Monad m}
+              {T U : Type@{d}} (f : T -> U) : m T -> m U :=
+    fun x => bind x (fun x => ret (f x)).
+
+  Definition liftM2@{d c}
+              {m : Type@{d} -> Type@{c}}
+              {M : Monad m}
+              {T U V : Type@{d}} (f : T -> U -> V) : m T -> m U -> m V :=
+    Eval cbv beta iota zeta delta [ liftM ] in
+      fun x y => bind x (fun x => liftM (f x) y).
+
+  Definition liftM3@{d c}
+              {m : Type@{d} -> Type@{c}}
+              {M : Monad m}
+              {T U V W : Type@{d}} (f : T -> U -> V -> W) : m T -> m U -> m V -> m W :=
+    Eval cbv beta iota zeta delta [ liftM2 ] in
+      fun x y z => bind x (fun x => liftM2 (f x) y z).
+
+  Definition apM@{d c}
+              {m : Type@{d} -> Type@{c}}
+              {M : Monad m}
+              {A B : Type@{d}} (fM:m (A -> B)) (aM:m A) : m B :=
+    bind fM (fun f => liftM f aM).
+
+  (* Left-to-right composition of Kleisli arrows. *)
+  Definition mcompose@{c d}
+             {m:Type@{d}->Type@{c}}
+             {M: Monad m}
+             {T U V:Type@{d}}
+             (f: T -> m U) (g: U -> m V): (T -> m V) :=
+    fun x => bind (f x) g.
+
+End monadic.
+
+Module MonadNotation.
+
+  Delimit Scope monad_scope with monad.
+
+  Notation "c >>= f" := (@bind _ _ _ _ c f) (at level 58, left associativity) : monad_scope.
+  Notation "f =<< c" := (@bind _ _ _ _ c f) (at level 61, right associativity) : monad_scope.
+  Notation "f >=> g" := (@mcompose _ _ _ _ _ f g) (at level 61, right associativity) : monad_scope.
+
+  Notation "x <- c1 ;; c2" := (@bind _ _ _ _ c1 (fun x => c2))
+    (at level 61, c1 at next level, right associativity) : monad_scope.
+
+  Notation "e1 ;; e2" := (_ <- e1%monad ;; e2%monad)%monad
+    (at level 61, right associativity) : monad_scope.
+
+  Notation "' pat <- c1 ;; c2" :=
+    (@bind _ _ _ _ c1 (fun x => match x with pat => c2 end))
+    (at level 61, pat pattern, c1 at next level, right associativity) : monad_scope.
+
+End MonadNotation.
+
+Section MonadLaws.
 
   Context (m : Type -> Type).
   Context {EqM : @EqM m}.
@@ -33,7 +98,6 @@ Section Laws.
 
   Local Open Scope monad_scope.
 
-  (* This should go coq-ext-lib. *)
   Class MonadLaws :=
     { bind_ret_l : forall a b (f : a -> m b) (x : a), bind (ret x) f ≈ f x
     ; bind_ret_r : forall a (x : m a), bind x (fun y => ret y) ≈ x
@@ -44,9 +108,113 @@ Section Laws.
          bind)
     }.
 
-End Laws.
+End MonadLaws.
 
+Arguments MonadLaws m {_ _}.
 Arguments bind_ret_l {m _ _ _}.
 Arguments bind_ret_r {m _ _ _}.
 Arguments bind_bind {m _ _ _}.
 Arguments Proper_bind {m _ _ _}.
+
+(** ** Loop operator *)
+
+(** [iter]: A primitive for general recursion.
+    Iterate a function updating an accumulator [I], until it produces
+    an output [R].
+ *)
+Polymorphic Class MonadIter (M : Type -> Type) : Type :=
+  iter : forall {R I: Type}, (I -> M (I + R)%type) -> I -> M R.
+
+(* Its laws are defined by its [Kleisli] category forming an [Iterative] category *)
+
+Section MonadHomomorphism.
+
+  Local Open Scope monad_scope.
+
+  Variable M M': Type -> Type.
+  Context {MM: Monad M}.
+  Context {MM': Monad M'}.
+  Context {IM: MonadIter M}.
+  Context {IM': MonadIter M'}.
+  Context {EqMM': @EqM M'}.
+  Variable F: M ~> M'.
+
+  Class MonadHom: Prop :=
+    {
+      resp_ret : forall A (a: A), F (ret a) ≈ ret a;
+      resp_bind: forall A B (m: M A) (k: A -> M B),
+          F (bind m k) ≈ bind (F m) (fun x => F (k x))
+    }.
+
+  Class IterHom: Prop :=
+    {
+      resp_iter: forall (I R: Type) (body: I -> M (I + R)%type) i,
+        F (iter body i) ≈ iter (fun x => F (body x)) i
+    }.
+
+End MonadHomomorphism.
+
+(* TO PLUG IN WHENEVER
+
+Section MonadTriggerable.
+
+  Local Open Scope monad_scope.
+
+  Variable M M': Type -> Type.
+  Context {MM: Monad M}.
+  Context {MM': Monad M'}.
+  Context {EqMM': @EqM M'}.
+  Context {IM: MonadIter M}.
+  Context {IM': MonadIter M'}.
+
+  (**
+     Monads that allow for the embedding of an effect as a minimal
+     monadic effectful computation are dubbed "Triggerable".
+   *)
+
+  Class Triggerable (E: Type -> Type) := trigger: E ~> M.
+
+  (* The correctness of this operation, i.e. its minimality, is expressed
+     with respect to a notion of interpretation of monads.
+     A monad [M] is said to be "Interpretable" into a monad [M'] if there
+     is a family of monad monomorphisms for each handler [h: E ~> M'].
+   *)
+
+  Class Interpretable :=
+    interp: forall (E: Type -> Type) (h: E ~> M'), M ~> M'.
+
+  Class InterpCorrect E {InterpMM': Interpretable} {TrigM: Triggerable E}: Prop :=
+    {
+      interp_monad_hom h :> MonadHom (interp E h);
+      interp_iter_hom  h :> IterHom (interp E h);
+      interp_trigger h T (e: E T): interp E h (trigger _ e) ≈ h _ e
+    }.
+
+End MonadTriggerable.
+
+ *)
+
+Import CatNotations.
+Local Open Scope cat_scope.
+Local Open Scope monad_scope.
+
+Ltac rw_pointed_l H :=
+  match goal with
+    |- ?f ?x ≈ _ =>
+    let tmp := fresh "H" in
+    assert (tmp: f ⩯ f) by reflexivity;
+    setoid_rewrite H in tmp at 1;
+    specialize (tmp x);
+    setoid_rewrite <- tmp
+  end.
+
+Ltac rw_pointed_r H :=
+  match goal with
+    |- _ ≈ ?f ?x =>
+    let tmp := fresh "H" in
+    assert (tmp: f ⩯ f) by reflexivity;
+    setoid_rewrite H in tmp at 1;
+    specialize (tmp x);
+    setoid_rewrite <- tmp
+  end.
+
diff --git a/theories/Basics/MonadEither.v b/theories/Basics/MonadEither.v
new file mode 100644
index 00000000..4d0f8952
--- /dev/null
+++ b/theories/Basics/MonadEither.v
@@ -0,0 +1,245 @@
+From Coq Require Import
+     Setoid
+     Morphisms.
+
+From ITree Require Import
+     Basics.Basics
+     Basics.Category
+     Basics.CategoryKleisli
+     Basics.CategoryKleisliFacts
+     Basics.Functor
+     Basics.Monad.
+
+Import CatNotations.
+Import MonadNotation.
+Local Open Scope cat_scope.
+Local Open Scope cat.
+Local Open Scope monad_scope.
+
+Definition eitherT (exn: Type) (M: Type -> Type) (a: Type) : Type :=
+  M (sum exn a).
+Definition either (exn a : Type) : Type :=
+  sum exn a.
+
+Section Functor_Either.
+  Global Instance Functor_eitherT {M} {Fm : Functor M} (exn: Type) : Functor (eitherT exn M)
+    := {|
+        fmap _ _ f :=  fmap (fun ma => match ma with
+                                    | inl e => inl e
+                                    | inr a => inr (f a)
+                                    end)
+      |}.
+
+End Functor_Either.
+
+Section Monad_Either.
+  Variable M : Type -> Type.
+  Variable exn : Type.
+  Context {EQM : EqM M}.
+  Context {HM: Monad M}.
+  Context {HEQP: @EqMProps M _ EQM}.
+  Context {ML: @MonadLaws M _ HM}.
+
+  Global Instance Monad_eitherT : Monad (eitherT exn M)
+    := {|
+        ret _ a := ret (inr a)
+        ; bind _ _ t k :=
+            bind (m := M) t
+                 (fun ma =>
+                    match ma with
+                    | inl e => ret (inl e)
+                    | inr a => k a
+                    end)
+      |}.
+
+  Global Instance EqM_eitherTM : EqM (eitherT exn M) := fun _ => eqm (m := M).
+
+  Global Instance EqMProps_eitherTM : @EqMProps _ _ EqM_eitherTM.
+  Proof.
+  constructor.
+  - repeat red; reflexivity.
+  - repeat red; intros x y; cbn; symmetry; auto.
+  - repeat red; intros x y z; cbn; etransitivity; eauto.
+  Qed.
+
+  Instance MonadLaws_eitherTM : @MonadLaws (eitherT exn M) _ _.
+  Proof.
+  constructor.
+  - cbn. intros a b f x.
+    repeat red.
+    rewrite bind_ret_l; cbn.
+    reflexivity.
+  - cbn; intros a x. unfold eitherT in x.
+    unfold eqm, EqM_eitherTM.
+    match goal with
+      |- _ ≈ ?h => rewrite <- (bind_ret_r _ h) at 2
+    end.
+    apply Proper_bind; [reflexivity | intros [b | m]; reflexivity].
+  - cbn. intros a b c x f g; cbn.
+    rewrite bind_bind. do 2 red.
+    apply Proper_bind; [reflexivity | intros [? | m]].
+    + rewrite bind_ret_l; reflexivity.
+    + reflexivity.
+  - cbn; intros a b x y EQ x' y' H'; cbn in *.
+    do 2 red; apply Proper_bind; [auto | intros [? | ?]]; [reflexivity | apply H'].
+  Qed.
+
+End Monad_Either.
+
+Section Iter_Either.
+
+  Variable M : Type -> Type.
+  Variable exn : Type.
+  Context {EQM : EqM M}.
+  Context {HM: Monad M}.
+  Context {HEQP: @EqMProps M HM EQM}.
+  Context {ML: @MonadLaws M EQM HM}.
+  Context {IM: MonadIter M}.
+  Context {CM: Iterative (Kleisli M) sum}.
+
+  Definition iso {a b:Type} (Aab : exn + (a + b)) : (a  + (exn + b)) :=
+    match Aab with
+    | inl A => inr (inl A)
+    | inr (inl a) => inl a
+    | inr (inr b) => inr (inr b)
+    end.
+
+  Definition internalize {a b:Type} (f : Kleisli (eitherT exn M) a b) : Kleisli M a (exn + b) := f.
+
+  Global Instance Iter_eitherTM : MonadIter (eitherT exn M) :=
+    fun (b a: Type) (f: a -> M (exn + (a + b))) x =>
+      iter ((internalize f) >>> (pure iso)) x.
+
+  Instance proper_internalize {a b}: Proper (eq2 ==> eq2) (@internalize a b).
+  intros x y H o; apply H.
+  Qed.
+
+  Global Instance Proper_Iter_eitherTM : forall a b, @Proper (Kleisli (eitherT exn M) a (a + b) -> (Kleisli (eitherT exn M) a b)) (eq2 ==> eq2) iter.
+  Proof.
+    destruct CM.
+    intros A B x y H a.
+    apply iterative_proper_iter.
+    apply cat_eq2_r.
+    rewrite H; reflexivity.
+  Qed.
+
+  Global Instance IterUnfold_eitherTM : IterUnfold (Kleisli (eitherT exn M)) sum.
+  Proof.
+    intros A B f a; cbn.
+    unfold CategoryOps.iter, Iter_Kleisli.
+    rewrite iter_monad_to_cat.
+    rw_pointed_l iter_unfold.
+    unfold cat, Cat_Kleisli.
+    do 2 red.
+    rewrite bind_bind.
+    apply Proper_bind.
+    + reflexivity.
+    + intros [xA | [xa | xb]]; unfold pure; rewrite bind_ret_l; reflexivity.
+  Qed.
+
+  Global Instance IterNatural_eitherTM : IterNatural (Kleisli (eitherT exn M)) sum.
+  Proof.
+    destruct CM.
+    intros A B C f g a; cbn.
+    setoid_rewrite iterative_natural.
+    apply iterative_proper_iter; intros a'.
+    unfold cat, Cat_Kleisli.
+    unfold internalize; cbn.
+    rewrite! bind_bind.
+    apply Proper_bind; [reflexivity |].
+    intros [xA | [xa | xb]]; unfold pure; cbn; rewrite !bind_ret_l; cbn; unfold cat, Cat_Kleisli; cbn.
+    - rewrite bind_ret_l; cbn; reflexivity.
+    - unfold id_, Id_Kleisli, pure; rewrite bind_bind, !bind_ret_l; reflexivity.
+    - cbn; rewrite bind_bind.
+      apply Proper_bind; [reflexivity |].
+      intros [? | ?]; rewrite bind_ret_l; reflexivity.
+  Qed.
+
+  Lemma iter_dinatural_helper:
+    forall (a b c : Type) (f : Kleisli (eitherT exn M) a (b + c)) (g : Kleisli (eitherT exn M) b (a + c)),
+      internalize (f >>> case_ g inr_) >>> pure iso ⩯ internalize f >>> pure iso >>> case_ (internalize g >>> pure iso) inr_.
+  Proof.
+    destruct CM.
+    intros a b c f g o.
+    unfold cat, Cat_Kleisli, internalize; cbn.
+    repeat rewrite bind_bind; cbn.
+    unfold pure; cbn.
+    apply Proper_bind; [reflexivity | intros [xA | [xa | xb]]]; cbn.
+    - rewrite !bind_ret_l; reflexivity.
+    - rewrite bind_ret_l; reflexivity.
+    - rewrite !bind_ret_l; reflexivity.
+  Qed.
+
+  Global Instance IterDinatural_eitherTM : IterDinatural (Kleisli (eitherT exn M)) sum.
+  Proof.
+    destruct CM.
+    unfold IterDinatural.
+    intros A B C f g a.
+    unfold iter, Iter_eitherTM. cbn.
+    eapply transitivity.
+    eapply iterative_proper_iter.
+    apply iter_dinatural_helper.
+    rewrite iterative_dinatural.
+    cbn.
+    unfold cat, Cat_Kleisli.
+    rewrite bind_bind.
+    unfold internalize. cbn.
+    do 2 red.
+    apply Proper_bind.
+    - reflexivity.
+    - unfold pure; cbn; intros [xA | [xa | xb]]; cbn.
+      + rewrite bind_ret_l; cbn; reflexivity.
+      + rewrite bind_ret_l; cbn.
+        eapply iterative_proper_iter.
+        intros ?; rewrite !bind_bind.
+        apply Proper_bind; [reflexivity | intros [|[|]]]; cbn; rewrite !bind_ret_l; try reflexivity.
+      + rewrite bind_ret_l; cbn.
+        reflexivity.
+  Qed.
+
+  Global Instance IterCodiagonal_eitherTM : IterCodiagonal (Kleisli (eitherT exn M)) sum.
+  Proof.
+    destruct CM.
+    unfold IterCodiagonal.
+    intros a b f o.
+    unfold iter, Iter_eitherTM.
+    cbn.
+    eapply transitivity.
+    eapply iterative_proper_iter.
+    eapply Proper_cat_Kleisli; [| reflexivity].
+    unfold internalize; cbn. reflexivity.
+    eapply transitivity.
+
+    eapply iterative_proper_iter.
+    apply iterative_natural.
+    rewrite iterative_codiagonal.
+    eapply iterative_proper_iter.
+    rewrite cat_assoc, bimap_case, cat_id_l, cat_id_r.
+    unfold internalize.
+    intros o'; cbn.
+    unfold cat, Cat_Kleisli; cbn; rewrite !bind_bind; cbn.
+    apply Proper_bind; [reflexivity | intros [| [|]]].
+    unfold pure; rewrite !bind_ret_l; reflexivity.
+    unfold pure; cbn; rewrite !bind_ret_l; reflexivity.
+    unfold pure; cbn; rewrite !bind_ret_l; reflexivity.
+  Qed.
+
+  Global Instance Iterative_eitherTM : Iterative (Kleisli (eitherT exn M)) sum.
+  Proof.
+  constructor;
+  typeclasses eauto.
+  Qed.
+
+End Iter_Either.
+
+(* Section Interpretable_Either. *)
+
+(*   Variable M : Type -> Type. *)
+(*   Variable exn : Type. *)
+(*   Context {EQM : EqM M}. *)
+(*   Context {HM: Monad M}. *)
+(*   Context {HEQP: @EqMProps M _ EQM}. *)
+(*   Context {ML: @MonadLaws M _ HM}. *)
+(*   Context {IM: MonadIter M}. *)
+(*   Context {CM: Iterative (Kleisli M) sum}. *)
+
diff --git a/theories/Basics/MonadId.v b/theories/Basics/MonadId.v
new file mode 100644
index 00000000..00a3fb5b
--- /dev/null
+++ b/theories/Basics/MonadId.v
@@ -0,0 +1,22 @@
+From Coq Require Import
+     Setoid
+     Morphisms.
+
+From ITree Require Import
+     Basics.Basics
+     Basics.Category
+     Basics.CategoryKleisli
+     Basics.CategoryKleisliFacts
+     Basics.Functor
+     Basics.Monad.
+
+Import CatNotations.
+Import MonadNotation.
+Local Open Scope cat_scope.
+Local Open Scope cat.
+Local Open Scope monad_scope.
+
+Definition identityT (M: Type -> Type) (a: Type) : Type := a.
+Definition identity (a : Type) : Type := a.
+
+
diff --git a/theories/Basics/MonadState.v b/theories/Basics/MonadState.v
index 921658e7..6a32f83d 100644
--- a/theories/Basics/MonadState.v
+++ b/theories/Basics/MonadState.v
@@ -3,22 +3,35 @@ From Coq Require Import
      Setoid
      Morphisms.
 
-From ExtLib Require Import
-     Structures.Monad.
-
 From ITree Require Import
      Basics.Basics
      Basics.Category
      Basics.CategoryKleisli
      Basics.CategoryKleisliFacts
+     Basics.Functor
      Basics.Monad.
 
-Import ITree.Basics.Basics.Monads.
 Import CatNotations.
+Import MonadNotation.
 Local Open Scope cat_scope.
 Local Open Scope cat.
+Local Open Scope monad_scope.
+
+Definition stateT (S: Type) (M: Type -> Type) (A : Type) : Type :=
+  S -> M (prod S A).
+Definition state (S A : Type) := S -> prod S A.
+
+Section Functor_State.
+
+  Global Instance Functor_stateT {M} {Fm : Functor M} {S} : Functor (stateT S M)
+    := {|
+        fmap _ _ f := fun run s => fmap (fun sa => (fst sa, f (snd sa))) (run s)
+      |}.
+
+End Functor_State.
+
+Section Monad_State.
 
-Section State.
   Variable M : Type -> Type.
   Variable S : Type.
   Context {EQM : EqM M}.
@@ -26,6 +39,14 @@ Section State.
   Context {HEQP: @EqMProps M _ EQM}.
   Context {ML: @MonadLaws M _ HM}.
 
+  Global Instance Monad_stateT : Monad (stateT S M)
+    := {|
+        ret _ a := fun s => ret (s, a)
+        ; bind _ _ t k := fun s =>
+                            sa <- t s ;;
+                            k (snd sa) (fst sa)
+      |}.
+
   Global Instance EqM_stateTM : EqM (stateT S M).
   Proof.
     exact (fun a => pointwise_relation _ eqm).
@@ -40,7 +61,7 @@ Section State.
   - repeat red. intros. etransitivity; eauto. apply H.  apply H0.
   Qed.
 
-  Instance MonadLaws_stateTM : @MonadLaws (stateT S M) _ _.
+  Global Instance MonadLaws_stateTM : @MonadLaws (stateT S M) _ _.
   Proof.
   constructor.
   - cbn. intros a b f x.
@@ -66,7 +87,17 @@ Section State.
       apply H0.
   Qed.
 
-  Context {IM: Iter (Kleisli M) sum}.
+End Monad_State.
+
+Section Iter_State.
+
+  Variable M : Type -> Type.
+  Variable S : Type.
+  Context {EQM : EqM M}.
+  Context {HM: Monad M}.
+  Context {HEQP: @EqMProps M _ EQM}.
+  Context {ML: @MonadLaws M _ HM}.
+  Context {IM: MonadIter M}.
   Context {CM: Iterative (Kleisli M) sum}.
 
   Definition iso {a b:Type} (sab : S * (a + b)) : (S * a) + (S * b) :=
@@ -111,7 +142,6 @@ Section State.
     reflexivity.
   Qed.
 
-
   Lemma internalize_pure {a b c} (f : Kleisli (stateT S M) a b) (g : S * b -> S * c) :
     internalize f >>> pure g   ⩯   (internalize (f >>> (fun b s => ret (g (s,b))))).
   Proof.
@@ -125,13 +155,9 @@ Section State.
       unfold pure. reflexivity.
   Qed.
 
-
-  Global Instance Iter_stateTM : Iter (Kleisli (stateT S M)) sum.
-  Proof.
-    exact
-      (fun (a b : Type) (f : a -> S -> M (S * (a + b))) (x:a) (s:S) =>
-        iter ((internalize f) >>> (pure iso)) (s, x)).
-  Defined.
+  Global Instance Iter_stateTM : MonadIter (stateT S M) :=
+    fun a b (body: b -> S -> M (S * (b + a))) x s =>
+      iter ((internalize body) >>> (pure iso)) (s, x).
 
   Global Instance Proper_Iter_stateTM : forall a b, @Proper (Kleisli (stateT S M) a (a + b) -> (Kleisli (stateT S M) a b)) (eq2 ==> eq2) iter.
   Proof.
@@ -149,43 +175,38 @@ Section State.
 
   Global Instance IterUnfold_stateTM : IterUnfold (Kleisli (stateT S M)) sum.
   Proof.
-  destruct CM.
-  unfold IterUnfold.
-  intros a b f.
-  repeat red.
-  intros a0 s.
-  unfold cat, Cat_Kleisli.
-  unfold iter, Iter_stateTM.
-  rewrite iterative_unfold.  (* SAZ: why isn't iter_unfold exposed here? *)
-  unfold cat, Cat_Kleisli.
-  simpl.
-  rewrite bind_bind.
-  apply Proper_bind.
-  + reflexivity.
-  + repeat red. destruct a1 as [s' [x | y]]; simpl.
-    * unfold pure. rewrite bind_ret_l.
-      reflexivity.
-    * unfold pure. rewrite bind_ret_l.
-      reflexivity.
+    (* destruct CM. *)
+    unfold IterUnfold, CategoryOps.iter, Iter_Kleisli, iter, Iter_stateTM.
+    intros A B f a s.
+    rewrite iter_monad_to_cat.
+    rw_pointed_l iter_unfold.
+    unfold cat, Cat_Kleisli.
+    simpl.
+    rewrite bind_bind.
+    apply Proper_bind.
+    + reflexivity.
+    + intros [? [? | ?]]; simpl.
+      * unfold pure. rewrite bind_ret_l.
+        reflexivity.
+      * unfold pure. rewrite bind_ret_l.
+        reflexivity.
   Qed.
 
   Global Instance IterNatural_stateTM : IterNatural (Kleisli (stateT S M)) sum.
   Proof.
     destruct CM.
-    unfold IterNatural.
-    intros a b c f g.
-    repeat red.
-    intros a0 s.
+    intros A B C f g a s.
+    unfold CategoryOps.iter, Iter_Kleisli, iter, Iter_stateTM.
     setoid_rewrite iterative_natural.
     apply iterative_proper_iter.
     repeat red.
-    destruct a1.
+    intros [].
     unfold cat, Cat_Kleisli.
     cbn.
     rewrite! bind_bind.
     apply Proper_bind.
     - reflexivity.
-    - repeat red. destruct a2 as [s' [x | y]]; simpl.
+    - repeat red. intros [s' [x | y]]; simpl.
       + unfold pure. rewrite bind_ret_l.
         cbn. unfold cat, Cat_Kleisli. cbn.
         rewrite bind_bind.
@@ -198,7 +219,7 @@ Section State.
         rewrite bind_bind.
         apply Proper_bind.
         * reflexivity.
-        * repeat red. destruct a2.
+        * repeat red. intros [].
           cbn.
           rewrite bind_ret_l. reflexivity.
   Qed.
@@ -357,4 +378,4 @@ Section State.
   typeclasses eauto.
   Qed.
 
-End State.
+End Iter_State.
diff --git a/theories/Basics/MonadWriter.v b/theories/Basics/MonadWriter.v
new file mode 100644
index 00000000..4fff3a03
--- /dev/null
+++ b/theories/Basics/MonadWriter.v
@@ -0,0 +1,23 @@
+(* begin hide *)
+From Coq Require Import
+     Setoid
+     Morphisms.
+
+From ITree Require Import
+     Basics.Basics
+     Basics.Category
+     Basics.CategoryKleisli
+     Basics.CategoryKleisliFacts
+     Basics.Functor
+     Basics.Monad.
+
+Import CatNotations.
+Import MonadNotation.
+Local Open Scope cat_scope.
+Local Open Scope cat.
+Local Open Scope monad_scope.
+
+Definition writerT (W: Type) (M: Type -> Type) (A : Type) : Type :=
+  M (prod W A).
+Definition writer := prod.
+
diff --git a/theories/Core/ITreeDefinition.v b/theories/Core/ITreeDefinition.v
index f6370e82..6b4ba660 100644
--- a/theories/Core/ITreeDefinition.v
+++ b/theories/Core/ITreeDefinition.v
@@ -1,12 +1,9 @@
 (** * Interaction trees: core definitions *)
 
 (* begin hide *)
-Require Import ExtLib.Structures.Functor.
-Require Import ExtLib.Structures.Applicative.
-Require Import ExtLib.Structures.Monad.
 Require Import Program.Tactics.
 
-From ITree Require Import Basics.
+From ITree Require Import Basics Monad Applicative Functor.
 
 Set Implicit Arguments.
 Set Contextual Implicit.
@@ -213,6 +210,7 @@ Definition map {E R S} (f : R -> S)  (t : itree E R) : itree E S :=
 (** Atomic itrees triggering a single event. *)
 Definition trigger {E : Type -> Type} : E ~> itree E :=
   fun R e => Vis e (fun x => Ret x).
+(* Instance trigger_itree {E: Type -> Type} : Triggerable (itree E) E := trigger. *)
 
 (** Ignore the result of a tree. *)
 Definition ignore {E R} : itree E R -> itree E unit :=
diff --git a/theories/Core/KTreeFacts.v b/theories/Core/KTreeFacts.v
index 031eecf9..8d78e1ba 100644
--- a/theories/Core/KTreeFacts.v
+++ b/theories/Core/KTreeFacts.v
@@ -152,7 +152,7 @@ Lemma unfold_iter_ktree {E A B} (f : ktree E A (A + B)) (a0 : A) :
     | inr b => Ret b
     end.
 Proof.
-  unfold iter, Iter_Kleisli, Basics.iter, MonadIter_itree, cat.
+  unfold iter, Iter_Kleisli, Monad.iter, MonadIter_itree, cat.
   rewrite unfold_iter; cbn.
   eapply eqit_bind; try reflexivity.
 Qed.
diff --git a/theories/Events/Dependent.v b/theories/Events/Dependent.v
index 3c6b5fe4..764de262 100644
--- a/theories/Events/Dependent.v
+++ b/theories/Events/Dependent.v
@@ -16,11 +16,12 @@
 (* begin hide *)
 From ITree Require Import
      Basics.Basics
+     Basics.Monad
+     Basics.MonadId
      Core.ITreeDefinition
      Indexed.Sum
      Core.Subevent.
 
-Import Basics.Basics.Monads.
 (* end hide *)
 
 Variant depE {I : Type} (F : I -> Type) : Type -> Type :=
diff --git a/theories/Events/Map.v b/theories/Events/Map.v
index d6dbade3..fcc58f6f 100644
--- a/theories/Events/Map.v
+++ b/theories/Events/Map.v
@@ -8,14 +8,12 @@ From Coq Require Import
      String List.
 Import ListNotations.
 
-From ExtLib Require Import
-     Core.RelDec.
-
 From ExtLib.Structures Require
-     Functor Monoid Maps.
+     Monoid Maps.
 
 From ITree Require Import
      Basics.Basics
+     Basics.MonadState
      Basics.CategoryOps
      Core.ITreeDefinition
      Indexed.Sum
@@ -23,7 +21,6 @@ From ITree Require Import
      Interp.Interp
      Events.State.
 
-Import ITree.Basics.Basics.Monads.
 (* end hide *)
 
 Section Map.
diff --git a/theories/Events/MapDefault.v b/theories/Events/MapDefault.v
index ab55564d..09e0f37c 100644
--- a/theories/Events/MapDefault.v
+++ b/theories/Events/MapDefault.v
@@ -8,10 +8,13 @@ From ExtLib Require Import
      Core.RelDec.
 
 From ExtLib.Structures Require
-     Functor Monoid Maps.
+     Monoid Maps.
 
 From ITree Require Import
      Basics.Basics
+     Basics.Functor
+     Basics.Monad
+     Basics.MonadState
      Basics.CategoryOps
      Core.ITreeDefinition
      Indexed.Sum
@@ -19,7 +22,6 @@ From ITree Require Import
      Interp.Interp
      Events.State.
 
-Import ITree.Basics.Basics.Monads.
 (* end hide *)
 
 Section Map.
@@ -35,7 +37,7 @@ Section Map.
   Arguments Insert {d}.
   Arguments LookupDef {d}.
   Arguments Remove {d}.
-  
+
   Definition insert {E d} `{(mapE d) -< E} : K -> V -> itree E unit := embed Insert.
   Definition lookup_def {E d} `{(mapE d) -< E} : K -> itree E V := embed LookupDef.
   Definition remove {E d} `{(mapE d) -< E} : K -> itree E unit := embed Remove.
@@ -50,7 +52,7 @@ Section Map.
     | Some v' => v'
     | None => d
     end.
-  
+
   Definition handle_map {E d} : mapE d ~> stateT map (itree E) :=
     fun _ e env =>
       match e with
@@ -60,7 +62,7 @@ Section Map.
       end.
 
   (* SAZ: I think that all of these [run_foo] functions should be renamed
-     [interp_foo].  That would be more consistent with the idea that 
+     [interp_foo].  That would be more consistent with the idea that
      we define semantics by nested interpretation.  Also, it seems a bit
      strange to define [interp_map] in terms of [interp_state].
   *)
@@ -73,7 +75,7 @@ Section Map.
      answers under [lookup_default] *)
   Definition eq_map (d:V) (m1 m2 : map) : Prop :=
     forall k, lookup_default k d m1 = lookup_default k d m2.
-  
+
 End Map.
 
 Arguments insert {K V E d _}.
diff --git a/theories/Events/MapDefaultFacts.v b/theories/Events/MapDefaultFacts.v
index 529866d5..c0c0f1da 100644
--- a/theories/Events/MapDefaultFacts.v
+++ b/theories/Events/MapDefaultFacts.v
@@ -13,12 +13,15 @@ From ExtLib Require Import
      Core.RelDec.
 
 From ExtLib.Structures Require
-     Functor Monoid Maps.
+     Monoid Maps.
 
 From Paco Require Import paco.
 
 From ITree Require Import
      Basics.Basics
+     Basics.Monad
+     Basics.Functor
+     Basics.MonadState
      Basics.CategoryOps
      ITree
      ITreeFacts
@@ -28,7 +31,6 @@ From ITree Require Import
      Events.StateFacts
      Events.MapDefault.
 
-Import ITree.Basics.Basics.Monads.
 Import Structures.Maps.
 (* end hide *)
 
@@ -45,7 +47,7 @@ Section MapFacts.
   Lemma lookup_add_eq: forall k v s, lookup k (add k v s) = Some v.
   Proof.
     intros.
-    rewrite mapsto_lookup; apply mapsto_add_eq. 
+    rewrite mapsto_lookup; apply mapsto_add_eq.
     Unshelve.
     2: typeclasses eauto.
   Qed.
@@ -101,7 +103,7 @@ Section MapFacts.
   Global Instance eq_map_refl {d} : Reflexive (@eq_map _ _ _ _ d).
   Proof.
     red. intros. unfold eq_map. tauto.
-  Qed.    
+  Qed.
 
   Global Instance eq_map_sym {d} : Symmetric (@eq_map _ _ _ _ d).
   Proof.
@@ -113,7 +115,7 @@ Section MapFacts.
 
   Global Instance eq_map_trans {d} : Transitive (@eq_map _ _ _ _ d).
   Proof.
-    repeat intro. 
+    repeat intro.
     unfold eq_map in *.
     rewrite H. rewrite H0. reflexivity.
   Qed.
@@ -123,7 +125,7 @@ Section MapFacts.
   Context {R1 R2 : Type}.
   Variable RR : R1 -> R2 -> Prop.
 
-  Definition map_default_eq d {E} 
+  Definition map_default_eq d {E}
     : (stateT map (itree E) R1) -> (stateT map (itree E) R2) -> Prop :=
     fun t1 t2 => forall s1 s2, (@eq_map _ _ _ _ d) s1 s2 -> eutt (prod_rel (@eq_map _ _ _ _ d) RR) (t1 s1) (t2 s2).
 
@@ -141,7 +143,7 @@ Section MapFacts.
       rewrite 2 lookup_add_eq; reflexivity.
     - unfold lookup_default in *.
       rewrite 2 lookup_add_neq; auto.
-  Qed.      
+  Qed.
 
   Lemma eq_map_remove:
     forall (d : V) (s1 s2 : map) (k : K), (@eq_map _ _ _ _ d) s1 s2 -> (@eq_map _ _ _ _ d) (remove k s1) (remove k s2).
@@ -154,8 +156,8 @@ Section MapFacts.
     - rewrite 2 lookup_remove_neq; auto.
       apply H.
   Qed.
-  
-  Lemma handle_map_eq : 
+
+  Lemma handle_map_eq :
     forall d E X (s1 s2 : map) (m : mapE K d X),
       (@eq_map _ _ _ _ d) s1 s2 ->
       eutt (prod_rel (@eq_map _ _ _ _ d) eq) (handle_map m s1) ((handle_map m s2) : itree E (map * X)).
@@ -175,8 +177,8 @@ Section MapFacts.
     apply handle_map_eq.
     assumption.
   Qed.
-    
-  
+
+
   (* This lemma states that the operations provided by [handle_map] respect
      the equivalence on the underlying map interface *)
   Lemma interp_map_id d {E X} (t : itree (mapE K d +' E) X) :
@@ -202,7 +204,7 @@ Section MapFacts.
         gstep; constructor.
         gbase. apply CH. assumption.
   Qed.
- 
+
   Global Instance interp_map_proper {R E d} {RR : R -> R -> Prop} :
     Proper ((eutt RR) ==> (@map_default_eq _ _ RR d E)) (@interp_map _ _ _ _ E d R).
   Proof.
@@ -212,7 +214,7 @@ Section MapFacts.
     einit.
     ecofix CH.
     intros.
-    rewrite! unfold_interp_state. 
+    rewrite! unfold_interp_state.
     punfold H0. red in H0.
     revert s1 s2 H1.
     induction H0; intros; subst; simpl; pclearbot.
@@ -225,7 +227,7 @@ Section MapFacts.
         destruct e. apply handle_map_eq. assumption.
         unfold pure_state.
         pstep. econstructor. intros. constructor. pfold. econstructor. constructor; auto.
-      } 
+      }
       intros.
       inversion H. subst.
       estep; constructor. ebase.
@@ -234,5 +236,5 @@ Section MapFacts.
     - rewrite tau_euttge, unfold_interp_state.
       eauto.
   Qed.
-    
+
 End MapFacts.
diff --git a/theories/Events/State.v b/theories/Events/State.v
index ca262519..52a7e409 100644
--- a/theories/Events/State.v
+++ b/theories/Events/State.v
@@ -3,12 +3,11 @@
 (** Events to read and update global state. *)
 
 (* begin hide *)
-From ExtLib Require Import
-     Structures.Functor
-     Structures.Monad.
-
 From ITree Require Import
      Basics.Basics
+     Basics.Functor
+     Basics.Monad
+     Basics.MonadState
      Basics.CategoryOps
      Basics.CategoryKleisli
      Core.ITreeDefinition
@@ -17,7 +16,6 @@ From ITree Require Import
      Core.Subevent
      Interp.Interp.
 
-Import ITree.Basics.Basics.Monads.
 Import ITreeNotations.
 
 Open Scope itree_scope.
diff --git a/theories/Events/StateFacts.v b/theories/Events/StateFacts.v
index db612636..192347d2 100644
--- a/theories/Events/StateFacts.v
+++ b/theories/Events/StateFacts.v
@@ -11,6 +11,8 @@ From Paco Require Import paco.
 
 From ITree Require Import
      Basics.Basics
+     Basics.Monad
+     Basics.MonadState
      Basics.Category
      Basics.CategoryKleisli
      Basics.Monad
@@ -25,12 +27,10 @@ From ITree Require Import
      Interp.RecursionFacts
      Events.State.
 
-Import ITree.Basics.Basics.Monads.
 Import ITreeNotations.
 
 Open Scope itree_scope.
 
-Import Monads.
 (* end hide *)
 
 Definition _interp_state {E F S R}
@@ -42,23 +42,24 @@ Definition _interp_state {E F S R}
   | VisF e k => f _ e s >>= (fun sx => Tau (interp_state f (k (snd sx)) (fst sx)))
   end.
 
-Lemma unfold_interp_state {E F S R} (h : E ~> Monads.stateT S (itree F))
+Lemma unfold_interp_state {E F S R} (h : E ~> stateT S (itree F))
       (t : itree E R) s :
     eq_itree eq
       (interp_state h t s)
       (_interp_state h (observe t) s).
 Proof.
-  unfold interp_state, interp, Basics.iter, MonadIter_stateT0, Basics.iter, MonadIter_itree; cbn.
+  unfold interp_state, interp, iter, Iter_stateTM, iter, MonadIter_itree, internalize; cbn.
   rewrite unfold_iter; cbn.
+  rewrite bind_bind. 
   destruct observe; cbn.
   - rewrite 2 bind_ret_l. reflexivity.
   - rewrite 2 bind_ret_l.
     reflexivity.
-  - rewrite bind_map, bind_bind; cbn. setoid_rewrite bind_ret_l.
+  - rewrite bind_map. cbn. setoid_rewrite bind_ret_l.
     apply eqit_bind; reflexivity.
 Qed.
 
-Instance eq_itree_interp_state {E F S R} (h : E ~> Monads.stateT S (itree F)) :
+Instance eq_itree_interp_state {E F S R} (h : E ~> stateT S (itree F)) :
   Proper (eq_itree eq ==> eq ==> eq_itree eq)
          (@interp_state _ _ _ _ _ _ h R).
 Proof.
@@ -83,7 +84,7 @@ Proof.
 Qed.
 
 Lemma interp_state_vis {E F : Type -> Type} {S T U : Type}
-      (e : E T) (k : T -> itree E U) (h : E ~> Monads.stateT S (itree F)) (s : S)
+      (e : E T) (k : T -> itree E U) (h : E ~> stateT S (itree F)) (s : S)
   : interp_state h (Vis e k) s
   ≅ h T e s >>= fun sx => Tau (interp_state h (k (snd sx)) (fst sx)).
 Proof.
@@ -91,14 +92,14 @@ Proof.
 Qed.
 
 Lemma interp_state_tau {E F : Type -> Type} S {T : Type}
-      (t : itree E T) (h : E ~> Monads.stateT S (itree F)) (s : S)
+      (t : itree E T) (h : E ~> stateT S (itree F)) (s : S)
   : interp_state h (Tau t) s ≅ Tau (interp_state h t s).
 Proof.
   rewrite unfold_interp_state; reflexivity.
 Qed.
 
 Lemma interp_state_trigger {E F : Type -> Type} {R S : Type}
-      (e : E R) (f : E ~> Monads.stateT S (itree F)) (s : S)
+      (e : E R) (f : E ~> stateT S (itree F)) (s : S)
   : (interp_state f (ITree.trigger e) s) ≅ (f _ e s >>= fun x => Tau (Ret x)).
 Proof.
   unfold ITree.trigger. rewrite interp_state_vis.
@@ -134,7 +135,7 @@ Proof.
 Qed.
 
 Instance eutt_interp_state {E F: Type -> Type} {S : Type}
-         (h : E ~> Monads.stateT S (itree F)) R RR :
+         (h : E ~> stateT S (itree F)) R RR :
   Proper (eutt RR ==> eq ==> eutt (prod_rel eq RR)) (@interp_state E (itree F) S _ _ _ h R).
 Proof.
   repeat intro. subst. revert_until R.
@@ -152,7 +153,7 @@ Proof.
 Qed.
 
 Instance eutt_interp_state_eq {E F: Type -> Type} {S : Type}
-         (h : E ~> Monads.stateT S (itree F)) R :
+         (h : E ~> stateT S (itree F)) R :
   Proper (eutt eq ==> eq ==> eutt eq) (@interp_state E (itree F) S _ _ _ h R).
 Proof.
   repeat intro. subst. revert_until R.
@@ -173,7 +174,7 @@ Qed.
 Lemma eutt_interp_state_aloop {E F S I I' A A'}
       (RA : A -> A' -> Prop) (RI : I -> I' -> Prop)
       (RS : S -> S -> Prop)
-      (h : E ~> Monads.stateT S (itree F))
+      (h : E ~> stateT S (itree F))
       (t1 : I -> itree E (I + A))
       (t2 : I' -> itree E (I' + A')):
   (forall i i' s1 s2, RS s1 s2 -> RI i i' ->
@@ -199,7 +200,7 @@ Qed.
 Lemma eutt_interp_state_iter {E F S A A' B B'}
       (RA : A -> A' -> Prop) (RB : B -> B' -> Prop)
       (RS : S -> S -> Prop)
-      (h : E ~> Monads.stateT S (itree F))
+      (h : E ~> stateT S (itree F))
       (t1 : A -> itree E (A + B))
       (t2 : A' -> itree E (A' + B')) :
   (forall ca ca' s1 s2, RS s1 s2 ->
@@ -209,14 +210,14 @@ Lemma eutt_interp_state_iter {E F S A A' B B'}
           (interp_state h (t2 ca') s2)) ->
   (forall a a' s1 s2, RS s1 s2 -> RA a a' ->
      eutt (fun a b => RS (fst a) (fst b) /\ RB (snd a) (snd b))
-          (interp_state h (iter (C := ktree _) t1 a) s1)
-          (interp_state h (iter (C := ktree _) t2 a') s2)).
+          (interp_state h (CategoryOps.iter (C := ktree _) t1 a) s1)
+          (interp_state h (CategoryOps.iter (C := ktree _) t2 a') s2)).
 Proof.
   apply eutt_interp_state_aloop.
 Qed.
 
 Lemma eutt_interp_state_loop {E F S A B C} (RS : S -> S -> Prop)
-      (h : E ~> Monads.stateT S (itree F))
+      (h : E ~> stateT S (itree F))
       (t1 t2 : C + A -> itree E (C + B)) :
   (forall ca s1 s2, RS s1 s2 ->
      eutt (fun a b => RS (fst a) (fst b) /\ snd a = snd b)
@@ -255,9 +256,9 @@ Lemma interp_state_iter {E F } S (f : E ~> stateT S (itree F)) {I A}
       (t' : I -> stateT S (itree F) (I + A))
       (EQ_t : forall i, state_eq (State.interp_state f (t i)) (t' i))
   : forall i, state_eq (State.interp_state f (ITree.iter t i))
-                  (Basics.iter t' i).
+                  (iter t' i).
 Proof.
-  unfold Basics.iter, MonadIter_stateT0, Basics.iter, MonadIter_itree in *; cbn.
+  unfold iter, Iter_stateTM, iter, MonadIter_itree in *; cbn.
   ginit. gcofix CIH; intros i s.
   rewrite 2 unfold_iter; cbn.
   rewrite !bind_bind.
@@ -275,7 +276,7 @@ Qed.
 Lemma interp_state_iter' {E F } S (f : E ~> stateT S (itree F)) {I A}
       (t  : I -> itree E (I + A))
   : forall i, state_eq (State.interp_state f (ITree.iter t i))
-                       (Basics.iter (fun i => State.interp_state f (t i)) i).
+                       (iter (fun i => State.interp_state f (t i)) i).
 Proof.
   eapply interp_state_iter.
   intros i.
diff --git a/theories/Events/Writer.v b/theories/Events/Writer.v
index 1f2e208f..328b3005 100644
--- a/theories/Events/Writer.v
+++ b/theories/Events/Writer.v
@@ -11,13 +11,17 @@ From Coq Require Import
 Import ListNotations.
 
 From ExtLib Require Import
-     Structures.Functor
-     Structures.Monad
+(*      Structures.Functor *)
+(*      Structures.Monad *)
      Structures.Monoid.
 
 From ITree Require Import
      Basics.Basics
      Basics.CategoryOps
+     Basics.Functor
+     Basics.Monad
+     Basics.MonadState
+     Basics.MonadWriter
      Core.ITreeDefinition
      Indexed.Sum
      Core.Subevent
@@ -25,7 +29,6 @@ From ITree Require Import
      Interp.Handler
      Events.State.
 
-Import Basics.Basics.Monads.
 (* end hide *)
 
 (** Event to output values of type [W]. *)
@@ -68,7 +71,7 @@ Definition handle_writer {W E} (Monoid_W : Monoid W)
   : writerE W ~> stateT W (itree E)
   := fun _ e s =>
        match e with
-       | Tell w => Ret (monoid_plus Monoid_W s w, tt) 
+       | Tell w => Ret (monoid_plus Monoid_W s w, tt)
        end.
 
 Definition run_writer {W E} (Monoid_W : Monoid W)
diff --git a/theories/Interp/Handler.v b/theories/Interp/Handler.v
index 3084fbb8..f8195788 100644
--- a/theories/Interp/Handler.v
+++ b/theories/Interp/Handler.v
@@ -9,6 +9,7 @@ From Coq Require Import
 
 From ITree Require Import
      Basics.Basics
+     Basics.Monad
      Basics.Category
      Core.ITreeDefinition
      Eq.Eq
@@ -18,7 +19,6 @@ From ITree Require Import
      Interp.Interp
      Interp.Recursion.
 
-Import ITree.Basics.Basics.Monads.
 Import ITreeNotations.
 
 Open Scope itree_scope.
diff --git a/theories/Interp/HandlerFacts.v b/theories/Interp/HandlerFacts.v
index 125aef74..31ecc4b0 100644
--- a/theories/Interp/HandlerFacts.v
+++ b/theories/Interp/HandlerFacts.v
@@ -10,6 +10,7 @@ From Paco Require Import paco.
 
 From ITree Require Import
      Basics.Basics
+     Basics.Monad
      Basics.Category
      Core.ITreeDefinition
      Eq.Eq
@@ -21,7 +22,6 @@ From ITree Require Import
      Interp.InterpFacts
      Interp.RecursionFacts.
 
-Import ITree.Basics.Basics.Monads.
 Import ITreeNotations.
 
 Open Scope itree_scope.
diff --git a/theories/Interp/Interp.v b/theories/Interp/Interp.v
index cd59dde8..defc14d1 100644
--- a/theories/Interp/Interp.v
+++ b/theories/Interp/Interp.v
@@ -30,12 +30,10 @@
  *)
 
 (* begin hide *)
-From ExtLib Require Import
-     Structures.Functor
-     Structures.Monad.
-
 From ITree Require Import
      Basics.Basics
+     Basics.Monad
+     Basics.Functor
      Core.ITreeDefinition
      Indexed.Relation.
 (* end hide *)
diff --git a/theories/Interp/InterpEither.v b/theories/Interp/InterpEither.v
new file mode 100644
index 00000000..5cb967c0
--- /dev/null
+++ b/theories/Interp/InterpEither.v
@@ -0,0 +1,65 @@
+(** * Monadic interpretations of interaction trees *)
+
+(** We can derive semantics for an interaction tree [itree E ~> M]
+    from semantics given for every individual event [E ~> M],
+    when [M] is a monad (actually, with some more structure).
+
+    We define the following terminology for this library.
+    Other sources may have different usages for the same or related
+    words.
+
+    The notation [E ~> F] stands for [forall T, E T -> F T]
+    (in [ITree.Basics]).
+    It can mean many things, including the following:
+
+    - The semantics of itrees are given as monad morphisms
+      [itree E ~> M], also called "interpreters".
+
+    - "ITree interpreters" (or "itree morphisms") are monad morphisms
+      where the codomain is made of ITrees: [itree E ~> itree F].
+
+    Interpreters can be obtained from handlers:
+
+    - In general, "event handlers" are functions [E ~> M] where
+      [M] is a monad.
+
+    - "ITree event handlers" are functions [E ~> itree F].
+
+    Categorically, this boils down to saying that [itree] is a free
+    monad (not quite, but close enough).
+ *)
+
+(* begin hide *)
+From ITree Require Import
+     Basics.Basics
+     Basics.Monad
+     Basics.MonadEither
+     Core.ITreeDefinition
+     Indexed.Relation.
+(* end hide *)
+
+Definition interp_either {E M : Type -> Type} {A: Type}
+           {FM : Functor M} {MM : Monad M} {IM : MonadIter M}
+           (h : E ~> eitherT A M) :
+  eitherT A (itree E) ~> eitherT A M :=
+  fun R => iter (fun t =>
+                match observe (unEitherT t) with
+                | RetF (inl a) => mkEitherT (ret (inl a))
+                | RetF (inr r) => ret (inr r)
+                | TauF t => ret (inl (mkEitherT t))
+                | VisF e k => fmap (fun x => inl (mkEitherT (k x))) (h _ e)
+                end).
+
+Definition interp_either' {E M : Type -> Type} {A: Type}
+           {FM : Functor M} {MM : Monad M} {IM : MonadIter M}
+           (h : E ~> M) :
+  eitherT A (itree E) ~> eitherT A M :=
+  fun R => iter (fun t =>
+                match observe (unEitherT t) with
+                | RetF (inl a) => mkEitherT (ret (inl a))
+                | RetF (inr r) => ret (inr r)
+                | TauF t => ret (inl (mkEitherT t))
+                | VisF e k => fmap (fun x => inl (mkEitherT (k x))) (MonadTrans.lift (h _ e))
+                end).
+
+Arguments interp_either {E M A FM MM IM} h [T].
diff --git a/theories/Interp/InterpFacts.v b/theories/Interp/InterpFacts.v
index 361984bd..898b5cd6 100644
--- a/theories/Interp/InterpFacts.v
+++ b/theories/Interp/InterpFacts.v
@@ -68,7 +68,7 @@ Definition _interp {E F R} (f : E ~> itree F) (ot : itreeF E R _)
 Lemma unfold_interp {E F R} {f : E ~> itree F} (t : itree E R) :
   interp f t ≅ (_interp f (observe t)).
 Proof.
-  unfold interp. unfold Basics.iter, MonadIter_itree. rewrite unfold_iter.
+  unfold interp. unfold Monad.iter, MonadIter_itree. rewrite unfold_iter.
   destruct (observe t); cbn;
     rewrite ?bind_ret_l, ?bind_map; reflexivity.
 Qed.
@@ -349,7 +349,7 @@ Lemma interp_iter {E F} (f : E ~> itree F) {A B}
       (t : A -> itree E (A + B)) a0
   : interp f (iter t a0) ≅ iter (C := ktree _) (fun a => interp f (t a)) a0.
 Proof.
-  unfold iter, Iter_Kleisli, Basics.iter, MonadIter_itree.
+  unfold iter, Iter_Kleisli, Monad.iter, MonadIter_itree.
   apply interp_iter'.
   reflexivity.
 Qed.
diff --git a/theories/Interp/Recursion.v b/theories/Interp/Recursion.v
index c6affc57..c4d7e1d6 100644
--- a/theories/Interp/Recursion.v
+++ b/theories/Interp/Recursion.v
@@ -5,7 +5,7 @@ From ITree Require Import
      Core.ITreeDefinition
      Indexed.Sum.
 
-Import ITree.Basics.Basics.Monads.
+Import ITree.Basics.Monad.
 Import ITreeNotations.
 
 Open Scope itree_scope.
diff --git a/theories/Interp/TranslateFacts.v b/theories/Interp/TranslateFacts.v
index 1e1e1b73..471e8b56 100644
--- a/theories/Interp/TranslateFacts.v
+++ b/theories/Interp/TranslateFacts.v
@@ -1,8 +1,8 @@
 (** * Theorems about [Interp.translate] *)
 
 (* begin hide *)
-From ExtLib Require
-     Structures.Monoid.
+(* From ExtLib Require *)
+(*      Structures.Monoid. *)
 
 From ITree Require Import
      Basics.Basics
diff --git a/tutorial/Asm.v b/tutorial/Asm.v
index 2522b92c..3c94be23 100644
--- a/tutorial/Asm.v
+++ b/tutorial/Asm.v
@@ -13,21 +13,19 @@ From Coq Require Import
      Setoid
      RelationClasses.
 
-Require Import ExtLib.Structures.Monad.
-
-  (* SAZ: Should we add ITreeMonad to ITree? *)
 From ITree Require Import
      ITree
      ITreeFacts
      ITreeMonad
      Basics.Monad
+     Basics.MonadEither
+     Basics.MonadState
      Basics.CategorySub
      Events.State
      Events.StateFacts.
 
 Require Import Fin Utils_tutorial.
 
-Import Monads.
 (* end hide *)
 
 (** ** Syntax *)
@@ -61,6 +59,7 @@ Variant instr : Set :=
 Variant branch {label : Type} : Type :=
 | Bjmp (_ : label)                (* jump to label *)
 | Bbrz (_ : reg) (yes no : label) (* conditional jump *)
+| Bret (_: reg)
 | Bhalt
 .
 Global Arguments branch _ : clear implicits.
@@ -73,8 +72,6 @@ Inductive block {label : Type} : Type :=
 | bbb (_ : branch label).
 Global Arguments block _ : clear implicits.
 
-
-
 (** A piece of code should expose the set of labels allowing to enter into it,
     as well as the set of outer labels it might jump to.  To this end, [bks]
     represents a collection of blocks labeled by [F A], with branches in [F B].
@@ -123,7 +120,6 @@ Inductive Memory : Type -> Type :=
 | Load  (a : addr) : Memory value
 | Store (a : addr) (val : value) : Memory unit.
 
-
 (* SAZ: Move Exit to the itrees library? *)
 (** We also introduce a special event to model termination of the computation.
     Note that it expects _actively_ no answer from the environment: [Done] is
@@ -136,18 +132,19 @@ Inductive Exit : Type -> Type :=
 Definition exit {E A} `{Exit -< E} : itree E A :=
   vis Done (fun v => match v : void with end).
 
+(* TO MOVE *)
+(* Instance trigger' {E F: Type -> Type} `{E -< F} : Triggerable (eitherT value (itree F)) E := *)
+  (* fun _ e => Vis (subevent _ e) (fun x => ret (inr x)). *)
 
 Section Denote.
 
   (** Once again, [asm] programs shall be denoted as [itree]s. *)
 
   (* begin hide *)
-  Import ExtLib.Structures.Monad.
   Import MonadNotation.
   Local Open Scope monad_scope.
   (* end hide *)
 
-
   Section with_event.
 
     (** As with _Imp_, we parameterize our semantics by a universe of events
@@ -165,6 +162,7 @@ Section Denote.
       end.
 
     (** Instructions offer no suprises either. *)
+    Print Instances Monad.
     Definition denote_instr (i : instr) : itree E unit :=
       match i with
       | Imov d s =>
@@ -190,26 +188,34 @@ Section Denote.
         trigger (Store addr val)
       end.
 
+    Definition returns {B} r: eitherT value (itree E) B := val <- trigger (GetReg r);; ret (inl val).
+
+    Notation tree_ret := (eitherT value (itree E)).
+
+    (* TO MOVE *)
+    Definition lift {m T} `{Monad m} {V} (c: m T): eitherT V m T :=
+      bind c (fun x => ret (inr x)).
+
     (** A [branch] returns the computed label whose set of possible values [B]
         is carried by the type of the branch.  If the computation halts
         instead of branching, we return the [exit] tree.  *)
-    Definition denote_br {B} (b : branch B) : itree E B :=
+    Definition denote_br {B} (b : branch B) : tree_ret B :=
       match b with
       | Bjmp l => ret l
       | Bbrz v y n =>
         val <- trigger (GetReg v) ;;
-        if val:nat then ret y else ret n
+        if val:nat then ret (inr y) else ret (inr n)
+      | Bret r => returns r
       | Bhalt => exit
       end.
 
-
     (** The denotation of a basic [block] shares the same type, returning the
         [label] of the next [block] it shall jump to.  It recursively denote
         its instruction before that.  *)
-    Fixpoint denote_bk {B} (b : block B) : itree E B :=
+    Fixpoint denote_bk {B} (b : block B) : tree_ret B :=
       match b with
       | bbi i b =>
-        denote_instr i ;; denote_bk b
+        lift (denote_instr i) ;; denote_bk b
       | bbb b =>
         denote_br b
       end.
@@ -225,10 +231,10 @@ Section Denote.
         They have a nice algebraic structure, supported by the library,
         including a [loop] combinator that we can use to link collections of
         basic blocks. (See below.) *)
-    Definition denote_bks {A B : nat} (bs: bks A B): sub (ktree E) fin A B :=
+    Definition denote_bks {A B : nat} (bs: bks A B): sub (Kleisli tree_ret) fin A B :=
       fun a => denote_bk (bs a).
 
-  (** One can think of an [asm] program as a circuit/diagram where wires
+    (** One can think of an [asm] program as a circuit/diagram where wires
       correspond to jumps/program links.  [denote_bks] computes the meaning of
       each basic block as an [itree] that returns the label of the next block to
       jump to, laying down all our elementary wires.  In order to denote an [asm
@@ -238,7 +244,7 @@ Section Denote.
       accomplish this with the same [loop] combinator we used to denote _Imp_'s
       [while] loop.  It directly takes our [denote_bks (code s): ktree E (I + A)
       (I + B)] and hides [I] as desired.  *)
-    Definition denote_asm {A B} : asm A B -> sub (ktree E) fin A B :=
+    Definition denote_asm {A B} : asm A B -> sub (Kleisli tree_ret) fin A B :=
       fun s => loop (denote_bks (code s)).
 
   End with_event.
@@ -300,19 +306,53 @@ Definition h_memory {E : Type -> Type} `{mapE addr 0 -< E} :
 Definition registers := alist reg value.
 Definition memory    := alist addr value.
 
+(* Definition eitherT_stateT_commute {S A M R}: *)
+(*   (stateT S (eitherT A M) R) -> (eitherT A (stateT S M) R). *)
+(* intros ?. *)
 
+(* From ITree Require Import Interp.InterpEither. *)
 (** The _asm_ interpreter takes as inputs a starting heap [mem] and register
     state [reg] and interprets an itree in two nested instances of the [map]
     variant of the state monad. To get this type to work out, we have to
     do a bit of post-processing to swap the order of the "state components"
     introduced by the interpretation.
-*)
+ *)
+(* Should [eitherT] be on top of [itree E] or on the outside? *)
+
+(*
+
+Definition distribute {A B C: Type}: A * (B + C) -> A * B + A * C :=
+  fun '(a,bc) => match bc with
+              | inl b => inl (a,b)
+              | inr c => inr (a,c)
+              end.
+
+Definition interp_either_map {E K V Exc d map} `{M : Map K V map} :
+  eitherT Exc (itree (@mapE K V d +' E)) ~>
+          stateT map (eitherT (map * Exc) (itree E)) :=
+  fun T t s =>
+    let '(mkEitherT t') :=
+         interp_either' (M := stateT _ _) (case_ (@handle_map K V _ _ E d) pure_state) _ t in
+    mkEitherT (ITree.map distribute (t' s)).
+
+(*
+Definition MAS {m: Type -> Type} (S: Type) (Exc: Type): Type -> Type :=
+    fun (A: Type) => m ((Exc * S) + (A * S)).
+ *)
+
+Definition interp_asm {E A}
+           (t : eitherT value (itree (Reg +' Memory +' E)) A) :
+  stateT registers (stateT memory (eitherT (memory * (registers * value)) (itree E))) A :=
+  let h := bimap h_reg (bimap h_memory (id_ E)) in
+  let t' := interp_either' h _ t in
+  fun mem regs => interp_either_map _ (interp_either_map _ t' mem) regs.
+ *)
+
 Definition interp_asm {E A} (t : itree (Reg +' Memory +' E) A) :
-  memory -> registers -> itree E (memory * (registers * A)) :=
+  stateT registers (stateT memory (itree E)) A :=
   let h := bimap h_reg (bimap h_memory (id_ _)) in
   let t' := interp h t in
-  fun  mem regs => interp_map (interp_map t' regs) mem.
-
+  fun mem regs => interp_map (interp_map t' mem) regs.
 
 (** We can then define an evaluator for closed assembly programs by interpreting
     both store and heap events into two instances of [mapE], and running them
@@ -322,10 +362,11 @@ Definition run_asm (p: asm 1 0) := interp_asm (denote_asm p Fin.f0) empty empty.
 (* SAZ: Should some of thes notions of equivalence be put into the library?
    SAZ: Should this be stated in terms of ktree ?
  *)
+
 (** The definition [interp_asm] also induces a notion of equivalence (open)
     _asm_ programs, which is just the equivalence of the ktree category *)
-Definition eq_asm_denotations {E A B} (t1 t2 : Kleisli (itree (Reg +' Memory +' E)) A B) : Prop :=
-  forall a mem regs, interp_asm (t1 a) mem regs ≈ interp_asm (t2 a) mem regs.
+Definition eq_asm_denotations {E A B} (t1 t2 : Kleisli (eitherT value (itree (Reg +' Memory +' E))) A B) : Prop :=
+  forall  (a: A), eqm (interp_asm (t1 a)) (interp_asm (t2 a)).
 
 Definition eq_asm {A B} (p1 p2 : asm A B) : Prop :=
   eq_asm_denotations (denote_asm p1) (denote_asm p2).
@@ -336,35 +377,32 @@ Section InterpAsmProperties.
   Notation E := (Reg +' Memory +' E').
 
   (** This interpreter is compatible with the equivalence-up-to-tau. *)
-  Global Instance eutt_interp_asm {R}:
-    Proper (@eutt E R R eq ==> eq ==> eq ==> @eutt E' (prod memory (prod registers R)) (prod _ (prod _ R)) eq) interp_asm.
-  Proof.
-    repeat intro.
-    unfold interp_asm.
-    unfold interp_map.
-    rewrite H0.
-    rewrite H.
-    rewrite H1.
-    reflexivity.
-  Qed.
+  (* Global Instance eutt_interp_asm {R}: *)
+  (*   Proper (@eutt E R R eq ==> eq ==> eq ==> @eutt E' (prod memory (prod registers R)) (prod _ (prod _ R)) eq) interp_asm. *)
+  (* Proof. *)
+  (*   repeat intro. *)
+  (*   unfold interp_asm. *)
+  (*   unfold interp_map. *)
+  (*   rewrite H0. *)
+  (*   rewrite H. *)
+  (*   rewrite H1. *)
+  (*   reflexivity. *)
+  (* Qed. *)
 
   (** [interp_asm] commutes with [Ret]. *)
-  Lemma interp_asm_ret: forall {R} (r: R) (regs : registers) (mem: memory),
-      @eutt E' _ _ eq (interp_asm (ret r) mem regs)
-            (ret (mem, (regs, r))).
+  Lemma interp_asm_ret: forall {R} (r: R),
+      eqm (interp_asm (E := E') (ret r)) (ret r).
   Proof.
-    unfold interp_asm, interp_map.
-    intros.
-    unfold ret at 1, Monad_itree.
+    intros R r regs mem.
+    unfold interp_asm, interp_map. cbn.
     rewrite interp_ret, 2 interp_state_ret.
     reflexivity.
   Qed.
 
   (** [interp_asm] commutes with [bind]. *)
-  Lemma interp_asm_bind: forall {R S} (t: itree E R) (k: R -> itree _ S) (regs : registers) (mem: memory),
-      @eutt E' _ _ eq (interp_asm (ITree.bind t k) mem regs)
+  Lemma interp_asm_bind: forall {R S} (t: eitherT value (itree E) R) (k: R -> eitherT value (itree _) S) mem regs,
+      @eutt E' _ _ eq (interp_asm (bind t k) mem regs)
             (ITree.bind (interp_asm t mem regs) (fun '(mem', (regs', x)) => interp_asm (k x) mem' regs')).
-
   Proof.
     intros.
     unfold interp_asm.
diff --git a/tutorial/Fin.v b/tutorial/Fin.v
index 6132615c..433eb3c5 100644
--- a/tutorial/Fin.v
+++ b/tutorial/Fin.v
@@ -22,7 +22,12 @@ From ITree Require Import
      ITree
      ITreeFacts
      Basics.Category
-     Basics.CategorySub.
+     Basics.CategorySub
+     Basics.MonadEither
+     Basics.Monad.
+From ExtLib Require Import
+     EitherMonad.
+
 (* end hide *)
 
 (* Type with [n] inhabitants. *)
@@ -60,7 +65,17 @@ Proof.
   contradiction.
 Qed.
 
-Instance FinInitial {E} : Initial (sub (ktree E) fin) 0 := fun _ => fin_0.
+Section WithMonad.
+
+Variable M: Type -> Type.
+Context {EQM : EqM M}.
+Context {HM: Monad M}.
+Context {HEQP: @EqMProps M _ EQM}.
+Context {ML: @MonadLaws M _ HM}.
+
+Notation ktree := (Kleisli M).
+
+Global Instance FinInitial : Initial (sub ktree fin) 0 := fun _ => fin_0.
 
 Lemma split_fin_helper:
   forall n m x : nat, x < n + m -> ~ x < n -> x - n < m.
@@ -82,7 +97,7 @@ Defined.
 Program Definition L {n} (m : nat) (a : fin n) : fin (n + m) := _.
 Next Obligation.
   destruct a.
-  exists x. apply PeanoNat.Nat.lt_lt_add_r.  assumption.
+  exists x. apply PeanoNat.Nat.lt_lt_add_r. assumption.
 Defined.
 
 Program Definition R {m} (n:nat) (a:fin m) : fin (n + m) := _.
@@ -187,30 +202,30 @@ Proof.
     try contradiction + exfalso; lia.
 Qed.
 
-Instance ToBifunctor_ktree_fin {E} : ToBifunctor (ktree E) fin sum Nat.add :=
-  fun n m y => Ret (split_fin_sum n m y).
+Global Instance ToBifunctor_ktree_fin  : ToBifunctor ktree fin sum Nat.add :=
+  fun n m y => ret (split_fin_sum n m y).
 
-Instance FromBifunctor_ktree_fin {E} : FromBifunctor (ktree E) fin sum Nat.add :=
-  fun n m y => Ret (merge_fin_sum n m y).
+Global Instance FromBifunctor_ktree_fin : FromBifunctor ktree fin sum Nat.add :=
+  fun n m y => ret (merge_fin_sum n m y).
 
-Instance IsoBif_ktree_fin {E}
-  : forall a b, Iso (ktree E) (a := fin (Nat.add a b)) to_bif from_bif.
+Global Instance IsoBif_ktree_fin
+  : forall a b, Iso ktree (a := fin (Nat.add a b)) to_bif from_bif.
 Proof.
   unfold to_bif, ToBifunctor_ktree_fin, from_bif, FromBifunctor_ktree_fin.
   constructor; intros x.
   - unfold cat, Cat_sub, Cat_Kleisli. cbn. rewrite bind_ret_l.
-    apply eqit_Ret, merge_split.
+    rewrite merge_split; reflexivity.
   - unfold cat, Cat_sub, Cat_Kleisli. cbn. rewrite bind_ret_l.
-    apply eqit_Ret, split_merge.
+    rewrite split_merge; reflexivity.
 Qed.
 
-Instance ToBifunctor_Fun_fin : ToBifunctor Fun fin sum Nat.add :=
+Global Instance ToBifunctor_Fun_fin : ToBifunctor Fun fin sum Nat.add :=
   fun n m y => split_fin_sum n m y.
 
-Instance FromBifunctor_Fun_fin : FromBifunctor Fun fin sum Nat.add :=
+Global Instance FromBifunctor_Fun_fin : FromBifunctor Fun fin sum Nat.add :=
   fun n m y => merge_fin_sum n m y.
 
-Instance IsoBif_Fun_fin
+Global Instance IsoBif_Fun_fin
   : forall a b, Iso Fun (a := fin (Nat.add a b)) to_bif from_bif.
 Proof.
   constructor; intros x.
@@ -218,7 +233,9 @@ Proof.
   - apply split_merge.
 Qed.
 
-Instance InitialObject_ktree_fin {E} : InitialObject (sub (ktree E) fin) 0.
+Global Instance InitialObject_ktree_fin : InitialObject (sub ktree fin) 0.
 Proof.
   intros n f x; apply fin_0; auto.
 Qed.
+
+End WithMonad.