diff --git a/_CoqProject b/_CoqProject
index 2f1a3801..7940a007 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -8,6 +8,8 @@
 theories/core/preamble.v
 theories/core/hierarchy.v
 theories/core/category.v
+theories/core/concrete_category.v
+theories/core/monad_of_category_monad.v
 theories/core/monad_transformer.v
 theories/lib/monad_lib.v
 theories/lib/alt_lib.v
diff --git a/theories/core/category.v b/theories/core/category.v
index 140db9a7..9d60a567 100644
--- a/theories/core/category.v
+++ b/theories/core/category.v
@@ -1,9 +1,9 @@
 (* monae: Monadic equational reasoning in Rocq                                *)
 (* Copyright (C) 2025 monae authors, license: LGPL-2.1-or-later               *)
+From HB Require Import structures.
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require Import boolp.
 Require Import preamble.
-From HB Require Import structures.
 
 (**md**************************************************************************)
 (* # Formalization of basic category theory                                   *)
@@ -20,18 +20,18 @@ From HB Require Import structures.
 (*                        definition of concrete categories                   *)
 (*        {hom A -> B} == the hom-set of morphisms from A to B, where A and B *)
 (*                        are objects of a category C                         *)
-(*             [hom f] == morphism corresponding to the function f            *)
-(*                  CT := [the category of Type]                              *)
 (*         FunctorLaws == module that defines the functor laws                *)
-(*                  \O == functor composition                                 *)
-(*             F ~~> G == forall a, {hom F a ,G a}, which corresponds to a    *)
+(*             F ~~> G == unnatural transformation, i.e., functions of type   *)
+(*                        forall a, {hom F a ,G a};  corresponds to a         *)
 (*                        natural transformation when it satisfies the        *)
 (*                        predicate naturality                                *)
+(*              F ~> G == natural transformation: F ~~> G with naturality     *)
 (*                 NId == the identity natural transformation                 *)
-(*          [NEq F, G] == natural transformation from F to G where F and G    *)
-(*                        are convertible, especially when they are           *)
-(*                        compositions, and differ only by associativity or   *)
-(*                        insertion of unit functors                          *)
+(*          [NEq F, G] == natural transformation from F to G, where the       *)
+(*                        object parts of F and G are convertible, and the    *)
+(*                        morphism parts are transportable; e.g., when they   *)
+(*                        are compositions that differ only by associativity  *)
+(*                        or insertion of identity functors                   *)
 (*                  \v == vertical composition                                *)
 (*                  \h == horizontal composition, or Godement product         *)
 (*              F -| G == pair of adjoint functors (Module                    *)
@@ -40,13 +40,10 @@ From HB Require Import structures.
 (*                        two pairs of adjoint functors                       *)
 (*  JoinLaws, BindLaws == modules that define the monad laws                  *)
 (*             isMonad == mixin that defines the monad interface              *)
-(*   Monad_of_ret_bind == factory, monad defined by ret and bind              *)
 (*   Monad_of_ret_join == factory, monad defined by ret and join              *)
-(* Monad_of_adjoint_functors == module that defines a monad by a pair of      *)
-(*                        adjoint functors                                    *)
-(* Monad_of_category_monad == module, interface to isMonad from hierarchy.v   *)
-(* Monad_of_category_monad.m == turns a monad over the Type category into     *)
-(*                        a monad in the sense of isMonad from hierarchy.v    *)
+(*   Monad_of_ret_bind == factory, monad defined by ret and bind;             *)
+(*                        M need not be a priori a functor                    *)
+(* Monad_of_adjoint_functors == monad defined from a pair of adjoint functors *)
 (* ```                                                                        *)
 (******************************************************************************)
 
@@ -75,105 +72,36 @@ Proof. by []. Defined.
 #[global]
 Hint Resolve frefl_transparent : core.
 
-(* Our categories are always concrete; morphisms are just functions. *)
 HB.mixin Record isCategory (obj : Type) := {
-  el : obj -> Type ;
-  inhom : forall a b, (el a -> el b) -> Prop ;
-  idfun_inhom : forall a, @inhom a a idfun ;
-  funcomp_inhom : forall a b c (f : el a -> el b) (g : el b -> el c),
-      inhom _ _ f -> inhom _ _ g -> inhom _ _ (g \o f)
+  hom : obj -> obj -> Type ;
+  id : forall a, hom a a ;
+  comp : forall {a b c}, hom a b -> hom b c -> hom a c ;
+  left_id : forall a b (f : hom a b), comp f (id b) = f ;
+  right_id : forall a b (f : hom a b), comp (id a) f = f ;
+  assoc : forall a b c d (f : hom a b) (g : hom b c) (h : hom c d),
+      comp (comp f g) h = comp f (comp g h);
 }.
 Arguments isCategory.phant_Build : clear implicits.
 
 #[short(type=category)]
 HB.structure Definition Category := {C of isCategory C}.
+Arguments id {C} : rename.
+Arguments comp {C a b c} : rename.
 
-Arguments idfun_inhom [C] : rename.
-Arguments funcomp_inhom [C a b c f g] : rename.
-
-HB.mixin Record isHom (C : category) (a b : C) (f : el a -> el b) := {
-  isHom_inhom : inhom a b f
-}.
-HB.structure Definition Hom (C : category) (a b : C) :=
-  {f of isHom C a b f}.
-Arguments isHom_inhom [C a b].
-
-Notation "{ 'hom' U -> V }" := (Hom.type U V) : category_scope.
-Notation "{ 'hom' '[' C ']' U '->' V }" := (@Hom.type C U V)
+Notation "{ 'hom' U -> V }" := (hom U V) : category_scope.
+Notation "{ 'hom' '[' C ']' U '->' V }" := (@hom C U V)
   (only parsing) : category_scope.
-Notation "[ 'hom' f ]" := [the {hom _ -> _} of f]
-  (at level 0, format "[ 'hom'  f ]") : category_scope.
-(* TODO: FIX: At some places, this [hom f] notation is not used for printing and
-   [the {hom ...} of f] is undesirably printed instead. *)
-
-Lemma hom_ext (C : category) (a b : C) (f g : {hom a -> b}) :
-  f = g <-> f = g :> (_ -> _).
-Proof.
-move: f g => [f [[Hf]]] [g [[Hg]]] /=; split => [[]//|fg /=].
-rewrite fg in Hf Hg *.
-by rewrite (boolp.Prop_irrelevance Hf Hg).
-Qed.
-
-Section hom_interface.
-Variable C : category.
-Implicit Types a b c : C.
 
-HB.instance Definition _ c := isHom.Build _ _ _ (@idfun (el c)) (idfun_inhom c).
-
-HB.instance Definition _ (a b c : C) (f : {hom b -> c}) (g : {hom a -> b}):=
-  isHom.Build _ _ _ (f \o g) (funcomp_inhom (isHom_inhom g) (isHom_inhom f)).
-End hom_interface.
-
-(* Notation [\o f , .. , g , h] for hom compositions. *)
+(* Notations \c and [\c f , .. , g , h] for hom compositions. *)
+Notation "[id]" := (id _).
+Notation "g \c f" := (comp f g) (at level 50, format "g  \c  f").
 Module comps_notation.
-Notation "[ '\o' f , .. , g , h ]" := (f \o .. (g \o h) ..) (at level 0,
-  format "[ '[' '\o'  f ,  '/' .. ,  '/' g ,  '/' h ']' ]") : category_scope.
-End comps_notation.
-
-Section category_lemmas.
-Variable C : category.
-
-Lemma homfunK (a b : C) (f : {hom a -> b}) : [hom f] = f.
-Proof. by []. Qed.
-
-Lemma homcompA (a b c d : C) (h : {hom c -> d}) (g : {hom b -> c}) (f : {hom a -> b}) :
-  [hom [hom h \o g] \o f] = [hom h \o [hom g \o f]].
-Proof. by move: f g h => [? ?] [? ?] [? ?]; apply hom_ext. Qed.
-
-Lemma homcompE (a b c : C) (g : {hom b -> c}) (f : {hom a -> b}) :
-  [hom g \o f] = g \o f :> (el a -> el c).
-Proof. by []. Qed.
-
-Lemma hom_compE (a b c : C) (g : {hom b -> c}) (f : {hom a -> b}) x :
-  g (f x) = (g \o f) x.
-Proof. exact: compE. Qed.
-
-Import comps_notation.
-
-(* Restricting the components of a composition to homs and using the lemma
-   homcompA, we can avoid the infinite sequence of redundunt compositions
-   "_ \o id" or "id \o _" that pops out when we "rewrite !compA".*)
-Lemma hom_compA (a b c d : C) (h : {hom c -> d}) (g : {hom b -> c}) (f : {hom a -> b}) :
-  (h \o g) \o f = [\o h, g, f] :> (el a -> el d).
-Proof. exact: compA. Qed.
 
-Example hom_compA' (a b c d : C) (h : {hom c -> d}) (g : {hom b -> c}) (f : {hom a -> b}) :
-  (h \o g) \o f = [\o h, g, f].
-Proof.
-rewrite 10!compA.
-Undo 1.
-by rewrite !hom_compA.
-(* rewrite !homcompA blocks id's from coming in, thanks to {hom _ ->_} conditions on arguments. *)
-Abort.
-
-(* Tactic support is desirable for the following two cases :
-   1. rewriting at the head of the sequence;
-      compare for example the lemmas natural and natural_head below
-   2. rewriting under [hom _];
-      dependent type errors and explicit application of hom_ext is tedious.
-*)
-
-End category_lemmas.
+Notation "[ '\o' f , g , .. , h ]" := ( .. (f \o g) .. \o h) (at level 0,
+  format "[ '[' '\o'  f ,  g ,  '/' .. ,  '/' h ']' ]") : category_scope.
+Notation "[ '\c' f , g , .. , h ]" := ( .. (f \c g) .. \c h) (at level 0,
+  format "[ '[' '\c'  f ,  g ,  '/' .. ,  '/' h ']' ]") : category_scope.
+End comps_notation.
 
 (* transportation of hom along equality *)
 Section transport_lemmas.
@@ -190,73 +118,66 @@ Definition transport_hom (a a' b b' : C) (pa : a = a') (pb : b = b')
           (eq_rect a (fun x => {hom x -> b}) f a' pa)
           b' pb.
 Definition hom_of_eq (a b : C) (p : a = b) : {hom a -> b} :=
-  transport_codom p [hom idfun].
-(* (* this works too; not sure which is better *)
-Definition hom_of_eq (a b : C) (p : a = b) : {hom a -> b} :=
-  transport_codom p [hom idfun].
-*)
+  transport_codom p (id a).
+End transport_lemmas.
 
+Section concrete_transport_lemmas.
+Variable C : category.
 (* F for factorization *)
 Lemma transport_domF (a a' b : C) (p : a = a') (f : {hom a -> b}) :
-  transport_dom p f = [hom f \o hom_of_eq (esym p)].
-Proof. apply hom_ext; by subst a'. Qed.
+  transport_dom p f = f \c hom_of_eq (esym p).
+Proof. by subst a'=> /=; rewrite right_id. Qed.
+
 Lemma transport_codomF (a b b' : C) (p : b = b') (f : {hom a -> b}) :
-  transport_codom p f = [hom hom_of_eq p \o f].
-Proof. apply hom_ext; by subst b'. Qed.
+  transport_codom p f = hom_of_eq p \c f.
+Proof. by subst b'=> /=; rewrite left_id. Qed.
 Lemma transport_homF (a a' b b' : C) (pa : a = a') (pb : b = b') (f : {hom a -> b}) :
-  transport_hom pa pb f = [hom hom_of_eq pb \o f \o hom_of_eq (esym pa)].
-Proof. apply hom_ext; by subst a' b'. Qed.
-End transport_lemmas.
+  transport_hom pa pb f = hom_of_eq pb \c f \c hom_of_eq (esym pa).
+Proof. by subst a' b'=> //=; rewrite left_id right_id. Qed.
+End concrete_transport_lemmas.
 
 Section Type_as_a_category.
 (* TODO: consider using universe polymorphism *)
-Let UUx := Type.
+Let UUx := Type@{UU_category}.
 
 HB.instance Definition _ :=
-  isCategory.Build UUx (fun x : Type => x)
-    (fun _ _ _ => True) (fun=> I) (fun _ _ _ _ _ _ _ => I).
-
-HB.instance Definition _ (a b : [the category of UUx]) (f : a -> b)
-  := isHom.Build [the category of UUx] a b (f : el a -> el b) I.
+  isCategory.Build
+    UUx (fun a b => a -> b) (@idfun) (fun _ _ _ f g => g \o f)
+    (fun _ _ _ => erefl)
+    (fun _ _ _ => erefl)
+    (fun _ _ _ _ _ _ _ => erefl).
 
 End Type_as_a_category.
 
-Notation CT := [the category of Type].
-
 Module FunctorLaws.
 Section def.
 Variable (C D : category).
 Variable (F : C -> D) (f : forall a b, {hom a -> b} -> {hom F a -> F b}).
-Definition id := forall a, f [hom idfun] = [hom idfun] :> {hom F a -> F a}.
+Definition id := forall a, f (id a) = (id (F a)).
 Definition comp := forall a b c (g : {hom b -> c}) (h : {hom a -> b}),
-  f [hom g \o h] = [hom f g \o f h].
+  f (g \c h) = f g \c f h.
 End def.
 End FunctorLaws.
 
 HB.mixin Record isFunctor (C D : category) (F : C -> D) := {
-  actm : forall a b, {hom a -> b} -> {hom F a -> F b} ;
-  functor_id_hom : FunctorLaws.id actm ;
-  functor_o_hom : FunctorLaws.comp actm }.
+  Fhom : forall a b, {hom a -> b} -> {hom F a -> F b} ;
+  Fhom_id : FunctorLaws.id Fhom ;
+  Fhom_comp : FunctorLaws.comp Fhom }.
 
+#[short(type=functor)]
 HB.structure Definition Functor C D := {F of isFunctor C D F}.
-(*Notation functor := Functor.type.*)
+Arguments Fhom_id {C D}.
+Arguments Fhom_comp {C D}.
 
-Definition functor_phant (C D : category) of phant (C -> D) := Functor.type C D.
-Arguments actm [C D] F [a b] f: rename.
-Notation "F # f" := (actm F f) : category_scope.
+Definition functor_phant (C D : category) of phant (C -> D) := functor C D.
+Arguments Fhom {C D} F {a b} f: rename.
+Notation "F # f" := (Fhom F f) : category_scope.
 Notation "{ 'functor' fCD }" := (functor_phant (Phant fCD))
-  (format "{ 'functor'  fCD }") : category_scope.
+                                  (format "{ 'functor'  fCD }"): category_scope.
 
 Section functor_lemmas.
 Variables (C D : category) (F : {functor C -> D}).
 
-Lemma functor_id a : F # [hom idfun] = idfun :> (el (F a) -> el (F a)).
-Proof. by rewrite functor_id_hom. Qed.
-
-Lemma functor_o a b c (g : {hom b -> c}) (h : {hom a -> b}) :
-  F # [hom g \o h] = F # g \o F # h :> (el (F a) -> el (F c)).
-Proof. by rewrite functor_o_hom. Qed.
-
 Lemma functor_ext (G : {functor C -> D}) (pm : F =1 G) :
   (forall (A B : C) (f : {hom A -> B}),
       transport_hom (pm A) (pm B) (F # f) = G # f) -> F = G.
@@ -282,23 +203,24 @@ exact: erefl.
 Qed.
 End functor_lemmas.
 
-Section functor_o_head.
+Section Fhom_comp_tail.
 Import comps_notation.
 Variable C D : category.
-Lemma functor_o_head a b c (g : {hom b -> c}) (h : {hom a -> b}) d (F : {functor C -> D})
-    (k : {hom d -> F a}) :
-  (F # [hom g \o h]) \o k = [\o F # g, F # h, k].
-Proof. by rewrite functor_o_hom. Qed.
-End functor_o_head.
-Arguments functor_o_head [C D a b c g h d] F.
+Lemma Fhom_comp_tail (F : {functor C -> D})
+      a b c d (g : {hom b -> c}) (h : {hom a -> b}) (k : {hom F c -> d}) :
+  k \c (F # (g \c h)) = [\c k, F # g, F # h].
+Proof. by rewrite Fhom_comp assoc. Qed.
+End Fhom_comp_tail.
+Arguments Fhom_comp_tail [C D] F [a b c d].
 
 Section functorid.
 Variables C : category.
 Definition id_f (A B : C) (f : {hom A -> B}) := f.
 Lemma id_id : FunctorLaws.id id_f. Proof. by []. Qed.
 Lemma id_comp : FunctorLaws.comp id_f. Proof. by []. Qed.
-HB.instance Definition _ := isFunctor.Build _ _ idfun id_id id_comp.
-Definition FId : {functor C -> C} := [the {functor _ -> _} of idfun].
+Let _id (x : C) := x.
+HB.instance Definition _ := isFunctor.Build C C _id id_id id_comp.
+Definition FId : {functor C -> C} := _id.
 Lemma FIdf (A B : C) (f : {hom A -> B}) : FId # f = f.
 Proof. by []. Qed.
 End functorid.
@@ -311,47 +233,48 @@ Variables (F : {functor C1 -> C2}) (G : {functor C0 -> C1}).
 Definition functorcomposition a b := fun h : {hom a -> b} => F # (G # h).
 
 Lemma functorcomposition_id : FunctorLaws.id functorcomposition.
-Proof. by move=> A; rewrite /functorcomposition 2!functor_id_hom. Qed.
+Proof. by move=> A; rewrite /functorcomposition 2!Fhom_id. Qed.
 
 Lemma functorcomposition_comp : FunctorLaws.comp functorcomposition.
 Proof.
-by move=> a b c g h; rewrite /functorcomposition; rewrite 2!functor_o_hom.
+by move=> a b c g h; rewrite /functorcomposition; rewrite 2!Fhom_comp.
 Qed.
 
 HB.instance Definition _ :=
   isFunctor.Build C0 C2 (F \o G) functorcomposition_id functorcomposition_comp.
 End functorcomposition.
-Notation "F \O G" := ([the {functor _ -> _} of F \o G]) : category_scope.
+
 
 Section functorcomposition_lemmas.
 Lemma FCompE (C0 C1 C2 : category)
-      (F : {functor C1 -> C2}) (G : {functor C0 -> C1}) a b (k : {hom a -> b}) :
-  (F \O G) # k = F # (G # k).
+  (F : {functor C1 -> C2}) (G : {functor C0 -> C1}) a b (k : {hom a -> b}) :
+  (F \o G) # k = F # (G # k).
 Proof. by []. Qed.
 
 Variables (C0 C1 C2 C3 : category).
 
-Lemma FCompId (F : {functor C0 -> C1}) : F \O FId = F.
+Lemma FCompId (F : {functor C0 -> C1}) : F \o FId = F :> {functor _ -> _}.
 Proof. by apply: functor_ext=> *; rewrite FCompE FIdf. Qed.
 
-Lemma FIdComp (F : {functor C0 -> C1}) : FId \O F = F.
+Lemma FIdComp (F : {functor C0 -> C1}) : FId \o F = F :> {functor _ -> _}.
 Proof. by apply: functor_ext=> *; rewrite FCompE FIdf. Qed.
 
 Lemma FCompA
   (F : {functor C2 -> C3}) (G : {functor C1 -> C2}) (H : {functor C0 -> C1}) :
-  (F \O G) \O H = F \O (G \O H).
+  (F \o G) \o H = F \o (G \o H) :> {functor _ -> _}.
 Proof. apply: functor_ext=> *; by rewrite FCompE. Qed.
 End functorcomposition_lemmas.
 
-Notation "F ~~> G" := (forall a, {hom F a  ->G a}) : category_scope.
+Notation "F ~~> G" := (forall a, {hom F a -> G a}) : category_scope.
 Definition naturality (C D : category) (F G : {functor C -> D}) (f : F ~~> G) :=
-  forall a b (h : {hom a -> b}), (G # h) \o (f a) = (f b) \o (F # h).
+  forall a b (h : {hom a -> b}), (G # h) \c (f a) = (f b) \c (F # h).
 Arguments naturality [C D].
 HB.mixin Record isNatural
-    (C D : category) (F G : {functor C -> D}) (f : F ~~> G) :=
-  { natural : naturality F G f }.
+         (C D : category) (F G : {functor C -> D}) (f : F ~~> G) :=
+  {natural : naturality F G f}.
 #[short(type=nattrans)]
-HB.structure Definition _ (C D : category) (F G : {functor C -> D}) :=
+HB.structure Definition Nattrans
+             (C D : category) (F G : {functor C -> D}) :=
   {f of isNatural C D F G f}.
 Arguments natural [C D F G] phi : rename.
 Notation "F ~> G" := (nattrans F G) : category_scope.
@@ -359,30 +282,32 @@ Notation "F ~> G" := (nattrans F G) : category_scope.
 Section natural_transformation_lemmas.
 Import comps_notation.
 Variables (C D : category) (F G : {functor C -> D}).
-Lemma natural_head (phi : F ~> G) a b c (h : {hom a -> b}) (f : {hom c -> F a}) :
-  [\o G # h, phi a, f] = [\o phi b, F # h, f].
-Proof. by rewrite -!hom_compA natural. Qed.
+Lemma natural_tail (phi : F ~> G) a b c (h : {hom a -> b}) (f : {hom G b -> c}) :
+  [\c f, G # h, phi a] = [\c f, phi b, F # h].
+Proof. by rewrite -!assoc natural. Qed.
 
-Lemma nattrans_ext (f g : F ~> G) : f = g <-> forall a, (f a = g a :> (_ -> _)).
+Lemma nattrans_ext (f g : F ~> G) :
+  f = g <-> forall a, f a = g a.
 Proof.
-split=> [ -> // |]; move: f g => [f [[Hf]]] [g [[Hg]]] /= fg''.
-have fg' : forall a, f a = g a :> {hom _ -> _} by move=> a; rewrite hom_ext fg''.
+split => [ -> // |]; move: f g => [f [[Hf]]] [g [[Hg]]] /= fg''.
+have fg' : forall a, f a = g a by move=> a; rewrite fg''.
 move: (functional_extensionality_dep fg') => fg.
-by move: Hf Hg; rewrite fg=> Hf Hg; rewrite (proof_irr _ Hf Hg).
+by move: Hf Hg; rewrite fg=> Hf Hg; rewrite (proof_irr Hf Hg).
 Qed.
 End natural_transformation_lemmas.
-Arguments natural_head [C D F G].
+Arguments natural_tail [C D F G].
 
 Section id_natural_transformation.
 Variables (C D : category) (F : {functor C -> D}).
-Definition unnattrans_id := fun (a : C) => [hom (@idfun (el (F a)))].
+Definition unnattrans_id := fun (a : C) => id (F a).
 Definition natural_id : naturality _ _ unnattrans_id.
-Proof. by []. Qed.
+Proof. by move=> *; rewrite left_id right_id. Qed.
 
-HB.instance Definition _ := isNatural.Build C D F F unnattrans_id natural_id.
-Definition NId : F ~> F := [the _ ~> _ of unnattrans_id].
-Lemma NIdE : NId  = (fun a => [hom idfun]) :> (_ ~~> _).
-Proof. by []. Qed.
+HB.instance Definition _ :=
+  isNatural.Build C D F F unnattrans_id natural_id.
+Definition NId : F ~> F := locked (unnattrans_id : _ ~> _).
+Lemma NIdE : NId  = (fun a => id (F a)) :> (_ ~~> _).
+Proof. by rewrite /NId -lock. Qed.
 End id_natural_transformation.
 
 Module NEq.
@@ -393,29 +318,31 @@ Variable (Iobj : forall c, F c = G c).
 Local Notation tc := (transport_codom (Iobj _)).
 Local Notation td := (transport_dom (esym (Iobj _))).
 Variable (Imor : forall a b (f : {hom a -> b}), tc (F # f) = td (G # f)).
-Definition f : F ~~> G := fun (c : C) => tc [hom idfun].
+Definition f : F ~~> G := fun (c : C) => tc (id (F c)).
 Lemma natural : naturality F G f.
 Proof.
 move=> a b h.
-rewrite /f !transport_codomF 2!homcompE 2!compfid.
-have /hom_ext -> : [hom (hom_of_eq (Iobj b) \o F # h)] = [hom tc (F # h)]
+rewrite /f !transport_codomF !right_id.
+have -> : (hom_of_eq (Iobj b) \c F # h) = tc (F # h)
   by rewrite transport_codomF.
-by rewrite Imor transport_domF homfunK /= esymK.
+by rewrite Imor transport_domF /= esymK.
 Qed.
 
 HB.instance Definition _ := isNatural.Build C D F G f natural.
-Definition n : F ~> G := [the _ ~> _ of f].
+Definition n : F ~> G := f.
 End def.
 Module Exports.
+(*Arguments f [C D F G] c / : rename.*)
+Arguments f [C D F G] Iobj /.
 Arguments n [C D] : simpl never.
 Notation NEq := n.
-Lemma NEqE C D F G Iobj Imor : @NEq C D F G Iobj Imor =
-  (fun a => transport_codom (Iobj _) [hom idfun]) :> (_ ~~> _).
+Lemma NEqE C D F G Iobj Imor :
+  @NEq C D F G Iobj Imor =
+  (fun a => transport_codom (Iobj _) (id (F a))) :> (_ ~~> _).
 Proof. by []. Qed.
 End Exports.
 End NEq.
 Export NEq.Exports.
-
 Notation "[ 'NEq' F , G ]" :=
   (NEq F G (fun a => erefl) (fun a b f => erefl))
     (at level 0, format "[ 'NEq'  F ,  G ]") : category_scope.
@@ -423,49 +350,56 @@ Notation "[ 'NEq' F , G ]" :=
 Section vertical_composition.
 Variables (C D : category) (F G H : {functor C -> D}).
 Variables (g : G ~> H) (f : F ~> G).
-Definition vcomp := fun a => [hom g a \o f a].
+Definition vcomp := fun a => g a \c f a.
 Definition natural_vcomp : naturality _ _ vcomp.
-Proof. by move=> A B h; rewrite compA (natural g) -compA (natural f). Qed.
-
+Proof. by move=> a b h; rewrite assoc (natural g) -assoc (natural f) -assoc. Qed.
 HB.instance Definition _ := isNatural.Build C D F H
   vcomp natural_vcomp.
-Definition VComp : F ~> H := [the F ~> H of vcomp].
+Definition VComp : F ~> H := vcomp.
 End vertical_composition.
-Notation "f \v g" := (VComp f g).
+Notation "f \v g" := (locked (VComp f g)).
 
 Section vcomp_lemmas.
+Variables (C D : category) (F G H : {functor C -> D}).
+Variables (g : G ~> H) (f : F ~> G).
+Lemma VCompE_nat : g \v f = (fun a => g a \c f a) :> (_ ~~> _).
+Proof. by unlock. Qed.
+Lemma VCompE a : (g \v f) a = g a \c f a.
+Proof. by unlock. Qed.
+End vcomp_lemmas.
+
+Section vcomp_lemmas2.
 Variables (C D : category) (F G H I : {functor C -> D}).
 Variables (h : H ~> I) (g : G ~> H) (f : F ~> G).
+
 Lemma VCompId : f \v NId F = f.
-Proof. by apply nattrans_ext. Qed.
+Proof. by apply nattrans_ext=> a; rewrite VCompE NIdE right_id. Qed.
 Lemma VIdComp : NId G \v f = f.
-Proof. by apply nattrans_ext. Qed.
+Proof. by apply nattrans_ext=> a; rewrite VCompE NIdE left_id. Qed.
 Lemma VCompA : (h \v g) \v f = h \v (g \v f).
-Proof. by apply nattrans_ext. Qed.
-Lemma VCompE_nat : g \v f = (fun a => [hom g a \o f a]) :> (_ ~~> _).
-Proof. by []. Qed.
-Lemma VCompE a : (g \v f) a = g a \o f a :> (_ -> _).
-Proof. by []. Qed.
-End vcomp_lemmas.
+Proof. by apply nattrans_ext=> a; rewrite !VCompE !assoc. Qed.
+End vcomp_lemmas2.
 
 Section horizontal_composition.
 Variables (C D E : category) (F G : {functor C -> D}) (F' G' : {functor D -> E}).
 Variables (s : F ~> G) (t : F' ~> G').
 
-Definition hcomp : F' \O F ~~> G' \O G :=
-  fun (c : C) => [hom t (G c) \o F' # s c].
-Lemma natural_hcomp : naturality (F' \O F) (G' \O G) hcomp.
+Definition hcomp : F' \o F ~~> G' \o G :=
+  fun (c : C) => t (G c) \c F' # s c.
+Lemma natural_hcomp : naturality (F' \o F) (G' \o G) hcomp.
 Proof.
 move=> c0 c1 h.
-rewrite [in LHS]compA (natural t) -[in LHS]compA -[in RHS]compA; congr (_ \o _).
-rewrite [in RHS]FCompE -2!functor_o; congr (F' # _); apply hom_ext => /=.
+rewrite [in LHS]assoc (natural t) -[in LHS]assoc -[in RHS]assoc; congr (_ \c _).
+rewrite [in RHS]FCompE.
+rewrite -2!(@Fhom_comp D). (* TODO: why must D be explicit? *)
+congr (F' # _).
 by rewrite natural.
 Qed.
 
-HB.instance Definition _ := isNatural.Build C E (F' \O F) (G' \O G)
+HB.instance Definition _ := isNatural.Build C E (F' \o F) (G' \o G)
   hcomp natural_hcomp.
 
-Definition HComp : F' \O F ~> G' \O G := [the _ ~> _ of hcomp].
+Definition HComp : F' \o F ~> G' \o G := hcomp.
 End horizontal_composition.
 Notation "f \h g" := (locked (HComp g f)).
 
@@ -473,9 +407,9 @@ Section hcomp_extensionality_lemmas.
 Variables (C D E : category) (F G : {functor C -> D}) (F' G' : {functor D -> E}).
 Variables (s : F ~> G) (t : F' ~> G').
 Lemma HCompE_def : t \h s = HComp s t. Proof. by unlock. Qed.
-Lemma HCompE c : (t \h s) c = t (G c) \o F' # s c :> (_ -> _).
+Lemma HCompE c : (t \h s) c = t (G c) \c F' # s c.
 Proof. by unlock. Qed.
-Lemma HCompE_alt c : (t \h s) c = G' # (s c) \o t (F c) :> (_ -> _).
+Lemma HCompE_alt c : (t \h s) c = G' # (s c) \c t (F c).
 Proof. by rewrite HCompE natural. Qed.
 End hcomp_extensionality_lemmas.
 
@@ -486,24 +420,23 @@ Variables (F G : {functor C -> D}) (F' G' : {functor D -> E}) (F'' G'' : {functo
 Variables (s : F ~> G) (t : F' ~> G') (u : F'' ~> G'').
 
 Lemma HCompId c : (t \h NId F) c = t (F c).
-Proof. by rewrite hom_ext HCompE NIdE functor_id compfid. Qed.
+Proof. by rewrite HCompE NIdE Fhom_id right_id. Qed.
 Lemma HIdComp c : (NId G' \h s) c = G' # s c.
-Proof. by rewrite hom_ext HCompE NIdE compidf. Qed.
+Proof. by rewrite HCompE NIdE left_id. Qed.
 (* TODO: introduce the application of a functor to a natural transformation? *)
 
-Let HCompA_def : (u \h t) \h s =
-  [NEq G'' \O (G' \O G) , (G'' \O G') \O G]
+Lemma HCompA c : ((u \h t) \h s) c = (u \h (t \h s)) c.
+Proof. by rewrite !HCompE -assoc FCompE Fhom_comp. Qed.
+
+Lemma HCompA_nat : (u \h t) \h s =
+  [NEq G'' \o (G' \o G) , (G'' \o G') \o G]
   \v (u \h (t \h s))
-  \v [NEq (F'' \O F') \O F , F'' \O (F' \O F)].
+  \v [NEq (F'' \o F') \o F , F'' \o (F' \o F)].
 Proof.
-apply nattrans_ext => c /=.
-rewrite compidf compfid [in LHS]HCompE [in RHS]HCompE.
-rewrite [in LHS]HCompE hom_compA -functor_o; congr [\o _, _].
-by congr (_ # _); apply hom_ext; rewrite HCompE.
+apply nattrans_ext => c.
+rewrite 2!VCompE /= left_id right_id.
+by rewrite HCompA.
 Qed.
-Lemma HCompA c : ((u \h t) \h s) c = (u \h (t \h s)) c.
-Proof. by rewrite hom_ext HCompA_def. Qed.
-
 End hcomp_id_assoc_lemmas.
 
 Section hcomp_lemmas.
@@ -520,20 +453,28 @@ Proof.
 by apply nattrans_ext=> a; rewrite VCompE HCompE HIdComp HCompId -natural.
 Qed.
 
-Lemma NIdFId c : NId (@FId C) c = [hom idfun].
-Proof. by []. Qed.
+Lemma NIdFId c : NId (@FId C) c = [id].
+Proof. by rewrite NIdE. Qed.
 
-Lemma NIdFComp : NId (F' \O F) = NId F' \h NId F.
-Proof. by apply nattrans_ext => c /=; rewrite HCompE /= compidf functor_id. Qed.
+Lemma NIdFComp : NId (F' \o F) = (NId F') \h (NId F).
+Proof.
+by apply nattrans_ext => c /=; rewrite HCompE !NIdE /= left_id Fhom_id.
+Qed.
+End hcomp_lemmas.
 
+Section hcomp_lemmas.
 (* horizontal and vertical compositions interchange *)
-Variables (H : {functor C -> D}) (H' : {functor D -> E}).
+Variables (C D E : category).
+Variables (F G H : {functor C -> D}) (F' G' H' : {functor D -> E}).
+Variables (s : F ~> G) (t : F' ~> G').
 Variables (s' : G ~> H) (t' : G' ~> H').
 Lemma HCompACA : (t' \h s') \v (t \h s) = (t' \v t) \h (s' \v s).
 Proof.
+rewrite (HComp_VH s' t') (HComp_VH s t).
+rewrite -VCompA (VCompA (t' \h NId H)) -HComp_VH_aux (HComp_VH s' t).
 apply nattrans_ext => c /=.
-rewrite !HCompE !VCompE -compA -[in RHS]compA; congr (_ \o _).
-by rewrite natural_head -functor_o.
+rewrite !HCompE !VCompE !HCompE !NIdE /= !left_id !Fhom_id !right_id.
+by rewrite -!assoc Fhom_comp.
 Qed.
 End hcomp_lemmas.
 
@@ -543,9 +484,13 @@ End hcomp_lemmas.
 Module TriangularLaws.
 Section triangularlaws.
 Variables (C D : category) (F : {functor C -> D}) (G : {functor D -> C}).
-Variables (eta : FId ~> G \O F) (eps : F \O G ~> FId).
-Definition left := forall c, eps (F c) \o F # (eta c) = idfun.
-Definition right := forall d, G # (eps d) \o eta (G d) = idfun.
+Variables (eta : FId ~> G \o F) (eps : F \o G ~> FId).
+Definition left := forall c, eps (F c) \c F # (eta c) = [id].
+Definition right := forall d, G # (eps d) \c eta (G d) = [id].
+Definition left_tail := forall c d (k : {hom F c -> d}),
+    k \c eps (F c) \c F # (eta c) = k.
+Definition right_tail := forall c d (k : {hom G d -> c}),
+    k \c G # (eps d) \c eta (G d) = k.
 End triangularlaws.
 End TriangularLaws.
 
@@ -553,8 +498,8 @@ Module AdjointFunctors.
 Section def.
 Variables (C D : category) (F : {functor C -> D}) (G : {functor D -> C}).
 Record t := mk {
-  eta : FId ~> G \O F ;
-  eps : F \O G ~> FId ;
+  eta : FId ~> G \o F ;
+  eps : F \o G ~> FId ;
   triL : TriangularLaws.left eta eps ;
   triR : TriangularLaws.right eta eps
 }.
@@ -564,23 +509,29 @@ Local Notation "F -| G" := (t F G).
 Variables (C D : category) (F : {functor C -> D}) (G : {functor D -> C}).
 Variable A : F -| G.
 
+Lemma triL_tail : TriangularLaws.left_tail (eta A) (eps A).
+Proof. by move=> ? ? ?; rewrite -assoc triL right_id. Qed.
+
+Lemma triR_tail : TriangularLaws.right_tail (eta A) (eps A).
+Proof. by move=> ? ? ?; rewrite -assoc triR right_id. Qed.
+
 Definition hom_iso c d : {hom F c -> d} -> {hom c -> G d} :=
-  fun h => [hom (G # h) \o (eta A c)].
+  fun h => (G # h) \c (eta A c).
 
 Definition hom_inv c d : {hom c -> G d} -> {hom F c -> d} :=
-  fun h => [hom (eps A d) \o (F # h)].
+  fun h => (eps A d) \c (F # h).
 
 Import comps_notation.
 
 Lemma hom_isoK (c : C) (d : D) (f : {hom F c -> d}) : hom_inv (hom_iso f) = f.
 Proof.
-rewrite /hom_inv /hom_iso; apply hom_ext => /=.
-by rewrite functor_o -(natural_head (eps _)) triL.
+rewrite /hom_inv /hom_iso.
+by rewrite Fhom_comp !assoc -(natural (eps _)) triL_tail FIdf.
 Qed.
 Lemma hom_invK (c : C) (d : D) (g : {hom c -> G d}) : hom_iso (hom_inv g) = g.
 Proof.
-rewrite /hom_inv /hom_iso; apply hom_ext => /=.
-by rewrite functor_o hom_compA (natural (eta A)) -hom_compA triR.
+rewrite /hom_inv /hom_iso.
+by rewrite Fhom_comp (natural_tail (eta _)) triR FIdf left_id.
 Qed.
 
 Lemma hom_iso_inj (c : C) (d : D) : injective (@hom_iso c d).
@@ -588,10 +539,10 @@ Proof. exact: can_inj (@hom_isoK c d). Qed.
 Lemma hom_inv_inj (c : C) (d : D) : injective (@hom_inv c d).
 Proof. exact: can_inj (@hom_invK c d). Qed.
 
-Lemma eta_hom_iso (c : C) : eta A c = hom_iso [hom idfun].
-Proof. by apply hom_ext; rewrite /hom_iso /= functor_id. Qed.
-Lemma eps_hom_inv (d : D) : eps A d = hom_inv [hom idfun].
-Proof. by apply hom_ext; rewrite /hom_inv /= functor_id compfid. Qed.
+Lemma eta_hom_iso (c : C) : eta A c = hom_iso [id].
+Proof. by rewrite /hom_iso /= Fhom_id left_id. Qed.
+Lemma eps_hom_inv (d : D) : eps A d = hom_inv [id].
+Proof. by rewrite /hom_inv /= Fhom_id right_id. Qed.
 
 Lemma ext (B : F -| G) : eta A = eta B -> eps A = eps B -> A = B.
 Proof.
@@ -614,6 +565,7 @@ Arguments hom_inv_inj [C D F G].
 End AdjointFunctors.
 Notation "F -| G" := (AdjointFunctors.t F G).
 
+
 Module AdjComp.
 Section def.
 Import comps_notation.
@@ -621,67 +573,57 @@ Variables C0 C1 C2 : category.
 Variables (F0 : {functor C0 -> C1}) (G0 : {functor C1 -> C0}).
 Variables (F1 : {functor C1 -> C2}) (G1 : {functor C2 -> C1}).
 Variables
-  (eta0 : FId ~> G0 \O F0) (eta1 : FId ~> G1 \O F1)
-  (eps0 : F0 \O G0 ~> FId) (eps1 : F1 \O G1 ~> FId)
+  (eta0 : FId ~> G0 \o F0) (eta1 : FId ~> G1 \o F1)
+  (eps0 : F0 \o G0 ~> FId) (eps1 : F1 \o G1 ~> FId)
   (triL0 : TriangularLaws.left eta0 eps0)
   (triL1 : TriangularLaws.left eta1 eps1)
   (triR0 : TriangularLaws.right eta0 eps0)
   (triR1 : TriangularLaws.right eta1 eps1).
 
-Definition F := F1 \O F0.
-Definition G := G0 \O G1.
+Definition F := F1 \o F0.
+Definition G := G0 \o G1.
 
-Definition Eta : FId ~> G \O F :=
-  [NEq G0 \O (G1 \O F1) \O F0 , G \O F]
+Definition Eta : FId ~> G \o F :=
+  [NEq G0 \o (G1 \o F1) \o F0 , G \o F]
     \v (NId G0 \h eta1 \h NId F0)
-    \v [NEq G0 \O F0 , G0 \O FId \O F0]
+    \v [NEq G0 \o F0 , G0 \o FId \o F0]
     \v eta0.
-Lemma EtaE a : Eta a = G0 # (eta1 (F0 a)) \o (eta0 a) :> (_ -> _).
-Proof. by cbn; rewrite HCompId HIdComp. Qed.
-Lemma EtaE_hom a : Eta a = [hom G0 # (eta1 (F0 a)) \o (eta0 a)].
-Proof. by rewrite hom_ext EtaE. Qed.
+Lemma EtaE a : Eta a = G0 # (eta1 (F0 a)) \c (eta0 a).
+Proof. by rewrite !VCompE /= left_id right_id HCompId HIdComp. Qed.
 
-Definition Eps : F \O G ~> FId :=
+Definition Eps : F \o G ~> FId :=
   (eps1)
-    \v [NEq F1 \O FId \O G1 , F1 \O G1]
+    \v [NEq F1 \o FId \o G1 , F1 \o G1]
     \v (NId F1 \h eps0 \h NId G1)
-    \v [NEq F \O G , (F1 \O (F0 \O G0)) \O G1].
-Lemma EpsE a : Eps a = (eps1 _) \o F1 # (eps0 (G1 a)) :> (_ -> _).
-Proof. by cbn; rewrite HCompId HIdComp. Qed.
-Lemma EpsE_hom a : Eps a = [hom (eps1 _) \o F1 # (eps0 (G1 a))].
-Proof. by rewrite hom_ext EpsE. Qed.
+    \v [NEq F \o G , (F1 \o (F0 \o G0)) \o G1].
+Lemma EpsE a : Eps a = (eps1 _) \c F1 # (eps0 (G1 a)).
+Proof. by rewrite !VCompE /= !right_id HCompId HIdComp. Qed.
 
 Lemma triL : TriangularLaws.left Eta Eps.
 Proof.
 (* NB(tanaka): This proof does NOT follow the manner of 2-category, for now. *)
-move=> c; rewrite EpsE EtaE_hom hom_compA (functor_o F) /F -(functor_o_head F1).
-set X := [hom [\o _, _]].
-evar (TY : Type).
-evar (Y : TY).
-have-> : F1 # X = F1 # Y
-  by congr (F1 # _); rewrite hom_ext /X /= -(natural eps0); exact: erefl.
-rewrite (functor_o_head F1) FIdf.
-rewrite -!hom_compA triL1 compidf.
-rewrite -[in RHS](functor_id F1) -(functor_o F1); congr (F1 # _).
-by rewrite hom_ext /= triL0.
+move=> c/=.
+rewrite EpsE EtaE.
+rewrite (Fhom_comp_tail F).
+rewrite -(Fhom_comp_tail F1 (eps0 _)).
+rewrite -(natural eps0) FIdf.
+rewrite Fhom_comp !assoc triL1 left_id.
+by rewrite -(Fhom_comp F1) triL0 Fhom_id.
 Qed.
 
 Lemma triR : TriangularLaws.right Eta Eps.
 Proof.
 move=> c.
-rewrite EpsE_hom EtaE (functor_o_head G) -(functor_o_head G0 (eta0 _)).
-(* FRAGILE!
-   simpl here breaks the notation and renders the following set X impossible *)
-set X:= [hom [\o _, _]].
-evar (TY : Type).
-evar (Y : TY).
-have-> : G0 # X = G0 # Y
-  by congr (G0 # _); rewrite hom_ext /X /= (natural eta1); exact: erefl.
-rewrite (functor_o G0) hom_compA FIdf triR0 compfid.
-rewrite -[in RHS](functor_id G0) -(functor_o G0); congr (G0 # _).
-by rewrite hom_ext /= triR1.
+rewrite EpsE EtaE.
+rewrite (Fhom_comp G)/= !assoc.
+rewrite -(Fhom_comp_tail G0).
+rewrite (natural eta1) FIdf.
+rewrite Fhom_comp -!assoc triR0 right_id.
+by rewrite -(Fhom_comp G0) triR1 Fhom_id.
 Qed.
+
 End def.
+
 Module Exports.
 Section adj_comp.
 Variables (C0 C1 C2 : category).
@@ -698,253 +640,172 @@ Export AdjComp.Exports.
 Module JoinLaws.
 Section join_laws.
 Variables (C : category) (M : {functor C -> C}) .
-Variables (ret : FId ~~> M) (join : M \O M ~~> M).
+Variables (ret : FId ~~> M) (join : M \o M ~~> M).
 Definition left_unit :=
-  forall a, join a \o ret (M a) = idfun :> (el (M a) -> el (M a)).
+  forall a, join a \c ret (M a) = [id].
 Definition right_unit :=
-  forall a, join a \o M # ret a = idfun :> (el (M a) -> el (M a)).
+  forall a, join a \c M # ret a = [id].
 Definition associativity :=
-  forall a, join a \o M # join a = join a \o join (M a) :> (el (M (M (M a))) -> el (M a)).
+  forall a, join a \c M # join a = join a \c join (M a).
 End join_laws.
 End JoinLaws.
 
 Module BindLaws.
-Section bindlaws.
-Variables (C : category) (M : C -> C).
-Variable b : forall A B, {hom A -> M B} -> {hom M A -> M B}.
-Local Notation "m >>= f" := (b f m).
 (*
 bind is usually typed in the literature as follows:
 
-Variable b : forall A B, M A -> (A -> M B) -> M B.
-Local Notation "m >>= f" := (b m f).
+bind : forall A B, M A -> (A -> M B) -> M B.
+Notation "m >>= f" := (b m f).
 
-This does not work well since it does not keep the {hom _ -> _} structure
-in the result.
+We use a different type to keep the {hom _ -> _} structures:
+
+bind : forall a b, {hom a -> M b} -> {hom M a -> M b}.
+Notation "m >>= f" := (fn (bind f) m).
 *)
-Fact associative_aux x y z (f : {hom x -> M y}) (g : {hom y -> M z}) :
-  (fun w => (f w >>= g)) = (b g \o f).
-Proof. by []. Qed.
-Definition associative := forall A B C (m : el (M A)) (f : {hom A -> M B}) (g : {hom B -> M C}),
-  (m >>= f) >>= g = m >>= [hom b g \o f].
-Definition left_neutral (r : forall A, {hom A -> M A}) :=
-  forall A B (f : {hom A -> M B}), [hom (b f \o r A)] = f.
-Definition right_neutral (r : forall A, {hom A -> M A}) :=
-  forall A (m : el (M A)), m >>= r _ = m.
-End bindlaws.
+Section abscat.
+Variables (C : category) (*M : {functor C -> C}*) (M : C -> C).
+Variable bind : forall a b, {hom a -> M b} -> {hom M a -> M b}.
+Variable ret : forall a, {hom a -> M a}.
+
+Definition associative :=
+  forall a b c (f : {hom a -> M b}) (g : {hom b -> M c}),
+  bind g \c bind f = bind (bind g \c f).
+Definition left_neutral :=
+  forall a b (f : {hom a -> M b}), (bind f \c ret a) = f.
+Definition right_neutral :=
+  forall a, bind (ret a) = [id].
+End abscat.
 
-Section misc_laws_on_Type_monad.
-Variable M : {functor CT -> CT}.
-Variable b : forall A B, (A -> M B) -> M A -> M B.
-Local Notation "m >>= f" := (b f m).
-Definition bind_right_distributive (add : forall B, M B -> M B -> M B) :=
-  forall A B (m : M A) (k1 k2 : A -> M B),
-    m >>= (fun x => add _ (k1 x) (k2 x)) = add _ (m >>= k1) (m >>= k2).
-Definition bind_left_distributive (add : forall B, M B -> M B -> M B) :=
-  forall A B (m1 m2 : M A) (k : A -> M B),
-    (add _ m1 m2) >>= k = add _ (m1 >>= k) (m2 >>= k).
-Definition right_zero (f : forall A, M A) :=
-  forall A B (g : M B), g >>= (fun _ => f A) = f A.
-Definition left_zero (f : forall A, M A) := forall A B g, f A >>= g = f B.
-Definition left_id (r : forall A, M A) (add : forall B, M B -> M B -> M B) :=
-  forall A (m : M A), add _ (r _) m = m.
-Definition right_id (r : forall A, M A) (add : forall B, M B -> M B -> M B) :=
-  forall A (m : M A), add _ m (r _) = m.
-End misc_laws_on_Type_monad.
 End BindLaws.
 
-Section bind_lemmas.
-Variables (C : category) (M : C -> C).
-Variable b : forall A B, {hom A -> M B} -> {hom M A -> M B}.
-Local Notation "m >>= f" := (b f m).
-Lemma bind_left_neutral_hom_fun (r : forall A, {hom A -> M A})
-  : BindLaws.left_neutral b r
-    <-> forall A B (f : {hom A -> M B}), b f \o r A = f.
-Proof. by split; move=> H A B f; move: (H A B f); move/hom_ext. Qed.
-End bind_lemmas.
-
-(*
-The following definition of the structure fails with:
-Error: HB: coercion not to Sortclass or Funclass not supported yet.
-
-HB.mixin Record isMonad (C : category) (M : {functor C -> C}) := {
-  ret : FId ~> M ;
-  join : M \O M ~> M ;
-  bind : forall (a b : C), {hom a -> M b} -> {hom M a -> M b} ;
-  bindE : forall (a b : C) (f : {hom a -> M b}) (m : el (M a)),
-    bind a b f m = join b ((M # f) m) ;
-  joinretM : JoinLaws.left_unit ret join ;
-  joinMret : JoinLaws.right_unit ret join ;
-  joinA : JoinLaws.associativity join
-}.
-HB.structure Definition Monad (C : category) := {M of isMonad C M}.
-*)
-
 HB.mixin Record isMonad (C : category) (M : C -> C) of @Functor C C M := {
-  ret : FId ~> [the {functor C -> C} of M] ;
-  join : [the {functor C -> C} of M] \O [the {functor C -> C} of M] ~>
-         [the {functor C -> C} of M] ;
+  ret : FId ~> M ;
+  join : M \o M ~> M ;
   bind : forall (a b : C), {hom a -> M b} -> {hom M a -> M b} ;
-  bindE : forall (a b : C) (f : {hom a -> M b}) (m : el (M a)),
-    bind a b f m = join b (([the {functor C -> C} of M] # f) m) ;
+  bindE : forall (a b : C) (f : {hom a -> M b}),
+    bind a b f = join b \c M # f ;
   joinretM : JoinLaws.left_unit ret join ;
   joinMret : JoinLaws.right_unit ret join ;
   joinA : JoinLaws.associativity join
 }.
 #[short(type=monad)]
-HB.structure Definition Monad (C : category) :=
-  {M of isMonad C M & isFunctor C C M}.
+HB.structure Definition Monad (C : category) := {M of isMonad C M &}.
 Arguments bind {C M a b} : rename, simpl never.
 Notation "m >>= f" := (bind f m).
 
 Section monad_interface.
 Variable (C : category) (M : monad C).
-(* *_head lemmas are for [fun of f] \o ([fun of g] \o ([fun of h] \o ..))*)
+(* *_tail lemmas are for g and h in ((f \c .. \c g) \c h) *)
 Import comps_notation.
-Lemma joinretM_head a (c : C) (f : {hom c -> M a}) : [\o join _, ret _, f] = f.
-Proof. by rewrite compA joinretM. Qed.
-Lemma joinMret_head a (c : C) (f : {hom c -> M a}) : [\o join _, M # ret _, f] = f.
-Proof. by rewrite compA joinMret. Qed.
-Lemma joinA_head a (c : C) (f : {hom c -> M (M (M a))}) :
-  [\o join _, M # join _, f] = [\o join _, join _, f].
-Proof. by rewrite compA joinA. Qed.
+Lemma fmap_bindret (a b : C) (f : {hom a -> b}) : M # f = bind (ret b \c f).
+Proof. by rewrite bindE Fhom_comp assoc joinMret left_id. Qed.
+Lemma joinretM_tail a (c : C) (f : {hom M a -> c}) : [\c f, join _, ret _] = f.
+Proof. by rewrite -assoc joinretM right_id. Qed.
+Lemma joinMret_tail a (c : C) (f : {hom M a -> c}) : [\c f, join _, M # ret _] = f.
+Proof. by rewrite -assoc joinMret right_id. Qed.
+Lemma joinA_tail a (c : C) (f : {hom M (M (M a)) -> c}) :
+  [\c f, join _, M # join _] = [\c f, join _, join _].
+Proof. by rewrite -assoc joinA assoc. Qed.
 End monad_interface.
 
 HB.factory Record Monad_of_ret_join (C : category) (M : C -> C)
            of @Functor C C M := {
-  ret : FId ~> [the {functor C -> C} of M] ;
-  join : M \O M ~> [the {functor C -> C} of M] ;
+  ret : FId ~> M ;
+  join : M \o M ~> M ;
   joinretM : JoinLaws.left_unit ret join ;
   joinMret : JoinLaws.right_unit ret join ;
   joinA : JoinLaws.associativity join
 }.
 HB.builders Context C M of Monad_of_ret_join C M.
-Let F := [the {functor _ -> _} of M].
-Let bind (a b : C) (f : {hom a -> M b}) : {hom M a -> M b} := [hom join _ \o (F # f)].
-Let bindE (a b : C) (f : {hom a -> M b}) (m : el (M a)) :
-    bind f m = join b (([the {functor C -> C} of M] # f) m).
+Let F := M : {functor _ -> _}.
+Let bind (a b : C) (f : {hom a -> M b}) : {hom M a -> M b} := join _ \c (F # f).
+Let bindE (a b : C) (f : {hom a -> M b}) :
+    bind f = join b \c M # f.
 Proof. by []. Qed.
 HB.instance Definition _ := isMonad.Build C M bindE joinretM joinMret joinA.
 HB.end.
 
-(* Monads defined by ret and bind; M need not be a priori a functor *)
-HB.factory Record Monad_of_ret_bind (C : category) (acto : C -> C) := {
-  ret' : forall a, {hom a -> acto a} ;
-  bind : forall (a b : C), {hom a -> acto b} -> {hom acto a -> acto b} ;
-  bindretf : BindLaws.left_neutral bind ret' ;
-  bindmret : BindLaws.right_neutral bind ret' ;
+
+HB.factory Record Monad_of_ret_bind (C : category) (M : C -> C) :=
+{
+  ret : forall a, {hom a -> M a} ;
+  bind : forall (a b : C), {hom a -> M b} -> {hom M a -> M b} ;
+  bindfret : BindLaws.left_neutral bind ret ;
+  bindret : BindLaws.right_neutral bind ret ;
   bindA : BindLaws.associative bind ;
 }.
+
 HB.builders Context C M of Monad_of_ret_bind C M.
-Let fmap a b (f : {hom a -> b}) := bind [hom ret' b \o f].
-Let bindretf_fun : (forall (a b : C) (f : {hom a -> M b}),
-  bind f \o ret' a = f).
-Proof. by apply/bind_left_neutral_hom_fun/bindretf. Qed.
+
+Let fmap a b (f : {hom a -> b}) := bind (ret b \c f).
 Let fmap_id : FunctorLaws.id fmap.
-Proof.
-move=> A; apply/hom_ext/funext=>m. rewrite /fmap.
-rewrite/idfun/=.
-rewrite -[in RHS](bindmret m).
-congr (fun f => bind f m).
-by rewrite hom_ext.
-Qed.
+Proof. by move=> ?; rewrite /fmap right_id bindret. Qed.
 Let fmap_o : FunctorLaws.comp fmap.
-Proof.
-move=> a b c g h; apply/hom_ext/funext=>m; rewrite /fmap/=.
-rewrite bindA/=.
-congr (fun f => bind f m); rewrite hom_ext/=.
-by rewrite -[in RHS]hom_compA bindretf_fun.
-Qed.
+Proof. by move=> a b c g h; rewrite /fmap bindA !assoc bindfret. Qed.
 HB.instance Definition _ := isFunctor.Build _ _ _ fmap_id fmap_o.
-Notation F := [the {functor _ -> _} of M].
-Let ret'_naturality : naturality FId F ret'.
-Proof. by move=> A B h; rewrite FIdf bindretf_fun. Qed.
-HB.instance Definition _ := isNatural.Build _ _ FId F
-  (ret' : FId ~~> M)(*NB: fails without this type constraint*) ret'_naturality.
-Definition ret := [the FId ~> F of ret'].
-Let join' : F \O F ~~> F := fun _ => bind [hom idfun].
-Let fmap_bind a b c (f : {hom a ->b}) m (g : {hom c ->F a}) :
-  (fmap f) (bind g m) = bind [hom fmap f \o g] m.
-Proof. by rewrite /fmap bindA. Qed.
-Let join'_naturality : naturality (F \O F) F join'.
-Proof.
-move => A B h.
-rewrite /join /= funeqE => m /=.
-rewrite fmap_bind bindA /=.
-congr (fun f => bind f m).
-rewrite hom_ext/=.
-rewrite -[in RHS]hom_compA.
-by rewrite bindretf_fun.
-Qed.
-HB.instance Definition _ := isNatural.Build _ _ _ _ _ join'_naturality.
-Definition join := [the F \O F ~> F of join'].
 
-Let bind_fmap a b c (f : {hom a -> b}) (m : el (F a)) (g : {hom b -> F c}) :
-  bind g (fmap f m) = bind [hom g \o f] m .
-Proof.
-rewrite bindA /=; congr (fun f => bind f m); apply hom_ext => /=.
-by rewrite -hom_compA bindretf_fun.
-Qed.
-Lemma bindE (a b : C) (f : {hom a -> F b}) (m : el (F a)) :
-  bind f m = join b (([the {functor C -> C} of F] # f) m).
+Let fmapE a b (f : {hom a -> b}) : M # f = bind (ret b \c f).
+Proof. by []. Qed.
+Let ret_naturality : naturality FId M ret.
+Proof. by move=> A B h; rewrite bindfret. Qed.
+HB.instance Definition _ :=
+  isNatural.Build _ _ FId M (ret : FId ~~> M) ret_naturality.
+
+Let join : M \o M ~~> M := fun _ => bind [id].
+Let join_naturality : naturality (M \o M) M join.
 Proof.
-rewrite /join /=.
-rewrite /=bind_fmap/idfun/=.
-congr (fun f => bind f m).
-by rewrite hom_ext.
+move=> a b h.
+rewrite /Fhom/= /fmap /join/=.
+rewrite -(natural ret)/=.
+rewrite !bindA/= !bindfret right_id.
+by rewrite assoc bindfret left_id.
 Qed.
+HB.instance Definition _ := isNatural.Build _ _ _ _ _ join_naturality.
+
+Let bind_fmap a b c (f : {hom a -> b}) (g : {hom b -> M c}) :
+  bind g \c (fmap f) = bind (g \c f).
+Proof. by rewrite /= bindA assoc bindfret. Qed.
+Lemma bindE (a b : C) (f : {hom a -> M b}) : bind f = join b \c M # f.
+Proof. by rewrite bind_fmap left_id. Qed.
 Lemma joinretM : JoinLaws.left_unit ret join.
-Proof. by rewrite /join => A; rewrite bindretf_fun. Qed.
-Let bind_fmap_fun a b c (f : {hom a ->b}) (g : {hom b -> F c}) :
-  bind g \o fmap f = bind [hom g \o f].
-Proof. rewrite funeqE => ?; exact: bind_fmap. Qed.
+Proof. by move=> ?; rewrite /join bindfret. Qed.
 Lemma joinMret : JoinLaws.right_unit ret join.
-Proof.
-rewrite /join => A; rewrite funeqE => ma.
-rewrite bind_fmap_fun/= -[in RHS](bindmret ma).
-congr (fun f => bind f ma).
-by rewrite hom_ext.
-Qed.
+Proof. by move=> ?; rewrite /join/= bind_fmap left_id bindret. Qed.
 Lemma joinA : JoinLaws.associativity join.
-Proof.
-move => A; rewrite funeqE => mmma.
-rewrite /join.
-rewrite bind_fmap_fun/= bindA/=.
-congr (fun f => bind f mmma).
-by rewrite hom_ext.
-Qed.
+Proof. by move=> ?; rewrite /join/= bind_fmap left_id bindA right_id. Qed.
+
 HB.instance Definition _ := isMonad.Build C M bindE joinretM joinMret joinA.
 HB.end.
 
 Module _Monad_of_adjoint_functors.
-Section def.
+Section mixin.
 Import comps_notation.
 Variables C D : category.
 Variables (F : {functor C -> D}) (G : {functor D -> C}).
 Variable A : F -| G.
 Definition eps := AdjointFunctors.eps A.
 Definition eta := AdjointFunctors.eta A.
-Definition M := G \O F.
-Definition join : M \O M ~~> M := fun a => G # (eps (F a)).
+Definition M := G \o F.
+Definition join : M \o M ~~> M := fun a => G # (eps (F a)).
 Definition ret : FId ~~> M := fun a => eta a.
 Let triL := AdjointFunctors.triL A.
 Let triR := AdjointFunctors.triR A.
 Lemma naturality_ret : naturality FId M ret.
 Proof. by move=> *; rewrite (natural eta). Qed.
 HB.instance Definition _ := isNatural.Build C C FId M ret naturality_ret.
-Lemma naturality_join : naturality (M \O M) M join.
+Lemma naturality_join : naturality (M \o M) M join.
 Proof.
 rewrite /join => a b h.
-rewrite /M !FCompE -2!(functor_o G); congr (G # _).
-by rewrite hom_ext /= (natural eps).
+rewrite /M !FCompE -2!(Fhom_comp G); congr (G # _).
+exact: (natural eps).
 Qed.
-HB.instance Definition _ := isNatural.Build C C (M \O M) M join naturality_join.
+HB.instance Definition _ := isNatural.Build C C (M \o M) M join naturality_join.
 Let joinE : join = fun a => G # (@eps (F a)).
 Proof. by []. Qed.
-Let join_associativity' a : join a \o join (M a) = join a \o (M # join a).
+Let join_associativity' a : join a \c join (M a) = join a \c (M # join a).
 Proof.
-rewrite joinE -2!(functor_o G).
-by congr (G # _); rewrite hom_ext /= (natural eps).
+rewrite joinE -2!(Fhom_comp G).
+by congr (G # _); exact: (natural eps).
 Qed.
 Lemma join_associativity : JoinLaws.associativity join.
 Proof. by move=> a; rewrite join_associativity'. Qed.
@@ -952,99 +813,53 @@ Lemma join_left_unit : JoinLaws.left_unit ret join.
 Proof. by move=> a; rewrite joinE triR. Qed.
 Lemma join_right_unit : JoinLaws.right_unit ret join.
 Proof.
-move=> a; rewrite joinE. rewrite /M FCompE.
-rewrite /= -functor_o -[in RHS]functor_id.
+move=> a; rewrite joinE /M FCompE/= -Fhom_comp -[in RHS]Fhom_id.
 congr (G # _).
-by rewrite hom_ext/= triL.
+exact: triL.
 Qed.
-(*TODO: make this go through
-HB.instance Definition _ :=
- Monad_of_ret_join.Build  join_left_unit join_right_unit join_associativity.*)
-Let bind (a b : C) (f : {hom a -> M b}) : {hom M a -> M b} :=
-  [hom join _ \o (M # f)].
-Let bindE (a b : C) (f : {hom a -> M b}) (m : el (M a)) :
-  bind f m = join b (([the {functor C -> C} of M] # f) m).
-Proof. by []. Qed.
-HB.instance Definition monad_of_adjoint_mixin :=
-  isMonad.Build C (M : _ -> _)
-    bindE join_left_unit join_right_unit join_associativity.
-End def.
-Definition build (C D : category)
-           (F : {functor C -> D}) (G : {functor D -> C}) (A : F -| G) :=
-  Monad.Pack (Monad.Class (monad_of_adjoint_mixin A)).
-End _Monad_of_adjoint_functors.
-Notation Monad_of_adjoint_functors := _Monad_of_adjoint_functors.build.
-(* TODO: Can we turn this into a factory? *)
-
-(* Converter from category.monad to hierarchy.monad *)
-Require Import hierarchy.
-
-Module Monad_of_category_monad.
-Section def.
-Variable M : category.Monad.Exports.monad CT.
-
-Definition acto : Type -> Type := M.
-
-Definition actm (A B : Type) (h : A -> B) (x : acto A) : acto B :=
-  (M # [the {hom A -> B} of h]) x.
-
-Lemma actm_id A : actm id = @id (acto A).
-Proof. by rewrite /actm category.functor_id. Qed.
-
-Lemma actm_comp A B C (g : B -> C) (h : A -> B) :
-  actm (g \o h) = actm g \o actm h.
-Proof. by rewrite {1}/actm category.functor_o. Qed.
-
-HB.instance Definition _ := hierarchy.isFunctor.Build acto actm_id actm_comp.
-
-Let F := [the functor of acto].
-
-Lemma actmE (a b : CT) (h : {hom a -> b}) : (F # h)%monae = (M # h)%category.
-Proof. by congr (category.actm M); apply hom_ext. Qed.
-
-Definition ret_ : forall A, idfun A -> F A :=
-  fun A (a : A) => @category.ret _ M A a.
-
-Definition join_ : forall A, [the functor of F \o F] A -> F A :=
-  fun A => @category.join _ M A.
-
-Lemma naturality_ret : hierarchy.naturality _ _ ret_.
-Proof. by move=> ? ? ?; rewrite (category.natural (@category.ret _ M)). Qed.
-
-HB.instance Definition _ := hierarchy.isNatural.Build _ _ ret_ naturality_ret.
 
-Definition ret : (FId ~> F)%monae := [the nattrans _ _ of ret_].
-
-Lemma naturality_join : hierarchy.naturality [the functor of F \o F] F join_.
-Proof.
-move=> a b h; rewrite (_ : h = [the {hom a -> b} of h])//.
-rewrite /join_ actmE (category.natural category.join a).
-congr (_ \o _).
-by rewrite category.FCompE -2!actmE.
-Qed.
-
-HB.instance Definition _ := hierarchy.isNatural.Build _ _ join_ naturality_join.
-
-Definition join := [the nattrans _ _ of join_].
-
-Lemma retE a : ret a = category.ret a. Proof. by []. Qed.
+HB.instance Definition _ := Functor.on M.
+HB.instance Definition monad_of_adjoint_mixin :=
+  Monad_of_ret_join.Build C M join_left_unit join_right_unit join_associativity.
+End mixin.
 
-Lemma joinE a : join a = category.join a. Proof. by []. Qed.
+Section pack.
+Variables (C D : category) (F : {functor C -> D}) (G : {functor D -> C}).
+Variables (A : F -| G).
+Definition pack : monad C := HB.pack_for (monad C) (G \o F) (monad_of_adjoint_mixin A).
+End pack.
+End _Monad_of_adjoint_functors.
+Notation Monad_of_adjoint_functors := _Monad_of_adjoint_functors.pack.
 
-Lemma joinretM : hierarchy.JoinLaws.left_unit ret join.
-Proof.
-by move=> a; apply funext=> x; rewrite joinE retE (category.joinretM a).
-Qed.
+(*
+Require hierarchy.
 
-Lemma joinMret : hierarchy.JoinLaws.right_unit ret join.
-Proof. by move=> a; rewrite joinE retE actmE (@category.joinMret _ M). Qed.
+Module BindLaws2.
+Section misc_laws_on_Type_monad.
+Local Notation CT := (Type : category).
 
-Lemma joinA : hierarchy.JoinLaws.associativity join.
-Proof. by move=> a; rewrite joinE actmE (category.joinA a). Qed.
+Variable M : {functor CT -> CT}.
+Variable bind : forall a b, {hom a -> M b} -> {hom M a -> M b}.
+Local Notation "m >>= f" := (bind f m).
+Variable ret : forall a, {hom a -> M a}.
+Variable add : forall a, M a -> M a -> M a.
+Variable zero : forall a, M a.
+Definition bind_right_distributive  :=
+  forall a b (m : M a) (k1 k2 : a -> M b),
+    m >>= (fun x => add (k1 x) (k2 x)) = add (m >>= k1) (m >>= k2).
+Definition bind_left_distributive :=
+  forall a b (m1 m2 : M a) (k : a -> M b),
+    (add m1 m2) >>= k = add (m1 >>= k) (m2 >>= k).
+Definition right_zero := forall a b (g : M b), g >>= (fun _ => zero a) = zero a.
+Definition left_zero := forall a b g, zero a >>= g = zero b.
+Definition left_id := forall a (m : M a), add (zero a) m = m.
+Definition right_id := forall a (m : M a), add m (zero a) = m.
+
+Fact associative_Type (x y z : CT)
+     (f : {hom x -> M y}) (g : {hom y -> M z}) :
+  (fun w => (f w >>= g)) = (bind g \o f).
+Proof. by []. Qed.
+End misc_laws_on_Type_monad.
+End BindLaws2.
+*)
 
-HB.instance Definition _ := @hierarchy.isMonad_ret_join.Build acto ret join
-  joinretM joinMret joinA.
-End def.
-End Monad_of_category_monad.
-HB.export Monad_of_category_monad.
-(* TODO: Can we turn this into a factory? *)
diff --git a/theories/core/concrete_category.v b/theories/core/concrete_category.v
new file mode 100644
index 00000000..6ee62685
--- /dev/null
+++ b/theories/core/concrete_category.v
@@ -0,0 +1,99 @@
+(* monae: Monadic equational reasoning in Rocq                                *)
+(* Copyright (C) 2025 monae authors, license: LGPL-2.1-or-later               *)
+From HB Require Import structures.
+From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import boolp.
+Require Import preamble category.
+
+(**md**************************************************************************)
+(* # Formalization of basic concrete category theory                          *)
+(*                                                                            *)
+(* This file provides definitions of concrete category and related basic      *)
+(* constructions.                                                             *)
+(*                                                                            *)
+(* ```                                                                        *)
+(*        concrete_category == type of concrete categories; A concrete        *)
+(*                             category C comes with a universe a la Tarski:  *)
+(*                             there is a realizer function el that           *)
+(*                             associates to each object A the type el A      *)
+(*                             of its elements                                *)
+(*                  [fn f]  == function corresponding to the morphism f       *)
+(*            BindLaws_conc == module that define the element-wise monad laws *)
+(*   Monad_of_ret_bind_conc == factory, monad defined by element-wise ret     *)
+(*                             and bind operators                             *)
+(* ```                                                                        *)
+(******************************************************************************)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Local Open Scope category_scope.
+
+HB.mixin Record isConcreteCategory (obj : Type) of @Category obj := {
+  el : obj -> Type ;
+  fn : forall {a b : obj}, {hom a -> b} -> el a -> el b ;
+  fn_inj : forall a b, injective (@fn a b) ;
+  fn_id : forall a : obj , fn (id a) = idfun;
+  fn_comp : forall (a b c : obj) (f : {hom a -> b}) (g : {hom b -> c}),
+      fn (comp f g) = fn g \o fn f ;
+}.
+Arguments isConcreteCategory.phant_Build : clear implicits.
+#[short(type=concrete_category)]
+HB.structure Definition ConcreteCategory := {C of isConcreteCategory C & }.
+Arguments fn [C a b] : rename.
+Arguments fn_id [C] : rename.
+Arguments fn_comp [C] : rename.
+
+Section hom_interface.
+Lemma hom_ext (C : concrete_category) (a b : C) (f g : {hom a -> b}) :
+  f = g <-> fn f =1 fn g.
+Proof. by split; [move-> | by move/funext/fn_inj]. Qed.
+End hom_interface.
+
+Section Type_as_a_concrete_category.
+(* TODO: consider using universe polymorphism *)
+Let UUx := Type@{UU_category}.
+
+HB.instance Definition _ := Category.on UUx.
+HB.instance Definition _ :=
+  isConcreteCategory.Build
+    UUx (fun x => x) (fun _ _ f => f) (fun a b => @inj_id (a -> b))
+    (fun _ => erefl) (fun _ _ _ _ _ => erefl).
+
+End Type_as_a_concrete_category.
+
+Module BindLaws_conc.
+Section conccat.
+Variables (C : concrete_category) (M : C -> C).
+Variable bind : forall a b, {hom a -> M b} -> {hom M a -> M b}.
+Variable ret : forall a, {hom a -> M a}.
+Local Notation "m >>= f" := (fn (bind f) m).
+
+Definition associative :=
+  forall a b c (m : el (M a)) (f : {hom a -> M b}) (g : {hom b -> M c}),
+  (m >>= f) >>= g = m >>= (bind g \c f).
+Definition left_neutral :=
+  forall a b (f : {hom a -> M b}), (bind f \c ret a) = f.
+Definition right_neutral :=
+  forall a (m : el (M a)), m >>= ret a = m.
+End conccat.
+End BindLaws_conc.
+
+HB.factory Record Monad_of_ret_bind_conc (C : concrete_category) (M : C -> C) :=
+{
+  ret : forall a, {hom a -> M a} ;
+  bind : forall (a b : C), {hom a -> M b} -> {hom M a -> M b} ;
+  bindretf : BindLaws_conc.left_neutral bind ret ;
+  bindmret : BindLaws_conc.right_neutral bind ret ;
+  bindA : BindLaws_conc.associative bind ;
+}.
+HB.builders Context C M of Monad_of_ret_bind_conc C M.
+Let bindret : BindLaws.right_neutral bind ret.
+Proof. by move=> a; apply/hom_ext => m; rewrite bindmret fn_id. Qed.
+Let bindA' : BindLaws.associative bind.
+Proof.
+by move=> a b c f g; apply/hom_ext => m; rewrite fn_comp -bindA.
+Qed.
+HB.instance Definition _ :=  Monad_of_ret_bind.Build C M bindretf bindret bindA'.
+HB.end.
diff --git a/theories/core/hierarchy.v b/theories/core/hierarchy.v
index c8cf2a16..cce24f1b 100644
--- a/theories/core/hierarchy.v
+++ b/theories/core/hierarchy.v
@@ -3,12 +3,12 @@
 Ltac typeof X := type of X.
 
 Require Import ssrmatching JMeq Morphisms.
+From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum.
 From mathcomp Require boolp.
 From mathcomp Require Import unstable mathcomp_extra reals.
 From infotheo Require Import realType_ext convex.
 Require Import preamble.
-From HB Require Import structures.
 
 (**md**************************************************************************)
 (* # A formalization of monadic effects over the category Set                 *)
@@ -142,8 +142,7 @@ Notation "f ~~> g" := (forall A, f A -> g A)
 
 Local Open Scope monae_scope.
 
-Notation UU1 := Type.
-Notation UU0 := Type.
+Notation UU0 := Type@{UU_hierarchy}.
 
 (* NB: not putting M in Set -> Set because of expressions like:
   M (A * (size s).-1.-tuple A)%type *)
@@ -311,9 +310,9 @@ Variables (ret : idfun ~~> F) (join : F \o F ~~> F).
 Arguments ret {_}.
 Arguments join {A}.
 
-Definition left_unit := forall A, join \o ret = id :> (F A -> F A).
+Definition left_unit := forall A, join \o ret = idfun :> (F A -> F A).
 
-Definition right_unit := forall A, join \o F # ret = id :> (F A -> F A).
+Definition right_unit := forall A, join \o F # ret = idfun :> (F A -> F A).
 
 Definition associativity := forall A,
   join \o F # join = join \o join :> (F (F (F A)) -> F A).
diff --git a/theories/core/monad_of_category_monad.v b/theories/core/monad_of_category_monad.v
new file mode 100644
index 00000000..c407b34d
--- /dev/null
+++ b/theories/core/monad_of_category_monad.v
@@ -0,0 +1,81 @@
+(* monae: Monadic equational reasoning in Coq                                 *)
+(* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
+From HB Require Import structures.
+From mathcomp Require Import all_ssreflect.
+From mathcomp Require Import boolp.
+Require Import preamble category hierarchy.
+
+(**md**************************************************************************)
+(* # Converter from category.monad to hierarchy.monad                         *)
+(*                                                                            *)
+(* ```                                                                        *)
+(* Monad_of_category_monad == module, interface to isMonad from hierarchy.v   *)
+(* Monad_of_category_monad.m == turns a monad over the Type category into     *)
+(*                        a monad in the sense of isMonad from hierarchy.v    *)
+(* ```                                                                        *)
+(******************************************************************************)
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+Unset Printing Implicit Defensive.
+
+Local Open Scope category_scope.
+
+Local Notation CT := (Type : category).
+
+Module Monad_of_category_monad.
+Section def.
+Variable M : category.Monad.Exports.monad CT.
+
+Definition Fhom (A B : Type) (h : A -> B) (x : M A) : M B :=
+  (M # [the {hom [CT] A -> B} of h]) x.
+
+Lemma Fhom_id A : Fhom (fun x => x) = @id (M A).
+Proof. by rewrite /Fhom category.Fhom_id. Qed.
+
+Lemma Fhom_comp A B C (g : B -> C) (h : A -> B) :
+  Fhom (g \o h) = Fhom g \o Fhom h.
+Proof. by rewrite {1}/Fhom category.Fhom_comp. Qed.
+
+HB.instance Definition _ := @hierarchy.isFunctor.Build _ Fhom Fhom_id Fhom_comp.
+
+Local Notation F := (M : functor).
+
+Definition ret_ : forall A, ((idfun : functor) A : Type) -> F A :=
+  fun A (a : A) => @category.ret _ M A a.
+
+Definition join_ : forall A, (F \o F : functor) A -> F A :=
+  fun A => @category.join _ M A.
+
+Lemma naturality_ret : hierarchy.naturality _ _ ret_.
+Proof. exact: (category.natural (@category.ret _ M)). Qed.
+
+HB.instance Definition _ := hierarchy.isNatural.Build _ _ ret_ naturality_ret.
+
+Definition ret : ((idfun : functor) ~> F)%monae := (ret_ : nattrans _ _).
+
+Lemma naturality_join : hierarchy.naturality (F \o F : functor) F join_.
+Proof. exact: (category.natural (@category.join _ M)). Qed.
+
+HB.instance Definition _ := hierarchy.isNatural.Build _ _ join_ naturality_join.
+
+Definition join := (join_ : nattrans _ _).
+
+Lemma retE a : ret a = category.ret a. Proof. by []. Qed.
+
+Lemma joinE a : join a = category.join a. Proof. by []. Qed.
+
+Lemma joinretM : hierarchy.JoinLaws.left_unit ret join.
+Proof. exact: (@category.joinretM _ M). Qed.
+
+Lemma joinMret : hierarchy.JoinLaws.right_unit ret join.
+Proof. exact: (@category.joinMret _ M). Qed.
+
+Lemma joinA : hierarchy.JoinLaws.associativity join.
+Proof. exact: (@category.joinA _ M). Qed.
+
+HB.instance Definition _ := @hierarchy.isMonad_ret_join.Build M ret join
+  joinretM joinMret joinA.
+End def.
+End Monad_of_category_monad.
+HB.export Monad_of_category_monad.
diff --git a/theories/core/preamble.v b/theories/core/preamble.v
index 910236a1..72efa443 100644
--- a/theories/core/preamble.v
+++ b/theories/core/preamble.v
@@ -5,13 +5,6 @@ From mathcomp Require Import all_ssreflect.
 From mathcomp Require boolp.
 Require ProofIrrelevance.
 
-Definition proof_irr := boolp.Prop_irrelevance.
-
-Definition eq_rect_eq :=
-  @ProofIrrelevance.ProofIrrelevanceTheory.Eq_rect_eq.eq_rect_eq.
-
-Definition funext_dep := boolp.functional_extensionality_dep.
-
 (**md**************************************************************************)
 (* # Shared notations and easy definitions/lemmas of general interest         *)
 (*                                                                            *)
@@ -29,6 +22,25 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Universes UU_hierarchy UU_category.
+Constraint UU_category <= UU_hierarchy.
+
+(* We use a universe-polymorphic version of idfun (in place of ssrfun.idfun)
+   so that we can avoid universe inconsistencies. *)
+Polymorphic Definition idfun (T : Type) (x : T) := x.
+Arguments idfun {T}.
+
+Section shorthands_for_classical_axioms.
+
+Definition proof_irr := boolp.Prop_irrelevance.
+
+Definition eq_rect_eq :=
+  @ProofIrrelevance.ProofIrrelevanceTheory.Eq_rect_eq.eq_rect_eq.
+
+Definition funext_dep := boolp.functional_extensionality_dep.
+
+End shorthands_for_classical_axioms.
+
 (* notations common to hierarchy.v and category.v *)
 
 Reserved Notation "m >>= f" (at level 49).