diff --git a/README.md b/README.md
index bbdd1642..5e0ea505 100644
--- a/README.md
+++ b/README.md
@@ -94,36 +94,44 @@ This library has been applied to other formalizations:
 
 ## Files
 
-- basics:
-  + [monae_lib.v](./monae_lib.v): simple additions to base libraries
-  + [hierarchy.v](./hierarchy.v): hierarchy of monadic effects
-  + [category.v](./category.v): formalization of concrete categories (generalization of the bottom layers of `hierarchy.v`)
-  + [monad_transformer.v](./monad_transformer.v): monad transformers
+- core:
+  + [monae_lib.v](./theories/core/monae_lib.v): simple additions to base libraries
+  + [hierarchy.v](./theories/core/hierarchy.v): hierarchy of monadic effects
+  + [category.v](./theories/core/category.v): formalization of concrete categories (generalization of the bottom layers of `hierarchy.v`)
+  + [monad_transformer.v](./theories/core/monad_transformer.v): monad transformers
     * completed by `ifmt_lifting.v` and `iparametricty_codensity.v` in the directory `impredicative_set`
       - the directory `impredicative_set` contains a lighter version of Monae where monads live in `Set` and that compiles with `impredicative-set`
-- utility lemmas:  
-  + [monad_lib.v](./monad_lib.v): basic lemmas about monads
-  + [fail_lib.v](./fail_lib.v): lemmas about the fail monad and related monads
-  + [state_lib.v](./state_lib.v): lemmas about state-related monads
-  + [array_lib.v](./array_lib.v): lemmas about the array monad
-  + [trace_lib.v](./trace_lib.v): lemmas about about the state-trace monad
-  + [proba_lib.v](./proba_lib.v): lemmas about the probability monad
-  + [typed_store_lib.v](./typed_store_lib.v): derived definitions and lemmas about about the typed store monad
+- libraries for each monad theory:  
+  + [monad_lib.v](./theories/lib/monad_lib.v): basic lemmas about monads
+  + [fail_lib.v](./theories/lib/fail_lib.v): lemmas about the fail monad and related monads
+  + [state_lib.v](./theories/lib/state_lib.v): lemmas about state-related monads
+  + [array_lib.v](./theories/lib/array_lib.v): lemmas about the array monad
+  + [trace_lib.v](./theories/lib/trace_lib.v): lemmas about about the state-trace monad
+  + [proba_lib.v](./theories/lib/proba_lib.v): lemmas about the probability monad
+  + [typed_store_lib.v](./theories/lib/typed_store_lib.v): derived definitions and lemmas about about the typed store monad
 - models of monads:
-  + [monad_model.v](./monad_model.v): concrete models of monads
-  + [proba_monad_model.v](./proba_monad_model.v): model of the probability monad
-  + [gcm_model.v](./gcm_model.v): model of the geometrically convex monad
-  + [altprob_model.v](./altprob_model.v): model of a monad that mixes non-deterministic choice and probabilistic choice
-  + [typed_store_model.v](./typed_store_model.v): alternative model of the typed store monad
+  + [monad_model.v](./theories/models/monad_model.v): concrete models of monads
+  + [proba_monad_model.v](./theories/models//proba_monad_model.v): model of the probability monad
+  + [gcm_model.v](./theories/models//gcm_model.v): model of the geometrically convex monad
+  + [altprob_model.v](./theories/models//altprob_model.v): model of a monad that mixes non-deterministic choice and probabilistic choice
+  + [typed_store_model.v](./theories/models//typed_store_model.v): alternative model of the typed store monad
 - applications:
-  + [monad_composition.v](./monad_composition.v): composing monads
-  + [smallstep.v](./smallstep.v): semantics for an imperative language, with equivalence operational semantics/denotation and sample imperative programs
-  + example_*.v: various examples (Spark aggregation, the n-queens puzzle, tree relabeling,  Monty Hall problem, monad transformers, quicksort, OCaml programs, etc.)
-
-## About Installation with Windows 10 or 11
+  + [example_relabeling.v](./theories/applications/example_relabeling.v): tree relabeling
+  + [example_monty.v](./theories/applications/example_monty.v): Monty Hall problem
+  + [example_spark.v](./theories/applications/example_spark.v): Spark aggregation
+  + [example_iquicksort.v](./theories/applications/example_iquicksort.v): in-place quicksort
+  + [example_quicksort.v](./theories/applications/example_quicksort.v): functional quicksort
+  + [example_nqueens.v](./theories/applications/example_nqueens.v): the n-queens puzzle
+  + [example_typed_store.v](./theories/applications/example_typed_store.v): ML programs with references
+  + [example_transformer.v](./theories/applications/example_transformer.v): monad transformers
+  + [smallstep.v](./theories/applications/smallstep.v): semantics for an imperative language, with equivalence operational semantics/denotation and sample imperative programs
+  + [monad_composition.v](./theories/applications/monad_composition.v): composing monads
+  + [category_ext.v](./theories/applications/category_ext.v): experimental library about categories
+
+## About Installation with Windows 11
 
 Installation of monae on Windows is less simple.
-First install infotheo following the [instructions for Windows 10](https://github.com/affeldt-aist/infotheo).
+First install infotheo following the [instructions for Windows 11](https://github.com/affeldt-aist/infotheo).
 Once infotheo is installed (with opam), do:
 - `opam install coq-monae` or `git clone git@github.com:affeldt-aist/monae.git; opam install .`
 
diff --git a/_CoqProject b/_CoqProject
index f61e0c80..2cc005fc 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -5,33 +5,33 @@
 -arg -w -arg -notation-incompatible-format
 -arg -w -arg -elpi.add-const-for-axiom-or-sectionvar
 
-monae_lib.v
-hierarchy.v
-monad_lib.v
-fail_lib.v
-state_lib.v
-array_lib.v
-trace_lib.v
-proba_lib.v
-typed_store_lib.v
-monad_composition.v
-monad_model.v
-proba_monad_model.v
-category.v
-gcm_model.v
-altprob_model.v
-monad_transformer.v
-typed_store_model.v
-example_spark.v
-example_nqueens.v
-example_relabeling.v
-example_quicksort.v
-example_iquicksort.v
-example_monty.v
-example_typed_store.v
-smallstep.v
-example_transformer.v
-category_ext.v
-all_monae.v
+theories/core/preamble.v
+theories/core/hierarchy.v
+theories/core/category.v
+theories/core/monad_transformer.v
+theories/lib/monad_lib.v
+theories/lib/fail_lib.v
+theories/lib/state_lib.v
+theories/lib/array_lib.v
+theories/lib/trace_lib.v
+theories/lib/proba_lib.v
+theories/lib/typed_store_lib.v
+theories/models/monad_model.v
+theories/models/proba_monad_model.v
+theories/models/gcm_model.v
+theories/models/altprob_model.v
+theories/models/typed_store_model.v
+theories/applications/monad_composition.v
+theories/applications/example_spark.v
+theories/applications/example_nqueens.v
+theories/applications/example_relabeling.v
+theories/applications/example_quicksort.v
+theories/applications/example_iquicksort.v
+theories/applications/example_monty.v
+theories/applications/example_typed_store.v
+theories/applications/smallstep.v
+theories/applications/example_transformer.v
+theories/applications/category_ext.v
+theories/all_monae.v
 
 -R . monae
diff --git a/coq-monae.opam b/coq-monae.opam
index 16b3e4f9..4ca30249 100644
--- a/coq-monae.opam
+++ b/coq-monae.opam
@@ -15,7 +15,7 @@ description: """
 This Coq library contains a hierarchy of monads with their laws used
 in several examples of monadic equational reasoning."""
 
-build: [make "-j%{jobs}%" ]
+build: [make "-j%{jobs}%"]
 install: [make "install_full"]
 depends: [
   "coq" { (>= "8.18" & < "8.20~") | (= "dev") }
diff --git a/impredicative_set/_CoqProject b/impredicative_set/_CoqProject
index 2231e3b0..c1fb68cd 100644
--- a/impredicative_set/_CoqProject
+++ b/impredicative_set/_CoqProject
@@ -6,7 +6,7 @@
 -arg -w -arg -elpi.add-const-for-axiom-or-sectionvar
 -arg -impredicative-set
 
-imonae_lib.v
+ipreamble.v
 ihierarchy.v
 imonad_lib.v
 ifail_lib.v
diff --git a/impredicative_set/iexample_transformer.v b/impredicative_set/iexample_transformer.v
index 6150ab5c..c2617b29 100644
--- a/impredicative_set/iexample_transformer.v
+++ b/impredicative_set/iexample_transformer.v
@@ -1,7 +1,7 @@
 (* monae: Monadic equational reasoning in Coq                                 *)
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect.
-Require Import imonae_lib ihierarchy imonad_lib ifail_lib istate_lib.
+Require Import ipreamble ihierarchy imonad_lib ifail_lib istate_lib.
 Require Import imonad_transformer.
 
 (******************************************************************************)
diff --git a/impredicative_set/ifail_lib.v b/impredicative_set/ifail_lib.v
index 2898df0d..aca01694 100644
--- a/impredicative_set/ifail_lib.v
+++ b/impredicative_set/ifail_lib.v
@@ -1,7 +1,7 @@
 (* monae: Monadic equational reasoning in Coq                                 *)
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect.
-Require Import imonae_lib.
+Require Import ipreamble.
 From HB Require Import structures.
 Require Import ihierarchy imonad_lib.
 From Equations Require Import Equations.
diff --git a/impredicative_set/ifmt_lifting.v b/impredicative_set/ifmt_lifting.v
index fb688e9d..8825d69b 100644
--- a/impredicative_set/ifmt_lifting.v
+++ b/impredicative_set/ifmt_lifting.v
@@ -2,7 +2,7 @@
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect.
 From HB Require Import structures.
-Require Import imonae_lib ihierarchy imonad_lib imonad_transformer.
+Require Import ipreamble ihierarchy imonad_lib imonad_transformer.
 
 (******************************************************************************)
 (*   Uniform Lifting of Sigma-operations Along Functorial Monad Transformers  *)
diff --git a/impredicative_set/ihierarchy.v b/impredicative_set/ihierarchy.v
index 15455741..4458de2c 100644
--- a/impredicative_set/ihierarchy.v
+++ b/impredicative_set/ihierarchy.v
@@ -4,7 +4,7 @@ Ltac typeof X := type of X.
 
 Require Import ssrmatching JMeq.
 From mathcomp Require Import all_ssreflect.
-Require Import imonae_lib.
+Require Import ipreamble.
 From HB Require Import structures.
 
 (******************************************************************************)
diff --git a/impredicative_set/imonad_composition.v b/impredicative_set/imonad_composition.v
index 6ef83d65..4c8cd68d 100644
--- a/impredicative_set/imonad_composition.v
+++ b/impredicative_set/imonad_composition.v
@@ -2,7 +2,7 @@
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect.
 From HB Require Import structures.
-Require Import imonae_lib ihierarchy imonad_lib.
+Require Import ipreamble ihierarchy imonad_lib.
 
 (******************************************************************************)
 (*                          Composing monads                                  *)
diff --git a/impredicative_set/imonad_lib.v b/impredicative_set/imonad_lib.v
index b0a781cc..ffcf9a26 100644
--- a/impredicative_set/imonad_lib.v
+++ b/impredicative_set/imonad_lib.v
@@ -3,7 +3,7 @@
 Ltac typeof X := type of X.
 Require Import ssrmatching.
 From mathcomp Require Import all_ssreflect.
-Require Import imonae_lib.
+Require Import ipreamble.
 From HB Require Import structures.
 Require Import ihierarchy.
 
diff --git a/impredicative_set/imonad_model.v b/impredicative_set/imonad_model.v
index 211406c4..4edefb18 100644
--- a/impredicative_set/imonad_model.v
+++ b/impredicative_set/imonad_model.v
@@ -1,5 +1,5 @@
 From mathcomp Require Import all_ssreflect.
-Require Import imonae_lib.
+Require Import ipreamble.
 From HB Require Import structures.
 Require Import ihierarchy imonad_lib ifail_lib istate_lib itrace_lib.
 Require Import imonad_transformer.
diff --git a/impredicative_set/imonad_transformer.v b/impredicative_set/imonad_transformer.v
index 23b189f0..c1cdc896 100644
--- a/impredicative_set/imonad_transformer.v
+++ b/impredicative_set/imonad_transformer.v
@@ -1,7 +1,7 @@
 (* monae: Monadic equational reasoning in Coq                                 *)
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect.
-Require Import imonae_lib.
+Require Import ipreamble.
 From HB Require Import structures.
 Require Import ihierarchy imonad_lib ifail_lib istate_lib.
 
diff --git a/impredicative_set/iparametricity_codensity.v b/impredicative_set/iparametricity_codensity.v
index 98b41b46..c9d6886e 100644
--- a/impredicative_set/iparametricity_codensity.v
+++ b/impredicative_set/iparametricity_codensity.v
@@ -4,7 +4,7 @@ From Param Require Import Param.
 
 From mathcomp Require Import all_ssreflect.
 From HB Require Import structures.
-Require Import imonae_lib ihierarchy imonad_lib ifmt_lifting imonad_model.
+Require Import ipreamble ihierarchy imonad_lib ifmt_lifting imonad_model.
 
 (******************************************************************************)
 (* Instantiations of uniform lifting (Theorem 27 of [Mauro Jaskelioff,        *)
diff --git a/impredicative_set/imonae_lib.v b/impredicative_set/ipreamble.v
similarity index 100%
rename from impredicative_set/imonae_lib.v
rename to impredicative_set/ipreamble.v
diff --git a/impredicative_set/istate_lib.v b/impredicative_set/istate_lib.v
index 28b63046..76b731d6 100644
--- a/impredicative_set/istate_lib.v
+++ b/impredicative_set/istate_lib.v
@@ -1,7 +1,7 @@
 (* monae: Monadic equational reasoning in Coq                                 *)
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect.
-Require Import imonae_lib.
+Require Import ipreamble.
 From HB Require Import structures.
 Require Import ihierarchy imonad_lib ifail_lib.
 
diff --git a/meta.yml b/meta.yml
index 20d15450..4c8b013c 100644
--- a/meta.yml
+++ b/meta.yml
@@ -180,36 +180,44 @@ documentation: |-
 
   ## Files
 
-  - basics:
-    + [monae_lib.v](./monae_lib.v): simple additions to base libraries
-    + [hierarchy.v](./hierarchy.v): hierarchy of monadic effects
-    + [category.v](./category.v): formalization of concrete categories (generalization of the bottom layers of `hierarchy.v`)
-    + [monad_transformer.v](./monad_transformer.v): monad transformers
+  - core:
+    + [preamble.v](./theories/core/preamble.v): simple additions to base libraries
+    + [hierarchy.v](./theories/core/hierarchy.v): hierarchy of monadic effects
+    + [category.v](./theories/core/category.v): formalization of concrete categories (generalization of the bottom layers of `hierarchy.v`)
+    + [monad_transformer.v](./theories/core/monad_transformer.v): monad transformers
       * completed by `ifmt_lifting.v` and `iparametricty_codensity.v` in the directory `impredicative_set`
         - the directory `impredicative_set` contains a lighter version of Monae where monads live in `Set` and that compiles with `impredicative-set`
-  - utility lemmas:  
-    + [monad_lib.v](./monad_lib.v): basic lemmas about monads
-    + [fail_lib.v](./fail_lib.v): lemmas about the fail monad and related monads
-    + [state_lib.v](./state_lib.v): lemmas about state-related monads
-    + [array_lib.v](./array_lib.v): lemmas about the array monad
-    + [trace_lib.v](./trace_lib.v): lemmas about about the state-trace monad
-    + [proba_lib.v](./proba_lib.v): lemmas about the probability monad
-    + [typed_store_lib.v](./typed_store_lib.v): derived definitions and lemmas about about the typed store monad
+  - libraries for each monad theory:  
+    + [monad_lib.v](./theories/lib/monad_lib.v): basic lemmas about monads
+    + [fail_lib.v](./theories/lib/fail_lib.v): lemmas about the fail monad and related monads
+    + [state_lib.v](./theories/lib/state_lib.v): lemmas about state-related monads
+    + [array_lib.v](./theories/lib/array_lib.v): lemmas about the array monad
+    + [trace_lib.v](./theories/lib/trace_lib.v): lemmas about about the state-trace monad
+    + [proba_lib.v](./theories/lib/proba_lib.v): lemmas about the probability monad
+    + [typed_store_lib.v](./theories/lib/typed_store_lib.v): derived definitions and lemmas about about the typed store monad
   - models of monads:
-    + [monad_model.v](./monad_model.v): concrete models of monads
-    + [proba_monad_model.v](./proba_monad_model.v): model of the probability monad
-    + [gcm_model.v](./gcm_model.v): model of the geometrically convex monad
-    + [altprob_model.v](./altprob_model.v): model of a monad that mixes non-deterministic choice and probabilistic choice
-    + [typed_store_model.v](./typed_store_model.v): alternative model of the typed store monad
+    + [monad_model.v](./theories/models/monad_model.v): concrete models of monads
+    + [proba_monad_model.v](./theories/models//proba_monad_model.v): model of the probability monad
+    + [gcm_model.v](./theories/models//gcm_model.v): model of the geometrically convex monad
+    + [altprob_model.v](./theories/models//altprob_model.v): model of a monad that mixes non-deterministic choice and probabilistic choice
+    + [typed_store_model.v](./theories/models//typed_store_model.v): alternative model of the typed store monad
   - applications:
-    + [monad_composition.v](./monad_composition.v): composing monads
-    + [smallstep.v](./smallstep.v): semantics for an imperative language, with equivalence operational semantics/denotation and sample imperative programs
-    + example_*.v: various examples (Spark aggregation, the n-queens puzzle, tree relabeling,  Monty Hall problem, monad transformers, quicksort, OCaml programs, etc.)
-
-  ## About Installation with Windows 10 or 11
+    + [example_relabeling.v](./theories/applications/example_relabeling.v): tree relabeling
+    + [example_monty.v](./theories/applications/example_monty.v): Monty Hall problem
+    + [example_spark.v](./theories/applications/example_spark.v): Spark aggregation
+    + [example_iquicksort.v](./theories/applications/example_iquicksort.v): in-place quicksort
+    + [example_quicksort.v](./theories/applications/example_quicksort.v): functional quicksort
+    + [example_nqueens.v](./theories/applications/example_nqueens.v): the n-queens puzzle
+    + [example_typed_store.v](./theories/applications/example_typed_store.v): ML programs with references
+    + [example_transformer.v](./theories/applications/example_transformer.v): monad transformers
+    + [smallstep.v](./theories/applications/smallstep.v): semantics for an imperative language, with equivalence operational semantics/denotation and sample imperative programs
+    + [monad_composition.v](./theories/applications/monad_composition.v): composing monads
+    + [category_ext.v](./theories/applications/category_ext.v): experimental library about categories
+
+  ## About Installation with Windows 11
  
   Installation of monae on Windows is less simple.
-  First install infotheo following the [instructions for Windows 10](https://github.com/affeldt-aist/infotheo).
+  First install infotheo following the [instructions for Windows 11](https://github.com/affeldt-aist/infotheo).
   Once infotheo is installed (with opam), do:
   - `opam install coq-monae` or `git clone git@github.com:affeldt-aist/monae.git; opam install .`
 
diff --git a/all_monae.v b/theories/all_monae.v
similarity index 94%
rename from all_monae.v
rename to theories/all_monae.v
index eaf670ee..be4dd9b7 100644
--- a/all_monae.v
+++ b/theories/all_monae.v
@@ -1,4 +1,4 @@
-Require Export monae_lib.
+Require Export preamble.
 Require Export hierarchy.
 Require Export monad_lib.
 Require Export fail_lib.
diff --git a/category_ext.v b/theories/applications/category_ext.v
similarity index 98%
rename from category_ext.v
rename to theories/applications/category_ext.v
index 8af624ed..5514dd1a 100644
--- a/category_ext.v
+++ b/theories/applications/category_ext.v
@@ -1,6 +1,8 @@
+(* monae: Monadic equational reasoning in Coq                                 *)
+(* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require Import boolp.
-Require Import monae_lib category.
+Require Import preamble category.
 From HB Require Import structures.
 
 (******************************************************************************)
diff --git a/example_iquicksort.v b/theories/applications/example_iquicksort.v
similarity index 99%
rename from example_iquicksort.v
rename to theories/applications/example_iquicksort.v
index 043ea453..4c7e9449 100644
--- a/example_iquicksort.v
+++ b/theories/applications/example_iquicksort.v
@@ -2,7 +2,7 @@
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require boolp.
-Require Import monae_lib hierarchy monad_lib fail_lib state_lib.
+Require Import preamble hierarchy monad_lib fail_lib state_lib.
 Require Import array_lib example_quicksort.
 From infotheo Require Import ssr_ext.
 
diff --git a/example_monty.v b/theories/applications/example_monty.v
similarity index 99%
rename from example_monty.v
rename to theories/applications/example_monty.v
index a8e1f8eb..d870478a 100644
--- a/example_monty.v
+++ b/theories/applications/example_monty.v
@@ -4,7 +4,7 @@ Require Import Reals Lra.
 From mathcomp Require Import all_ssreflect ssralg ssrnum.
 From mathcomp Require Import mathcomp_extra reals Rstruct.
 From infotheo Require Import ssrR realType_ext Reals_ext proba.
-Require Import monae_lib hierarchy monad_lib fail_lib proba_lib.
+Require Import preamble hierarchy monad_lib fail_lib proba_lib.
 
 (******************************************************************************)
 (*                            Monty Hall example                              *)
diff --git a/example_nqueens.v b/theories/applications/example_nqueens.v
similarity index 99%
rename from example_nqueens.v
rename to theories/applications/example_nqueens.v
index c90fd189..9f600b3f 100644
--- a/example_nqueens.v
+++ b/theories/applications/example_nqueens.v
@@ -4,7 +4,7 @@ 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.
+Require Import preamble hierarchy monad_lib fail_lib state_lib.
 
 (******************************************************************************)
 (*                            N-queens example                                *)
diff --git a/example_quicksort.v b/theories/applications/example_quicksort.v
similarity index 99%
rename from example_quicksort.v
rename to theories/applications/example_quicksort.v
index 106fcd23..bb8fa073 100644
--- a/example_quicksort.v
+++ b/theories/applications/example_quicksort.v
@@ -2,7 +2,7 @@
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require boolp.
-Require Import monae_lib.
+Require Import preamble.
 Require Import hierarchy monad_lib fail_lib state_lib.
 From infotheo Require Import ssr_ext.
 Require Import Recdef.
diff --git a/example_relabeling.v b/theories/applications/example_relabeling.v
similarity index 99%
rename from example_relabeling.v
rename to theories/applications/example_relabeling.v
index 98e53b84..b718484c 100644
--- a/example_relabeling.v
+++ b/theories/applications/example_relabeling.v
@@ -2,7 +2,7 @@
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require boolp.
-Require Import monae_lib hierarchy monad_lib fail_lib state_lib.
+Require Import preamble hierarchy monad_lib fail_lib state_lib.
 
 (******************************************************************************)
 (*                           Tree relabeling                                  *)
diff --git a/example_spark.v b/theories/applications/example_spark.v
similarity index 99%
rename from example_spark.v
rename to theories/applications/example_spark.v
index 02db9fcd..2e3e153f 100644
--- a/example_spark.v
+++ b/theories/applications/example_spark.v
@@ -2,7 +2,7 @@
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require boolp.
-Require Import monae_lib hierarchy monad_lib fail_lib.
+Require Import preamble hierarchy monad_lib fail_lib.
 
 (******************************************************************************)
 (*                              Spark example                                 *)
diff --git a/example_transformer.v b/theories/applications/example_transformer.v
similarity index 98%
rename from example_transformer.v
rename to theories/applications/example_transformer.v
index 9a4ea730..9f5dbb96 100644
--- a/example_transformer.v
+++ b/theories/applications/example_transformer.v
@@ -1,7 +1,7 @@
 (* monae: Monadic equational reasoning in Coq                                 *)
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect.
-Require Import monae_lib hierarchy monad_lib fail_lib state_lib.
+Require Import preamble hierarchy monad_lib fail_lib state_lib.
 Require Import monad_transformer.
 
 (******************************************************************************)
diff --git a/example_typed_store.v b/theories/applications/example_typed_store.v
similarity index 99%
rename from example_typed_store.v
rename to theories/applications/example_typed_store.v
index 4aafb051..759b86bf 100644
--- a/example_typed_store.v
+++ b/theories/applications/example_typed_store.v
@@ -6,7 +6,7 @@ From mathcomp Require boolp.
 From infotheo Require Import ssrZ.
 Require Import monad_model.
 From HB Require Import structures.
-Require Import monae_lib hierarchy monad_lib typed_store_lib.
+Require Import preamble hierarchy monad_lib typed_store_lib.
 
 (******************************************************************************)
 (*                         Typed store examples                               *)
diff --git a/monad_composition.v b/theories/applications/monad_composition.v
similarity index 99%
rename from monad_composition.v
rename to theories/applications/monad_composition.v
index 412c4737..dc135c56 100644
--- a/monad_composition.v
+++ b/theories/applications/monad_composition.v
@@ -2,7 +2,7 @@
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect.
 From HB Require Import structures.
-Require Import monae_lib hierarchy monad_lib.
+Require Import preamble hierarchy monad_lib.
 
 (******************************************************************************)
 (*                          Composing monads                                  *)
diff --git a/smallstep.v b/theories/applications/smallstep.v
similarity index 100%
rename from smallstep.v
rename to theories/applications/smallstep.v
diff --git a/category.v b/theories/core/category.v
similarity index 99%
rename from category.v
rename to theories/core/category.v
index 8f35bd82..55b1f08f 100644
--- a/category.v
+++ b/theories/core/category.v
@@ -2,7 +2,7 @@
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require Import boolp.
-Require Import monae_lib.
+Require Import preamble.
 From HB Require Import structures.
 
 (******************************************************************************)
diff --git a/hierarchy.v b/theories/core/hierarchy.v
similarity index 99%
rename from hierarchy.v
rename to theories/core/hierarchy.v
index 26ea0a1f..7701e269 100644
--- a/hierarchy.v
+++ b/theories/core/hierarchy.v
@@ -8,7 +8,7 @@ From mathcomp Require boolp.
 From mathcomp Require Import mathcomp_extra Rstruct reals.
 From infotheo Require Import Reals_ext.
 From infotheo Require Import realType_ext.
-Require Import monae_lib.
+Require Import preamble.
 From HB Require Import structures.
 
 (******************************************************************************)
diff --git a/monad_transformer.v b/theories/core/monad_transformer.v
similarity index 99%
rename from monad_transformer.v
rename to theories/core/monad_transformer.v
index b52e6fd8..5c412c45 100644
--- a/monad_transformer.v
+++ b/theories/core/monad_transformer.v
@@ -2,7 +2,7 @@
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require boolp.
-Require Import monae_lib.
+Require Import preamble.
 From HB Require Import structures.
 Require Import hierarchy monad_lib fail_lib state_lib.
 
diff --git a/monae_lib.v b/theories/core/preamble.v
similarity index 100%
rename from monae_lib.v
rename to theories/core/preamble.v
diff --git a/array_lib.v b/theories/lib/array_lib.v
similarity index 99%
rename from array_lib.v
rename to theories/lib/array_lib.v
index 8fb658eb..eb3c32fd 100644
--- a/array_lib.v
+++ b/theories/lib/array_lib.v
@@ -2,7 +2,7 @@
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require boolp.
-Require Import monae_lib.
+Require Import preamble.
 From HB Require Import structures.
 Require Import hierarchy monad_lib fail_lib.
 
diff --git a/fail_lib.v b/theories/lib/fail_lib.v
similarity index 99%
rename from fail_lib.v
rename to theories/lib/fail_lib.v
index eaf17353..ece6ab07 100644
--- a/fail_lib.v
+++ b/theories/lib/fail_lib.v
@@ -2,7 +2,7 @@
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require boolp.
-Require Import monae_lib.
+Require Import preamble.
 From HB Require Import structures.
 Require Import hierarchy monad_lib.
 From infotheo Require convex necset.
diff --git a/monad_lib.v b/theories/lib/monad_lib.v
similarity index 99%
rename from monad_lib.v
rename to theories/lib/monad_lib.v
index 15cebda1..3c20d90c 100644
--- a/monad_lib.v
+++ b/theories/lib/monad_lib.v
@@ -4,7 +4,7 @@ Ltac typeof X := type of X.
 Require Import ssrmatching.
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require boolp.
-Require Import monae_lib.
+Require Import preamble.
 From HB Require Import structures.
 Require Import hierarchy.
 
diff --git a/proba_lib.v b/theories/lib/proba_lib.v
similarity index 99%
rename from proba_lib.v
rename to theories/lib/proba_lib.v
index 901ce8e3..e070d010 100644
--- a/proba_lib.v
+++ b/theories/lib/proba_lib.v
@@ -7,7 +7,7 @@ From mathcomp Require boolp.
 From mathcomp Require Import reals mathcomp_extra Rstruct lra.
 From infotheo Require Import ssrR realType_ext Reals_ext.
 From infotheo Require Import proba convex necset.
-Require Import monae_lib hierarchy monad_lib fail_lib.
+Require Import preamble hierarchy monad_lib fail_lib.
 
 (******************************************************************************)
 (*             Definitions and lemmas for probability monads                  *)
diff --git a/state_lib.v b/theories/lib/state_lib.v
similarity index 99%
rename from state_lib.v
rename to theories/lib/state_lib.v
index dc4aa465..82425a84 100644
--- a/state_lib.v
+++ b/theories/lib/state_lib.v
@@ -2,7 +2,7 @@
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require boolp.
-Require Import monae_lib.
+Require Import preamble.
 From HB Require Import structures.
 Require Import hierarchy monad_lib fail_lib.
 
diff --git a/trace_lib.v b/theories/lib/trace_lib.v
similarity index 100%
rename from trace_lib.v
rename to theories/lib/trace_lib.v
diff --git a/typed_store_lib.v b/theories/lib/typed_store_lib.v
similarity index 99%
rename from typed_store_lib.v
rename to theories/lib/typed_store_lib.v
index f0445f31..82d1c0b7 100644
--- a/typed_store_lib.v
+++ b/theories/lib/typed_store_lib.v
@@ -6,7 +6,7 @@ Require Import ssrmatching Reals JMeq.
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require boolp.
 From infotheo Require Import Reals_ext.
-Require Import monae_lib hierarchy.
+Require Import preamble hierarchy.
 
 (******************************************************************************)
 (*                      Lemmas using the typed store monad                    *)
diff --git a/altprob_model.v b/theories/models/altprob_model.v
similarity index 98%
rename from altprob_model.v
rename to theories/models/altprob_model.v
index e7e410be..fdbe0290 100644
--- a/altprob_model.v
+++ b/theories/models/altprob_model.v
@@ -10,7 +10,7 @@ From infotheo Require Import Reals_ext realType_ext.
 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 preamble hierarchy monad_lib proba_lib monad_model gcm_model.
 Require Import category.
 
 (******************************************************************************)
diff --git a/gcm_model.v b/theories/models/gcm_model.v
similarity index 99%
rename from gcm_model.v
rename to theories/models/gcm_model.v
index 53ccaf54..ef9b5197 100644
--- a/gcm_model.v
+++ b/theories/models/gcm_model.v
@@ -6,7 +6,7 @@ From mathcomp Require Import boolp classical_sets.
 From mathcomp Require Import finmap.
 From infotheo Require Import Reals_ext classical_sets_ext ssrR ssr_ext.
 From infotheo Require Import fdist fsdist convex necset.
-Require Import monae_lib.
+Require Import preamble.
 From HB Require Import structures.
 Require Import category.
 
diff --git a/monad_model.v b/theories/models/monad_model.v
similarity index 99%
rename from monad_model.v
rename to theories/models/monad_model.v
index 0ab75b0a..0bb520b1 100644
--- a/monad_model.v
+++ b/theories/models/monad_model.v
@@ -4,7 +4,7 @@ From mathcomp Require Import finmap.
 From mathcomp Require boolp.
 From mathcomp Require Import classical_sets.
 From infotheo Require convex classical_sets_ext.
-Require Import monae_lib.
+Require Import preamble.
 From HB Require Import structures.
 Require Import hierarchy monad_lib fail_lib state_lib trace_lib.
 Require Import monad_transformer.
@@ -344,7 +344,7 @@ Proof. by move=> A B C f g; apply boolp.funext => -[]. Qed.
 HB.instance Definition _ := isFunctor.Build acto func_id func_comp.
 End empty.
 End Empty.
-HB.export monae.monad_model.Empty.
+HB.export monae.theories.models.monad_model.Empty.
 
 Module Append.
 Section append.
diff --git a/proba_monad_model.v b/theories/models/proba_monad_model.v
similarity index 98%
rename from proba_monad_model.v
rename to theories/models/proba_monad_model.v
index 26045c02..6b7a037c 100644
--- a/proba_monad_model.v
+++ b/theories/models/proba_monad_model.v
@@ -7,7 +7,7 @@ From mathcomp Require Import reals Rstruct.
 From infotheo Require Import Reals_ext realType_ext ssr_ext fsdist.
 From infotheo Require Import convex.
 From HB Require Import structures.
-Require Import monae_lib hierarchy monad_lib proba_lib.
+Require Import preamble hierarchy monad_lib proba_lib.
 
 (******************************************************************************)
 (*                     Model for the probability monad                        *)
diff --git a/typed_store_model.v b/theories/models/typed_store_model.v
similarity index 99%
rename from typed_store_model.v
rename to theories/models/typed_store_model.v
index c95f02b5..e3e5681c 100644
--- a/typed_store_model.v
+++ b/theories/models/typed_store_model.v
@@ -4,7 +4,7 @@ Require Import JMeq.
 From mathcomp Require Import all_ssreflect finmap.
 From mathcomp Require boolp.
 #[local] Remove Hints boolp.Prop_irrelevance : core.
-Require Import monae_lib.
+Require Import preamble.
 From HB Require Import structures.
 Require Import hierarchy monad_lib fail_lib state_lib trace_lib.
 Require Import monad_transformer monad_model.