diff --git a/theories/applications/monad_composition.v b/theories/applications/monad_composition.v
index aae9c0c5..3d876d7b 100644
--- a/theories/applications/monad_composition.v
+++ b/theories/applications/monad_composition.v
@@ -388,7 +388,5 @@ have @join : [the functor of (T \o S) \o (T \o S)] ~> [the functor of T \o S].
   apply: HComp.
     exact: f.
   exact: NId.
-apply: (Monad.Pack (Monad.Class (isMonad.Axioms_ (CRet T S) join _ _ _ _ _))).
-move=> A.
-rewrite /join.
+(* construct monad using (CRet T S) and join... *)
 Abort.
diff --git a/theories/core/hierarchy.v b/theories/core/hierarchy.v
index 55001325..6a5c6ecc 100644
--- a/theories/core/hierarchy.v
+++ b/theories/core/hierarchy.v
@@ -29,13 +29,17 @@ From HB Require Import structures.
 (*   naturality F G f == the components f form a natural transformation       *)
 (*                       F ~> G                                               *)
 (*    Module JoinLaws == join laws of a monad                                 *)
-(*            isMonad == mixin of monad                                       *)
+(*    Module BindLaws == bind laws of a monad                                 *)
+(*    Functor_isMonad == mixin of monad; has both ret, join and bind laws     *)
+(*            isMonad == compat. factory; = Functor_isMonad - bind laws       *)
+(*   isMonad_ret_join == factory on ret and join                              *)
+(*   isMonad_ret_bind == factory on ret and bind; no need of functoriarity    *)
+(*                       (i.e., the extension system)                         *)
 (*                >>= == notation for the standard bind operator              *)
 (*             m >> f := m >>= (fun _ => f)                                   *)
 (*              monad == type of monads                                       *)
 (*                Ret == natural transformation idfun ~> M for a monad M      *)
 (*               Join == natural transformation M \o M ~> M for a monad M     *)
-(*    Module BindLaws == bind laws of a monad                                 *)
 (* ```                                                                        *)
 (*                                                                            *)
 (* Failure and nondeterministic monads:                                       *)
@@ -167,6 +171,26 @@ HB.structure Definition Functor := {F of isFunctor F}.
 Notation "F # g" := (@actm F _ _ g) : monae_scope.
 Notation "'fmap' f" := (_ # f) : mprog.
 
+Lemma functor_ext (F G : functor) :
+  forall (H : Functor.sort F = Functor.sort G),
+  @actm G =
+  eq_rect _ (fun m : UU0 -> UU0 => forall A B : UU0, (A -> B) -> m A -> m B)
+            (@actm F) _ H  ->
+  G = F.
+Proof.
+move: F G => [F [[HF1 HF2 HF3]]] [G [[HG1 HG2 HG3]]] /= H.
+subst F => /= H.
+congr (Functor.Pack (Functor.Class _)).
+have ? : HG1 = HF1.
+  rewrite /actm /= in H.
+  apply funext_dep => x.
+  apply funext_dep => y.
+  apply funext_dep => z.
+  by move/(congr1 (fun i => i x y z)) : H.
+subst HG1.
+congr (isFunctor.Axioms_ _); exact/proof_irr.
+Defined.
+
 Section functorid.
 Let id_actm (A B : UU0) (f : A -> B) : idfun A -> idfun B := f.
 Let id_id : FunctorLaws.id id_actm. Proof. by []. Qed.
@@ -185,6 +209,8 @@ Let comp_actm (A B : UU0) (h : A -> B) : (F \o G) A -> (F \o G) B :=
 Let comp_id : FunctorLaws.id comp_actm.
 Proof. by rewrite /FunctorLaws.id => A; rewrite /comp_actm 2!functor_id. Qed.
 
+(* TODO(bug): `rewrite !functor_o` leads to an infinite loop
+   (due to expansions of the form `f` = `f \o id`) *)
 Let comp_comp : FunctorLaws.comp comp_actm.
 Proof.
 rewrite /FunctorLaws.comp => A B C g' h; rewrite /comp_actm.
@@ -225,26 +251,6 @@ End fcomp.
 Notation "f (o) g" := (fcomp f g) : mprog.
 Arguments fcomp : simpl never.
 
-Lemma functor_ext (F G : functor) :
-  forall (H : Functor.sort F = Functor.sort G),
-  @actm G =
-  eq_rect _ (fun m : UU0 -> UU0 => forall A B : UU0, (A -> B) -> m A -> m B)
-            (@actm F) _ H  ->
-  G = F.
-Proof.
-move: F G => [F [[HF1 HF2 HF3]]] [G [[HG1 HG2 HG3]]] /= H.
-subst F => /= H.
-congr (Functor.Pack (Functor.Class _)).
-have ? : HG1 = HF1.
-  rewrite /actm /= in H.
-  apply funext_dep => x.
-  apply funext_dep => y.
-  apply funext_dep => z.
-  by move/(congr1 (fun i => i x y z)) : H.
-subst HG1.
-congr (isFunctor.Axioms_ _); exact/proof_irr.
-Defined.
-
 Definition naturality (F G : functor) (f : F ~~> G) :=
   forall (A B : UU0) (h : A -> B), (G # h) \o f A = f B \o (F # h).
 Arguments naturality : clear implicits.
@@ -321,41 +327,6 @@ Definition associativity := forall A,
 End join_laws.
 End JoinLaws.
 
-HB.mixin Record isMonad (F : UU0 -> UU0) of Functor F := {
-  ret : idfun ~> F ;
-  join : F \o F ~> F ;
-  bind : forall (A B : UU0), F A -> (A -> F B) -> F B ;
-  bindE : forall (A B : UU0) (f : A -> F B) (m : F A),
-    bind A B m f = join B ((F # f) m) ;
-  joinretM : JoinLaws.left_unit ret join ;
-  joinMret : JoinLaws.right_unit ret join ;
-  joinA : JoinLaws.associativity join }.
-
-#[short(type=monad)]
-HB.structure Definition Monad := {F of isMonad F &}.
-
-(* we introduce Ret as a way to make the second arguments of ret implicit,
-   o.w. Rocq won't let us *)
-Notation Ret := (@ret _ _).
-Notation Join := (@join _ _).
-Arguments bind {s A B} : simpl never.
-Notation "m >>= f" := (bind m f) : monae_scope.
-
-Lemma eq_bind (M : monad) (A B : UU0) (m : M A) (f1 f2 : A -> M B) :
-  f1 =1 f2 -> m >>= f1 = m >>= f2.
-Proof. by move=> f12; congr bind; apply boolp.funext. Qed.
-
-Section monad_lemmas.
-Variable M : monad.
-
-Lemma fmapE (A B : UU0) (f : A -> B) (m : M A) :
- (M # f) m = m >>= (ret B \o f).
-Proof.
-by rewrite bindE [in RHS]functor_o -[in RHS]compE compA joinMret.
-Qed.
-
-End monad_lemmas.
-
 Module BindLaws.
 Section bindlaws.
 Variable F : UU0 -> UU0.
@@ -394,40 +365,107 @@ Definition right_id (r : forall A, F A) (op : forall B, F B -> F B -> F B) :=
 End bindlaws.
 End BindLaws.
 
-Definition join_of_bind (F : functor)
-    (b : forall (A B : UU0), F A -> (A -> F B) -> F B) : F \o F ~~> F :=
-  fun A : UU0 => (b _ A)^~ id.
+HB.mixin Record Functor_isMonad (F : UU0 -> UU0) of Functor F := {
+  ret : idfun ~> F ;
+  join : F \o F ~> F ;
+  bind : forall (A B : UU0), F A -> (A -> F B) -> F B ;
+  bindE : forall (A B : UU0) (f : A -> F B) (m : F A),
+    bind A B m f = join B ((F # f) m) ;
+  joinretM : JoinLaws.left_unit ret join ;
+  joinMret : JoinLaws.right_unit ret join ;
+  joinA : JoinLaws.associativity join ;
+  bindretf : BindLaws.left_neutral bind ret ;
+  bindmret : BindLaws.right_neutral bind ret ;
+  bindA : BindLaws.associative bind ;
+}.
 
-Definition bind_of_join (F : functor) (j : F \o F ~~> F)
-    (A B : UU0) (m : F A) (f : A -> F B) : F B :=
-  j B ((F # f) m).
+#[short(type=monad)]
+HB.structure Definition Monad := {F of Functor_isMonad F &}.
+
+(* we introduce Ret as a way to make the second arguments of ret implicit,
+   o.w. Rocq won't let us *)
+Notation Ret := (@ret _ _).
+Notation Join := (@join _ _).
+Arguments bind {s A B} : simpl never.
+Notation "m >>= f" := (bind m f) : monae_scope.
+
+Arguments bindretf {s} [A B].
+Arguments bindmret {s} [A].
+Arguments bindA {s} [A B C].
 
-Section from_join_laws_to_bind_laws.
-Variable (F : functor) (ret : idfun ~> F) (join : F \o F ~> F).
+HB.factory Record isMonad (F : UU0 -> UU0) of Functor F := {
+  ret : idfun ~> F ;
+  join : F \o F ~> F ;
+  bind : forall (A B : UU0), F A -> (A -> F B) -> F B ;
+  bindE : forall (A B : UU0) (f : A -> F B) (m : F A),
+    bind A B m f = join B ((F # f) m) ;
+  joinretM : JoinLaws.left_unit ret join ;
+  joinMret : JoinLaws.right_unit ret join ;
+  joinA : JoinLaws.associativity join }.
+
+HB.builders Context M of isMonad M.
+
+Local Notation "m >>= f" := (bind m f).
+Notation Ret := (ret _).
 
-Hypothesis joinretM : JoinLaws.left_unit ret join.
-Hypothesis joinMret : JoinLaws.right_unit ret join.
-Hypothesis joinA : JoinLaws.associativity join.
+Lemma bindE_ext :
+  bind = fun (A B : UU0) (m : M A) (f : A -> M B) => join B ((M # f) m).
+Proof.
+do ! apply/funext_dep => ?.
+by rewrite bindE.
+Qed.
+
+Lemma fmapE (A B : UU0) (f : A -> B) (m : M A) :
+ (M # f) m = m >>= (ret B \o f).
+Proof. by rewrite bindE [in RHS]functor_o -[in RHS]compE compA joinMret. Qed.
 
-Lemma bindretf_derived : BindLaws.left_neutral (bind_of_join join) ret.
+Lemma bindretf : BindLaws.left_neutral bind ret.
 Proof.
-move=> A B a f; rewrite /bind_of_join -(compE (@join _)) -(compE _ (@ret _)).
+move=> A B a f.
+rewrite bindE -(compE (join _)) -(compE _ (ret _)).
 by rewrite -compA (natural ret) compA joinretM compidf.
 Qed.
 
-Lemma bindmret_derived : BindLaws.right_neutral (bind_of_join join) ret.
-Proof. by move=> A m; rewrite /bind_of_join -(compE (@join _)) joinMret. Qed.
+Lemma bindmret : BindLaws.right_neutral bind ret.
+Proof. by move=> A m; rewrite bindE -(compE (join _)) joinMret. Qed.
 
-Lemma bindA_derived : BindLaws.associative (bind_of_join join).
+Lemma bindA : BindLaws.associative bind.
 Proof.
-move=> A B C m f g; rewrite /bind_of_join.
-rewrite [LHS](_ : _ = ((@join _ \o (F # g \o @join _) \o F # f) m)) //.
-rewrite (natural join) (compA (@join C)) -joinA -(compE (@join _)).
-transitivity ((@join _ \o F # (@join _ \o (F # g \o f))) m) => //.
-by rewrite -2!compA functor_o FCompE -[in LHS](@functor_o F).
+move=> A B C m f g; rewrite !bindE_ext.
+rewrite [LHS](_ : _ = ((join _ \o (M # g \o join _) \o M # f) m)) //.
+rewrite (natural join) (compA (join C)) -joinA -(compE (join _)).
+transitivity ((join _ \o M # (join _ \o (M # g \o f))) m) => //.
+by rewrite -2!compA functor_o FCompE -[in LHS](@functor_o M).
 Qed.
 
-End from_join_laws_to_bind_laws.
+HB.instance Definition _ :=
+  Functor_isMonad.Build M
+    bindE joinretM joinMret joinA bindretf bindmret bindA.
+
+HB.end.
+
+Lemma eq_bind (M : monad) (A B : UU0) (m : M A) (f1 f2 : A -> M B) :
+  f1 =1 f2 -> m >>= f1 = m >>= f2.
+Proof. by move=> f12; congr bind; apply boolp.funext. Qed.
+
+Section monad_lemmas.
+Variable M : monad.
+
+Lemma fmapE (A B : UU0) (f : A -> B) (m : M A) :
+ (M # f) m = m >>= (ret B \o f).
+Proof.
+by rewrite bindE [in RHS]functor_o -[in RHS]compE compA joinMret.
+Qed.
+
+End monad_lemmas.
+
+Definition join_of_bind (F : functor)
+    (b : forall (A B : UU0), F A -> (A -> F B) -> F B) : F \o F ~~> F :=
+  fun A : UU0 => (b _ A)^~ id.
+
+Definition bind_of_join (F : functor) (j : F \o F ~~> F)
+    (A B : UU0) (m : F A) (f : A -> F B) : F B :=
+  j B ((F # f) m).
 
 HB.factory Record isMonad_ret_join (F : UU0 -> UU0) of isFunctor F := {
   ret : idfun ~> F ;
@@ -556,38 +594,6 @@ Qed.
 HB.instance Definition _ := isMonad.Build M bindE joinretM joinMret joinA.
 HB.end.
 
-Section monad_lemmas.
-Variable M : monad.
-
-Lemma bindretf : BindLaws.left_neutral (@bind M) ret.
-Proof.
-move: (@bindretf_derived M ret join joinretM).
-rewrite (_ : bind_of_join _ = @bind M) //.
-apply funext_dep => A; apply funext_dep => B.
-apply funext_dep => m; apply funext_dep => f.
-by rewrite bindE.
-Qed.
-
-Lemma bindmret : BindLaws.right_neutral (@bind M) ret.
-Proof.
-move: (@bindmret_derived M ret join joinMret).
-rewrite (_ : bind_of_join _ = @bind M) //.
-apply funext_dep => A; apply funext_dep => B.
-apply funext_dep => m; apply funext_dep => f.
-by rewrite bindE.
-Qed.
-
-Lemma bindA : BindLaws.associative (@bind M).
-Proof.
-move: (@bindA_derived M join joinA).
-rewrite (_ : bind_of_join _ = @bind M) //.
-apply funext_dep => A; apply funext_dep => B.
-apply funext_dep => m; apply funext_dep => f.
-by rewrite bindE.
-Qed.
-
-End monad_lemmas.
-
 Notation "'do' x <- m ; e" := (bind m (fun x => e)) (only parsing) : do_notation.
 Notation "'do' x : T <- m ; e" :=
   (bind m (fun x : T => e)) (only parsing) : do_notation.