diff --git a/README.md b/README.md
index 44b61829..abd1e9ee 100644
--- a/README.md
+++ b/README.md
@@ -94,7 +94,8 @@ This library has been applied to other formalizations:
 ## Files
 
 - [monae_lib.v](./monae_lib.v): simple additions to base libraries
-- [hierarchy.v](./hierarchy.v): hierarchy of monadic effects
+- [hierarchy.v](./hierarchy.v): hierarchy of monadic effects (part 1/2)
+- [proba_hierarchy.v](./proba_hierarchy.v): hierarchy of monadic effects (part 2/2)
 - [monad_lib.v](./monad_lib.v): basic lemmas about monads
 - [category.v](./category.v): formalization of categories (generalization of ~hierarchy.v~)
 - [fail_lib.v](./fail_lib.v): lemmas about fail monad and related monads
diff --git a/_CoqProject b/_CoqProject
index 562c7daf..dcae8af3 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -7,6 +7,7 @@
 
 monae_lib.v
 hierarchy.v
+proba_hierarchy.v
 monad_lib.v
 fail_lib.v
 state_lib.v
diff --git a/altprob_model.v b/altprob_model.v
index 24e94a2b..b78568f3 100644
--- a/altprob_model.v
+++ b/altprob_model.v
@@ -7,8 +7,8 @@ From infotheo Require Import classical_sets_ext Reals_ext Rbigop ssrR fdist.
 From infotheo Require Import fsdist convex necset.
 Require category.
 From HB Require Import structures.
-Require Import monae_lib hierarchy monad_lib proba_lib monad_model gcm_model.
-Require Import category.
+Require Import monae_lib hierarchy monad_model proba_hierarchy monad_lib.
+Require Import proba_lib gcm_model category.
 
 (******************************************************************************)
 (*                  Model of the monad type altProbMonad                      *)
diff --git a/example_array.v b/example_array.v
index 5d75b7f2..9518f064 100644
--- a/example_array.v
+++ b/example_array.v
@@ -3,7 +3,6 @@
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require boolp.
 Require Import monae_lib hierarchy monad_lib fail_lib state_lib.
-From infotheo Require Import ssr_ext.
 
 (*******************************************************************************)
 (*                                   wip                                       *)
@@ -16,7 +15,6 @@ Unset Printing Implicit Defensive.
 Local Open Scope order_scope.
 Import Order.TTheory.
 Local Open Scope monae_scope.
-Local Open Scope tuple_ext_scope.
 
 From infotheo Require Import ssrZ.
 Require Import ZArith.
diff --git a/example_monty.v b/example_monty.v
index ce474c6f..2e9b18ea 100644
--- a/example_monty.v
+++ b/example_monty.v
@@ -3,7 +3,7 @@
 Require Import Reals Lra.
 From mathcomp Require Import all_ssreflect.
 From infotheo Require Import ssrR Reals_ext proba.
-Require Import monae_lib hierarchy monad_lib fail_lib proba_lib.
+Require Import monae_lib hierarchy proba_hierarchy monad_lib fail_lib proba_lib.
 
 (******************************************************************************)
 (*                            Monty Hall example                              *)
diff --git a/example_relabeling.v b/example_relabeling.v
index 5f44c639..3f379995 100644
--- a/example_relabeling.v
+++ b/example_relabeling.v
@@ -3,7 +3,6 @@
 Require Import ZArith.
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require boolp.
-From infotheo Require Import ssrZ.
 Require Import monae_lib hierarchy monad_lib fail_lib state_lib.
 
 (******************************************************************************)
diff --git a/gcm_model.v b/gcm_model.v
index 79559be1..10b12ad9 100644
--- a/gcm_model.v
+++ b/gcm_model.v
@@ -4,7 +4,7 @@ Require Import Reals.
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require Import boolp classical_sets.
 From mathcomp Require Import finmap.
-From infotheo Require Import Reals_ext classical_sets_ext Rbigop ssrR ssr_ext.
+From infotheo Require Import Reals_ext Rbigop ssrR.
 From infotheo Require Import fdist fsdist convex necset.
 Require Import monae_lib.
 From HB Require Import structures.
@@ -621,7 +621,7 @@ End P_delta_functor.
 
 (* TODO: move *)
 Require monad_lib.
-Require Import hierarchy.
+Require Import hierarchy proba_hierarchy.
 
 Section P_delta_category_monad.
 Import category.
diff --git a/hierarchy.v b/hierarchy.v
index a428965c..7ef4d400 100644
--- a/hierarchy.v
+++ b/hierarchy.v
@@ -2,15 +2,14 @@
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 Ltac typeof X := type of X.
 
-Require Import ssrmatching Reals.
+Require Import ssrmatching.
 From mathcomp Require Import all_ssreflect.
-From mathcomp Require boolp.
-From infotheo Require Import Reals_ext.
 Require Import monae_lib.
 From HB Require Import structures.
 
 (******************************************************************************)
 (*        A formalization of monadic effects over the category Set            *)
+(*       (part 1/2, see proba_hierarchy.v for the probability monads)         *)
 (*                                                                            *)
 (* We consider the type Type of Coq as the category Set and define functors   *)
 (* and a hierarchy of monads on top of functors. These monads are used to     *)
@@ -70,13 +69,6 @@ From HB Require Import structures.
 (*       stateTraceMonad == state + trace                                     *)
 (*  stateTraceReifyMonad == stateTrace + reify                                *)
 (*                                                                            *)
-(* Probability monads:                                                        *)
-(*         probaMonad == probabilistic choice and bind left-distributes over  *)
-(*                       choice                                               *)
-(*        probDrMonad == probaMonad + bind right-distributes over choice      *)
-(*       altProbMonad == combined (probabilistic and nondeterministic) choice *)
-(*    exceptProbMonad == exceptions + probabilistic choice                    *)
-(*                                                                            *)
 (* Freshness monads:                                                          *)
 (*         freshMonad == monad with freshness                                 *)
 (*     failFreshMonad == freshMonad + failure                                 *)
@@ -105,7 +97,6 @@ Reserved Notation "f (o) g" (at level 11).
 Reserved Notation "m >> f" (at level 49).
 Reserved Notation "'fmap' f" (at level 4).
 Reserved Notation "x '[~]' y" (at level 50).
-Reserved Notation "mx <| p |> my" (format "mx  <| p |>  my", at level 49).
 
 Notation "f ~~> g" := (forall A, f A -> g A)
   (at level 51, only parsing) : monae_scope.
@@ -163,6 +154,7 @@ Qed.
 HB.instance Definition _ :=
   isFunctor.Build (f \o g) functorcomposition_id functorcomposition_comp.
 
+(* TODO: consider eliminating *)
 Definition FComp := [the functor of f \o g].
 End functorcomposition.
 
@@ -1039,70 +1031,6 @@ HB.structure Definition MonadStateTraceReify (S T : UU0) :=
          isMonadReify S M & isMonadStateTrace S T M }.
 Notation stateTraceReifyMonad := MonadStateTraceReify.type.
 
-Local Open Scope reals_ext_scope.
-HB.mixin Record isMonadProb (M : UU0 -> UU0) of Monad M := {
-  choice : forall (p : prob) (T : UU0), M T -> M T -> M T ;
-  (* identity axioms *)
-  choice0 : forall (T : UU0) (a b : M T), choice 0%:pr _ a b = b ;
-  choice1 : forall (T : UU0) (a b : M T), choice 1%:pr _ a b = a ;
-  (* skewed commutativity *)
-  choiceC : forall (T : UU0) p (a b : M T), choice p _ a b = choice (p.~ %:pr) _ b a ;
-  choicemm : forall (T : UU0) p, idempotent (@choice p T) ;
-  (* quasi associativity *)
-  choiceA : forall (T : UU0) (p q r s : prob) (a b c : M T),
-    (p = r * s :> R /\ s.~ = p.~ * q.~)%R ->
-    (*NB: needed to preserve the notation in the resulting choiceA lemma, report? *)
-    let bc := choice q _ b c in
-    let ab := choice r _ a b in
-    choice p _ a bc = choice s _ ab c;
-  (* composition distributes leftwards over [probabilistic] choice *)
-  prob_bindDl : forall p, BindLaws.left_distributive (@bind [the monad of M]) (choice p)
-}.
-
-HB.structure Definition MonadProb := {M of isMonadProb M & }.
-Notation "a <| p |> b" := (choice p _ a b).
-Notation probMonad := MonadProb.type.
-Arguments choiceA {_} {_} _ _ _ _ {_} {_} {_}.
-Arguments choiceC {_} {_} _ _ _.
-Arguments choicemm {_} {_} _.
-
-HB.mixin Record isMonadProbDr (M : UU0 -> UU0) of MonadProb M := {
-  (* composition distributes rightwards over [probabilistic] choice *)
-  (* WARNING: this should not be asserted as an axiom in conjunction with
-     distributivity of <||> over [] *)
-  prob_bindDr : forall p, BindLaws.right_distributive (@bind [the monad of M]) (choice p) (* NB: not used *)
-}.
-
-HB.structure Definition MonadProbDr := {M of isMonadProbDr M & }.
-Notation probDrMonad := MonadProbDr.type.
-
-HB.mixin Record isMonadAltProb (M : UU0 -> UU0) of MonadAltCI M & MonadProb M := {
-  choiceDr : forall T p,
-    right_distributive (@choice [the probMonad of M] p T) (fun a b => a [~] b)
-}.
-HB.structure Definition MonadAltProb :=
-  { M of isMonadAltProb M & isFunctor M & isMonad M & isMonadAlt M &
-         isMonadAltCI M & isMonadProb M }.
-Notation altProbMonad := MonadAltProb.type.
-
-Section altprob_lemmas.
-Local Open Scope proba_monad_scope.
-Variable (M : altProbMonad).
-Lemma choiceDl A p :
-  left_distributive (fun x y : M A => x <| p |> y) (fun x y => x [~] y).
-Proof. by move=> x y z; rewrite !(choiceC p) choiceDr. Qed.
-End altprob_lemmas.
-
-HB.mixin Record isMonadExceptProb (M : UU0 -> UU0) of MonadExcept M & MonadProb M := {
-  catchDl : forall (A : UU0) w,
-    left_distributive (@catch [the exceptMonad of M] A) (fun x y => choice w A x y)
-}.
-
-HB.structure Definition MonadExceptProb :=
- { M of isMonadExceptProb M & isFunctor M & isMonad M & isMonadFail M &
-        isMonadExcept M & isMonadProb M }.
-Notation exceptProbMonad := MonadExceptProb.type.
-
 HB.mixin Record isMonadFresh (S : eqType) (M : UU0 -> UU0) of Monad M := {
   fresh : M S
 }.
diff --git a/impredicative_set/ihierarchy.v b/impredicative_set/ihierarchy.v
index a435c748..3bf1cb7a 100644
--- a/impredicative_set/ihierarchy.v
+++ b/impredicative_set/ihierarchy.v
@@ -9,6 +9,7 @@ From HB Require Import structures.
 
 (******************************************************************************)
 (*        A formalization of monadic effects over the category Set            *)
+(*       (part 1/2, see proba_hierarchy.v for the probability monads)         *)
 (*                                                                            *)
 (* We consider the type Type of Coq as the category Set and define functors   *)
 (* and a hierarchy of monads on top of functors. These monads are used to     *)
@@ -96,7 +97,6 @@ Reserved Notation "f (o) g" (at level 11).
 Reserved Notation "m >> f" (at level 49).
 Reserved Notation "'fmap' f" (at level 4).
 Reserved Notation "x '[~]' y" (at level 50).
-Reserved Notation "mx <| p |> my" (format "mx  <| p |>  my", at level 49).
 
 Notation "f ~~> g" := (forall A, f A -> g A)
   (at level 51, only parsing) : monae_scope.
diff --git a/meta.yml b/meta.yml
index d5e69197..dc194927 100644
--- a/meta.yml
+++ b/meta.yml
@@ -170,7 +170,8 @@ documentation: |-
   ## Files
 
   - [monae_lib.v](./monae_lib.v): simple additions to base libraries
-  - [hierarchy.v](./hierarchy.v): hierarchy of monadic effects
+  - [hierarchy.v](./hierarchy.v): hierarchy of monadic effects (part 1/2)
+  - [proba_hierarchy.v](./proba_hierarchy.v): hierarchy of monadic effects (part 2/2)
   - [monad_lib.v](./monad_lib.v): basic lemmas about monads
   - [category.v](./category.v): formalization of categories (generalization of ~hierarchy.v~)
   - [fail_lib.v](./fail_lib.v): lemmas about fail monad and related monads
diff --git a/proba_hierarchy.v b/proba_hierarchy.v
new file mode 100644
index 00000000..c28f1336
--- /dev/null
+++ b/proba_hierarchy.v
@@ -0,0 +1,108 @@
+(* monae: Monadic equational reasoning in Coq                                 *)
+(* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
+Ltac typeof X := type of X.
+
+Require Import ssrmatching Reals.
+From mathcomp Require Import all_ssreflect.
+From mathcomp Require boolp.
+From infotheo Require Import Reals_ext.
+Require Import monae_lib.
+From HB Require Import structures.
+Require Import hierarchy.
+
+(******************************************************************************)
+(*        A formalization of monadic effects over the category Set            *)
+(*               (part 2/2, see hierarchy.v for part 1/2)                     *)
+(*                                                                            *)
+(* Probability monads:                                                        *)
+(*         probaMonad == probabilistic choice and bind left-distributes over  *)
+(*                       choice                                               *)
+(*        probDrMonad == probaMonad + bind right-distributes over choice      *)
+(*       altProbMonad == combined (probabilistic and nondeterministic) choice *)
+(*    exceptProbMonad == exceptions + probabilistic choice                    *)
+(*                                                                            *)
+(* references:                                                                *)
+(* - R. Affeldt, D. Nowak, Extending Equational Monadic Reasoning with Monad  *)
+(* Transformers, https://arxiv.org/abs/2011.03463                             *)
+(* - R. Affeldt, D. Nowak, T. Saikawa, A Hierarchy of Monadic Effects for     *)
+(* Program Verification using Equational Reasoning, MPC 2019                  *)
+(* - J. Gibbons, R. Hinze, Just do it: simple monadic equational reasoning,   *)
+(* ICFP 2011                                                                  *)
+(* - J. Gibbons, Unifying Theories of Programming with Monads, UTP 2012       *)
+(******************************************************************************)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Declare Scope do_notation.
+Declare Scope mprog.
+Declare Scope monae_scope.
+Delimit Scope monae_scope with monae.
+Declare Scope proba_monad_scope.
+
+Reserved Notation "mx <| p |> my" (format "mx  <| p |>  my", at level 49).
+
+Local Open Scope reals_ext_scope.
+HB.mixin Record isMonadProb (M : UU0 -> UU0) of Monad M := {
+  choice : forall (p : prob) (T : UU0), M T -> M T -> M T ;
+  (* identity axioms *)
+  choice0 : forall (T : UU0) (a b : M T), choice 0%:pr _ a b = b ;
+  choice1 : forall (T : UU0) (a b : M T), choice 1%:pr _ a b = a ;
+  (* skewed commutativity *)
+  choiceC : forall (T : UU0) p (a b : M T), choice p _ a b = choice (p.~ %:pr) _ b a ;
+  choicemm : forall (T : UU0) p, idempotent (@choice p T) ;
+  (* quasi associativity *)
+  choiceA : forall (T : UU0) (p q r s : prob) (a b c : M T),
+    (p = r * s :> R /\ s.~ = p.~ * q.~)%R ->
+    (*NB: needed to preserve the notation in the resulting choiceA lemma, report? *)
+    let bc := choice q _ b c in
+    let ab := choice r _ a b in
+    choice p _ a bc = choice s _ ab c;
+  (* composition distributes leftwards over [probabilistic] choice *)
+  prob_bindDl : forall p, BindLaws.left_distributive (@bind [the monad of M]) (choice p)
+}.
+
+HB.structure Definition MonadProb := {M of isMonadProb M & }.
+Notation "a <| p |> b" := (choice p _ a b).
+Notation probMonad := MonadProb.type.
+Arguments choiceA {_} {_} _ _ _ _ {_} {_} {_}.
+Arguments choiceC {_} {_} _ _ _.
+Arguments choicemm {_} {_} _.
+
+HB.mixin Record isMonadProbDr (M : UU0 -> UU0) of MonadProb M := {
+  (* composition distributes rightwards over [probabilistic] choice *)
+  (* WARNING: this should not be asserted as an axiom in conjunction with
+     distributivity of <||> over [] *)
+  prob_bindDr : forall p, BindLaws.right_distributive (@bind [the monad of M]) (choice p) (* NB: not used *)
+}.
+
+HB.structure Definition MonadProbDr := {M of isMonadProbDr M & }.
+Notation probDrMonad := MonadProbDr.type.
+
+HB.mixin Record isMonadAltProb (M : UU0 -> UU0) of MonadAltCI M & MonadProb M := {
+  choiceDr : forall T p,
+    right_distributive (@choice [the probMonad of M] p T) (fun a b => a [~] b)
+}.
+HB.structure Definition MonadAltProb :=
+  { M of isMonadAltProb M & isFunctor M & isMonad M & isMonadAlt M &
+         isMonadAltCI M & isMonadProb M }.
+Notation altProbMonad := MonadAltProb.type.
+
+Section altprob_lemmas.
+Local Open Scope proba_monad_scope.
+Variable (M : altProbMonad).
+Lemma choiceDl A p :
+  left_distributive (fun x y : M A => x <| p |> y) (fun x y => x [~] y).
+Proof. by move=> x y z; rewrite !(choiceC p) choiceDr. Qed.
+End altprob_lemmas.
+
+HB.mixin Record isMonadExceptProb (M : UU0 -> UU0) of MonadExcept M & MonadProb M := {
+  catchDl : forall (A : UU0) w,
+    left_distributive (@catch [the exceptMonad of M] A) (fun x y => choice w A x y)
+}.
+
+HB.structure Definition MonadExceptProb :=
+ { M of isMonadExceptProb M & isFunctor M & isMonad M & isMonadFail M &
+        isMonadExcept M & isMonadProb M }.
+Notation exceptProbMonad := MonadExceptProb.type.
diff --git a/proba_lib.v b/proba_lib.v
index 5c46e470..883752eb 100644
--- a/proba_lib.v
+++ b/proba_lib.v
@@ -5,7 +5,7 @@ From mathcomp Require Import all_ssreflect.
 From mathcomp Require boolp Rstruct.
 From infotheo Require Import ssrR Reals_ext proba.
 From infotheo Require convex necset.
-Require Import monae_lib hierarchy monad_lib fail_lib.
+Require Import monae_lib hierarchy proba_hierarchy monad_lib fail_lib.
 
 (******************************************************************************)
 (*             Definitions and lemmas for probability monads                  *)
diff --git a/proba_monad_model.v b/proba_monad_model.v
index 9fbc6e1e..80c2650e 100644
--- a/proba_monad_model.v
+++ b/proba_monad_model.v
@@ -3,13 +3,15 @@
 Require Import Reals.
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require boolp.
-From infotheo Require Import Reals_ext ssr_ext fsdist.
+From infotheo Require Import Reals_ext fsdist.
 From infotheo Require Import convex.
 From HB Require Import structures.
-Require Import monae_lib hierarchy monad_lib proba_lib.
+Require Import monae_lib hierarchy proba_hierarchy monad_lib proba_lib.
 
 (******************************************************************************)
 (*                     Model for the probability monad                        *)
+(*                                                                            *)
+(* Module MonadProbModel == probMonad using fsdist from infotheo              *)
 (******************************************************************************)
 
 Local Open Scope monae_scope.
@@ -74,7 +76,8 @@ Let choice0 : forall (T : UU0) (a b : acto T), choice 0%:pr _ a b = b.
 Proof. by move=> ? ? ?; exact: ConvFSDist.conv0. Qed.
 Let choice1 : forall (T : UU0) (a b : acto T), choice 1%:pr _ a b = a.
 Proof. by move=> ? ? ?; exact: ConvFSDist.conv1. Qed.
-Let choiceC : forall (T : UU0) p (a b : acto T), choice p _ a b = choice (p.~ %:pr) _ b a.
+Let choiceC : forall (T : UU0) p (a b : acto T),
+  choice p _ a b = choice (p.~ %:pr) _ b a.
 Proof. by move=> ? ? ?; exact: ConvFSDist.convC. Qed.
 Let choicemm : forall (T : Type) p, idempotent (@choice p T).
 Proof. by move=> ? ? ?; exact: ConvFSDist.convmm. Qed.
@@ -84,7 +87,8 @@ Let choiceA : forall (T : Type) (p q r s : prob) (a b c : acto T),
     let ab := (choice r _ a b) in
     choice p _ a bc = choice s _ ab c.
 Proof. by move=> ? ? ? ? ? ? ? ? ? /=; exact: ConvFSDist.convA. Qed.
-Let prob_bindDl p : BindLaws.left_distributive (@hierarchy.bind [the monad of acto]) (choice p).
+Let prob_bindDl p :
+  BindLaws.left_distributive (@hierarchy.bind [the monad of acto]) (choice p).
 Proof.
 move=> A B m1 m2 k.
 rewrite !(@BindE (choice_of_Type A) (choice_of_Type B)).
diff --git a/state_lib.v b/state_lib.v
index 33f033d1..1db3d159 100644
--- a/state_lib.v
+++ b/state_lib.v
@@ -3,7 +3,6 @@
 Require Import ZArith.
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require boolp.
-From infotheo Require Import ssrZ.
 Require Import monae_lib.
 From HB Require Import structures.
 Require Import hierarchy monad_lib fail_lib.