diff --git a/theories/applications/category_ext.v b/theories/applications/category_ext.v
index 07c4990b..97e6ce9d 100644
--- a/theories/applications/category_ext.v
+++ b/theories/applications/category_ext.v
@@ -41,7 +41,7 @@ Definition slice_category_inhom' (b c : slice) :
 Definition slice_category_inhom := Eval hnf in slice_category_inhom'.
 Local Notation el := slice_category_obj.
 Local Notation inhom := slice_category_inhom.
-Lemma slice_category_id : forall a : slice, inhom (@idfun (el a)).
+Lemma slice_category_id : forall a : slice, inhom (@up_idfun (el a)).
 Proof. by case. Qed.
 Lemma slice_category_comp :
   forall (aa ba ca : slice) (f : el aa -> el ba) (g : el ba -> el ca),
@@ -94,7 +94,7 @@ by case: (cid (Hf2 x)) => y ->.
 Qed.
 Definition inhom (A B : obj) (f : ele A -> ele B) : Prop :=
   exists H : separated f, inhom _ _ (sepfst H) /\ inhom _ _ (sepsnd H).
-Lemma idfun_separated (X : obj) : @separated X X idfun.
+Lemma idfun_separated (X : obj) : @separated X X up_idfun.
 Proof. by split; move=> x; exists x. Qed.
 Lemma comp_separated (X Y Z : obj) (f : ele X -> ele Y) (g : ele Y -> ele Z) :
   separated f -> separated g -> separated (g \o f).
@@ -104,13 +104,13 @@ move: X Y Z => [X1 X2] [Y1 Y2] [Z1 Z2] f g [/= Hf1 Hf2] [/= Hg1 Hg2]; split=> x.
 - by case/cid: (Hf1 x)=> y /= ->; case/cid: (Hg1 y)=> z /= ->; exists z.
 - by case/cid: (Hf2 x)=> y /= ->; case/cid: (Hg2 y)=> z /= ->; exists z.
 Qed.
-Lemma sepfst_idfun X : sepfst (idfun_separated X) = idfun.
+Lemma sepfst_idfun X : sepfst (idfun_separated X) = up_idfun.
 Proof.
 apply funext=> x /=.
 suff: inl (B:=el X.2) (sepfst (idfun_separated X) x) = inl x by move=> [=].
 by rewrite sepfstK.
 Qed.
-Lemma sepsnd_idfun X : sepsnd (idfun_separated X) = idfun.
+Lemma sepsnd_idfun X : sepsnd (idfun_separated X) = up_idfun.
 Proof.
 apply funext=> x /=.
 suff: inr (A:=el X.1) (sepsnd (idfun_separated X) x) = inr x by move=> [=].
@@ -134,7 +134,7 @@ suff: inr (A := el Z.1) (sepsnd (comp_separated Hf Hg) x) =
       inr (sepsnd Hg (sepsnd Hf x)) by case.
 by rewrite 3!sepsndK.
 Qed.
-Lemma idfun_inhom (X : obj) : @inhom X X idfun.
+Lemma idfun_inhom (X : obj) : @inhom X X up_idfun.
 Proof.
 exists (idfun_separated X); rewrite sepfst_idfun sepsnd_idfun;
   split; exact: idfun_inhom.
@@ -170,14 +170,14 @@ exact: Hom.Pack.
 Defined.
 Definition homsnd := Eval hnf in _homsnd.
 End homfstsnd.
-Lemma homfst_idfun x : homfst (x:=x) [hom idfun] = [hom idfun].
+Lemma homfst_idfun x : homfst (x:=x) [hom up_idfun] = [hom up_idfun].
 Proof.
 apply/hom_ext; rewrite boolp.funeqE => x1 /=.
 case: cid => i [i1 i2] /=.
 rewrite (_ : i = ProductCategory.idfun_separated _)//.
 by rewrite ProductCategory.sepfst_idfun.
 Qed.
-Lemma homsnd_idfun x : homsnd (x:=x) [hom idfun] = [hom idfun].
+Lemma homsnd_idfun x : homsnd (x:=x) [hom up_idfun] = [hom up_idfun].
 Proof.
 apply/hom_ext; rewrite boolp.funeqE => x1 /=.
 case: cid => i [i1 i2] /=.
@@ -259,7 +259,7 @@ End prodCat_pairhom.
 
 Section pairhom_idfun.
 Variables (A B : category) (a : A) (b : B).
-Lemma pairhom_idfun : pairhom (a1:=a) (b1:=b) [hom idfun] [hom idfun] = [hom idfun].
+Lemma pairhom_idfun : pairhom (a1:=a) (b1:=b) [hom up_idfun] [hom up_idfun] = [hom up_idfun].
 Proof. by apply/hom_ext/funext=> -[] x /=. Qed.
 End pairhom_idfun.
 
@@ -311,18 +311,18 @@ Section def.
 Variables (A B C : category) (F : {functor A * B -> C}) (a : A).
 Definition acto : B -> C := fun b => F (a, b).
 Definition actm (b1 b2 : B) (f : {hom b1 -> b2}) : {hom acto b1 -> acto b2} :=
-  F # pairhom [hom idfun] f.
+  F # pairhom [hom up_idfun] f.
 Let actm_id : FunctorLaws.id actm.
 Proof.
 move=> D; rewrite /actm; set h := pairhom _ _.
-rewrite (_ : h = [hom idfun]) ?functor_id_hom //.
+rewrite (_ : h = [hom up_idfun]) ?functor_id_hom //.
 by apply/hom_ext => /=; rewrite boolp.funeqE; case.
 Qed.
 Let actm_comp : FunctorLaws.comp actm.
 Proof.
 move=> b b0 b1 g h; rewrite /actm; set i := pairhom _ _.
-rewrite (_ : i = [hom (pairhom [hom idfun] g) \o
-                      (pairhom [hom idfun] h)]) ?functor_o_hom //.
+rewrite (_ : i = [hom (pairhom [hom up_idfun] g) \o
+                      (pairhom [hom up_idfun] h)]) ?functor_o_hom //.
 by apply/hom_ext => /=; rewrite boolp.funeqE; case.
 Qed.
 HB.instance Definition _ := isFunctor.Build _ _ _ actm_id actm_comp.
@@ -334,18 +334,18 @@ Section def.
 Variables (A B C : category) (F : {functor A * B -> C}) (b : B).
 Definition acto : A -> C := fun a => F (a, b).
 Definition actm (a1 a2 : A) (f : {hom a1 -> a2}) : {hom acto a1 -> acto a2} :=
-  F # pairhom f [hom idfun].
+  F # pairhom f [hom up_idfun].
 Let actm_id : FunctorLaws.id actm.
 Proof.
 move=> D; rewrite /actm; set h := pairhom _ _.
-rewrite (_ : h = [hom idfun]) ?functor_id_hom //.
+rewrite (_ : h = [hom up_idfun]) ?functor_id_hom //.
 by apply/hom_ext => /=; rewrite boolp.funeqE; case.
 Qed.
 Let actm_comp : FunctorLaws.comp actm.
 Proof.
 move=> a a0 a1 g h; rewrite /actm; set i := pairhom _ _.
-rewrite (_ : i = [hom (pairhom g [hom idfun]) \o
-                      (pairhom h [hom idfun])]) ?functor_o_hom //.
+rewrite (_ : i = [hom (pairhom g [hom up_idfun]) \o
+                      (pairhom h [hom up_idfun])]) ?functor_o_hom //.
 by apply/hom_ext => /=; rewrite boolp.funeqE; case.
 Qed.
 HB.instance Definition _ := isFunctor.Build _ _ _ actm_id actm_comp.
@@ -387,18 +387,18 @@ Variable F : {functor [the category of ((A * B) * C)%type] -> D}.
 Variables (a : A) (b : B).
 Definition acto : C -> D := papply_left.acto F (a, b).
 Definition actm (c1 c2 : C) (f : {hom c1 -> c2}) : {hom acto c1 -> acto c2} :=
-  F # pairhom [hom idfun] f.
+  F # pairhom [hom up_idfun] f.
 Let actm_id : FunctorLaws.id actm.
 Proof.
 move=> c0; rewrite /actm; set h := pairhom _ _.
-rewrite (_ : h = [hom idfun]) ?functor_id_hom //.
+rewrite (_ : h = [hom up_idfun]) ?functor_id_hom //.
 by apply/hom_ext => /=; rewrite boolp.funeqE; case.
 Qed.
 Let actm_comp : FunctorLaws.comp actm.
 Proof.
 move=> c c0 c1 g h; rewrite /actm; set i := pairhom _ _.
-rewrite (_ : i = [hom (pairhom [hom idfun] g) \o
-                      (pairhom [hom idfun] h)]) ?functor_o_hom //.
+rewrite (_ : i = [hom (pairhom [hom up_idfun] g) \o
+                      (pairhom [hom up_idfun] h)]) ?functor_o_hom //.
 by apply/hom_ext => /=; rewrite boolp.funeqE; case.
 Qed.
 HB.instance Definition _ := isFunctor.Build _ _ _ actm_id actm_comp.
diff --git a/theories/applications/example_relabeling.v b/theories/applications/example_relabeling.v
index 21e25467..0dc4dc3c 100644
--- a/theories/applications/example_relabeling.v
+++ b/theories/applications/example_relabeling.v
@@ -122,9 +122,7 @@ Proof.
 rewrite boolp.funeqE => -[x1 x2].
 rewrite 3!compE.
 rewrite joinE.
-rewrite fmapE.
-rewrite 2![in RHS]compE.
-rewrite [in RHS]/mpair.
+rewrite fmapE/=.
 rewrite [in LHS]/mpair.
 move H : (fmap dlabels) => h.
 rewrite /=.
diff --git a/theories/applications/example_typed_store.v b/theories/applications/example_typed_store.v
index 9ba0a8b3..3345044f 100644
--- a/theories/applications/example_typed_store.v
+++ b/theories/applications/example_typed_store.v
@@ -334,9 +334,9 @@ Section eval.
 Require Import typed_store_transformer.
 Import ModelTypedStoreRun.
 
-Definition M := acto ml_type idfun.
+Definition M := acto ml_type up_idfun.
 
-Definition Env := Env ml_type idfun.
+Definition Env := Env ml_type up_idfun.
 
 Definition empty_env : Env := [::].
 
@@ -367,9 +367,9 @@ Eval vm_compute in it1.
 Definition it2 := Restart it1 (do l <- FromW l; incr l).
 Eval vm_compute in it2.
 
-Local Notation cycle := (cycle idfun M).
-Local Notation rhd := (rhd idfun M).
-Local Notation rtl := (rtl idfun M).
+Local Notation cycle := (cycle up_idfun M).
+Local Notation rhd := (rhd up_idfun M).
+Local Notation rtl := (rtl up_idfun M).
 
 Definition it3 := Restart it2 (cycle ml_bool true false).
 Eval vm_compute in crun (FromW it3).
diff --git a/theories/applications/monad_composition.v b/theories/applications/monad_composition.v
index aae9c0c5..2a5c0333 100644
--- a/theories/applications/monad_composition.v
+++ b/theories/applications/monad_composition.v
@@ -20,13 +20,13 @@ Local Open Scope monae_scope.
 
 Section comp.
 Variables (M N : monad).
-Definition ret_comp : idfun ~~> M \o N := (@ret M) \h (@ret N).
-Lemma naturality_ret : naturality idfun [the functor of M \o N] ret_comp.
+Definition ret_comp : up_idfun ~~> M \o N := (@ret M) \h (@ret N).
+Lemma naturality_ret : naturality up_idfun [the functor of M \o N] ret_comp.
 Proof. by move=> A B h; rewrite -(natural ((@ret M) \h (@ret N))). Qed.
 HB.instance Definition _ := isNatural.Build
-  idfun [the functor of (M \o N)] ret_comp naturality_ret.
+  up_idfun [the functor of (M \o N)] ret_comp naturality_ret.
 End comp.
-Definition CRet (M N : monad) := [the idfun ~> [the functor of M \o N] of ret_comp M N].
+Definition CRet (M N : monad) := [the up_idfun ~> [the functor of M \o N] of ret_comp M N].
 
 Module Prod.
 Section prod.
@@ -127,7 +127,7 @@ move=> A B g; apply/esym; rewrite {1}/JOIN -compA Hdorp1.
 rewrite [LHS]compA.
 rewrite (FCompE M N (N # g)).
 rewrite -(@functor_o M).
-rewrite -natural.
+rewrite -(natural join).
 by rewrite functor_o.
 Qed.
 
@@ -218,7 +218,7 @@ Lemma prod1 : Prod.prod1 (@prod).
 Proof.
 move=> A B f; rewrite {1}/prod.
 rewrite -[LHS]compA Hswap1 (compA (M # Join)) -functor_o.
-by rewrite -natural functor_o -compA.
+by rewrite -(natural join)/= functor_o -compA.
 Qed.
 
 Lemma prod2 : Prod.prod2 (@prod).
@@ -312,13 +312,13 @@ End Swap.
 
 Section nattrans_cast_lemmas.
 Variables (F G : functor).
-Lemma IV : [the functor of idfun \o G] ~> F -> G ~> F.
+Lemma IV : [the functor of up_idfun \o G] ~> F -> G ~> F.
 Proof.
 move=> [s [] [GFs]].
 apply: (@Nattrans.Pack [the functor of G] F _ (Nattrans.Class (isNatural.Axioms_ _ _ _))).
 exact: GFs.
 Qed.
-Lemma VI : [the functor of G \o idfun] ~> F -> G ~> F.
+Lemma VI : [the functor of G \o up_idfun] ~> F -> G ~> F.
 Proof.
 move=> [s [] [GFs]].
 apply: (@Nattrans.Pack [the functor of G] F _ (Nattrans.Class (isNatural.Axioms_ _ _ _))).
diff --git a/theories/core/category.v b/theories/core/category.v
index 140db9a7..70c9aada 100644
--- a/theories/core/category.v
+++ b/theories/core/category.v
@@ -79,7 +79,7 @@ Hint Resolve frefl_transparent : core.
 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 ;
+  idfun_inhom : forall a, @inhom a a up_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)
 }.
@@ -118,7 +118,7 @@ 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 _ c := isHom.Build _ _ _ (@up_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)).
@@ -190,7 +190,7 @@ 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].
+  transport_codom p [hom up_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].
@@ -227,7 +227,7 @@ 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 [hom up_idfun] = [hom up_idfun] :> {hom F a -> 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].
 End def.
@@ -250,7 +250,7 @@ Notation "{ 'functor' fCD }" := (functor_phant (Phant fCD))
 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)).
+Lemma functor_id a : F # [hom up_idfun] = up_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}) :
@@ -297,8 +297,8 @@ 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].
+HB.instance Definition _ := isFunctor.Build _ _ up_idfun id_id id_comp.
+Definition FId : {functor C -> C} := [the {functor _ -> _} of up_idfun].
 Lemma FIdf (A B : C) (f : {hom A -> B}) : FId # f = f.
 Proof. by []. Qed.
 End functorid.
@@ -368,20 +368,20 @@ 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''.
 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].
 
 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) => [hom (@up_idfun (el (F a)))].
 Definition natural_id : naturality _ _ unnattrans_id.
 Proof. by []. 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]) :> (_ ~~> _).
+Lemma NIdE : NId  = (fun a => [hom up_idfun]) :> (_ ~~> _).
 Proof. by []. Qed.
 End id_natural_transformation.
 
@@ -393,7 +393,7 @@ 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 [hom up_idfun].
 Lemma natural : naturality F G f.
 Proof.
 move=> a b h.
@@ -410,7 +410,7 @@ Module Exports.
 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]) :> (_ ~~> _).
+  (fun a => transport_codom (Iobj _) [hom up_idfun]) :> (_ ~~> _).
 Proof. by []. Qed.
 End Exports.
 End NEq.
@@ -520,7 +520,7 @@ Proof.
 by apply nattrans_ext=> a; rewrite VCompE HCompE HIdComp HCompId -natural.
 Qed.
 
-Lemma NIdFId c : NId (@FId C) c = [hom idfun].
+Lemma NIdFId c : NId (@FId C) c = [hom up_idfun].
 Proof. by []. Qed.
 
 Lemma NIdFComp : NId (F' \O F) = NId F' \h NId F.
@@ -544,8 +544,8 @@ 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.
+Definition left := forall c, eps (F c) \o F # (eta c) = up_idfun.
+Definition right := forall d, G # (eps d) \o eta (G d) = up_idfun.
 End triangularlaws.
 End TriangularLaws.
 
@@ -588,9 +588,9 @@ 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].
+Lemma eta_hom_iso (c : C) : eta A c = hom_iso [hom up_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].
+Lemma eps_hom_inv (d : D) : eps A d = hom_inv [hom up_idfun].
 Proof. by apply hom_ext; rewrite /hom_inv /= functor_id compfid. Qed.
 
 Lemma ext (B : F -| G) : eta A = eta B -> eps A = eps B -> A = B.
@@ -700,9 +700,9 @@ Section join_laws.
 Variables (C : category) (M : {functor C -> C}) .
 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 \o ret (M a) = up_idfun :> (el (M a) -> el (M a)).
 Definition right_unit :=
-  forall a, join a \o M # ret a = idfun :> (el (M a) -> el (M a)).
+  forall a, join a \o M # ret a = up_idfun :> (el (M a) -> el (M a)).
 Definition associativity :=
   forall a, join a \o M # join a = join a \o join (M a) :> (el (M (M (M a))) -> el (M a)).
 End join_laws.
@@ -843,7 +843,7 @@ Proof. by apply/bind_left_neutral_hom_fun/bindretf. Qed.
 Let fmap_id : FunctorLaws.id fmap.
 Proof.
 move=> A; apply/hom_ext/funext=>m. rewrite /fmap.
-rewrite/idfun/=.
+rewrite/up_idfun/=.
 rewrite -[in RHS](bindmret m).
 congr (fun f => bind f m).
 by rewrite hom_ext.
@@ -862,7 +862,7 @@ 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 join' : F \O F ~~> F := fun _ => bind [hom up_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.
@@ -889,7 +889,7 @@ 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).
 Proof.
 rewrite /join /=.
-rewrite /=bind_fmap/idfun/=.
+rewrite /=bind_fmap/up_idfun/=.
 congr (fun f => bind f m).
 by rewrite hom_ext.
 Qed.
@@ -1002,7 +1002,7 @@ 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 :=
+Definition ret_ : forall A, up_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 :=
diff --git a/theories/core/hierarchy.v b/theories/core/hierarchy.v
index 55001325..63fdd4d9 100644
--- a/theories/core/hierarchy.v
+++ b/theories/core/hierarchy.v
@@ -168,13 +168,13 @@ Notation "F # g" := (@actm F _ _ g) : monae_scope.
 Notation "'fmap' f" := (_ # f) : mprog.
 
 Section functorid.
-Let id_actm (A B : UU0) (f : A -> B) : idfun A -> idfun B := f.
+Let id_actm (A B : UU0) (f : A -> B) : up_idfun A -> up_idfun B := f.
 Let id_id : FunctorLaws.id id_actm. Proof. by []. Qed.
 Let id_comp : FunctorLaws.comp id_actm. Proof. by []. Qed.
-HB.instance Definition _ := isFunctor.Build idfun id_id id_comp.
+HB.instance Definition _ := isFunctor.Build up_idfun id_id id_comp.
 End functorid.
 
-Lemma FIdE (A B : UU0) (f : A -> B) : idfun # f = f. Proof. by []. Qed.
+Lemma FIdE (A B : UU0) (f : A -> B) : up_idfun # f = f. Proof. by []. Qed.
 
 Section functor_composition.
 Variables F G : functor.
@@ -307,7 +307,7 @@ Qed.*)
 Module JoinLaws.
 Section join_laws.
 Context {F : functor}.
-Variables (ret : idfun ~~> F) (join : F \o F ~~> F).
+Variables (ret : up_idfun ~~> F) (join : F \o F ~~> F).
 Arguments ret {_}.
 Arguments join {A}.
 
@@ -322,7 +322,7 @@ End join_laws.
 End JoinLaws.
 
 HB.mixin Record isMonad (F : UU0 -> UU0) of Functor F := {
-  ret : idfun ~> F ;
+  ret : up_idfun ~> F ;
   join : F \o F ~> F ;
   bind : forall (A B : UU0), F A -> (A -> F B) -> F B ;
   bindE : forall (A B : UU0) (f : A -> F B) (m : F A),
@@ -403,7 +403,7 @@ Definition bind_of_join (F : functor) (j : F \o F ~~> F)
   j B ((F # f) m).
 
 Section from_join_laws_to_bind_laws.
-Variable (F : functor) (ret : idfun ~> F) (join : F \o F ~> F).
+Variable (F : functor) (ret : up_idfun ~> F) (join : F \o F ~> F).
 
 Hypothesis joinretM : JoinLaws.left_unit ret join.
 Hypothesis joinMret : JoinLaws.right_unit ret join.
@@ -430,7 +430,7 @@ Qed.
 End from_join_laws_to_bind_laws.
 
 HB.factory Record isMonad_ret_join (F : UU0 -> UU0) of isFunctor F := {
-  ret : idfun ~> F ;
+  ret : up_idfun ~> F ;
   join : F \o F ~> F ;
   joinretM : JoinLaws.left_unit ret join ;
   joinMret : JoinLaws.right_unit ret join ;
@@ -482,7 +482,7 @@ HB.instance Definition _ := isFunctor.Build M actm_id actm_comp.
 Let F := [the functor of M].
 Local Notation FF := [the functor of F \o F].
 
-Let ret_naturality : naturality idfun F ret.
+Let ret_naturality : naturality up_idfun F ret.
 Proof.
 move=> a b h.
 rewrite FIdE /hierarchy.actm /= /actm; apply: boolp.funext => m /=.
@@ -490,9 +490,9 @@ by rewrite bindretf.
 Qed.
 
 HB.instance Definition _ :=
-  isNatural.Build idfun F (ret : idfun ~~> F) ret_naturality.
+  isNatural.Build up_idfun F (ret : up_idfun ~~> F) ret_naturality.
 
-Let join' : FF ~~> F := fun _ m => bind m idfun.
+Let join' : FF ~~> F := fun _ m => bind m up_idfun.
 
 Let actm_bind (a b c : UU0) (f : a -> b) m (g : c -> F a) :
   (actm f) (bind m g) = bind m (actm f \o g).
@@ -703,7 +703,8 @@ Local Open Scope mprog.
 Lemma fcomp_kleisli A B C D (f : A -> B) (g : C -> M A) (h : D -> M C) :
   f (o) (g <=< h) = (f (o) g) <=< h.
 Proof.
-rewrite /kleisli 2!fcomp_def 2!(compA (fmap f)) natural [in RHS]functor_o.
+rewrite /kleisli 2!fcomp_def 2!(compA (fmap f)).
+rewrite (natural join) [in RHS]functor_o.
 by rewrite -compA.
 Qed.
 
@@ -778,7 +779,8 @@ Definition bassert {A : UU0} (p : pred A) (m : M A) : M A := m >>= assert p.
 Lemma commutativity_of_assertions A q :
   Join \o (M # (bassert q)) = bassert q \o Join :> (_ -> M A).
 Proof.
-by apply boolp.funext => x; rewrite !compE join_fmap /bassert joinE bindA.
+apply boolp.funext => x; rewrite !compE join_fmap /bassert joinE.
+by rewrite -/(_ >>= _) bindA.
 Qed.
 
 (* guards commute with anything *)
@@ -918,7 +920,7 @@ HB.mixin Record isMonadElgot (M : UU0 -> UU0) of WBisim M := {
                                           (M # inl \o g)
                                           (M # inr \o Ret)) a);
   codiagonalwB : forall (A B : UU0) (f : A -> M ((B + A) + A)%type) (a : A),
-    while ((M # (sum_rect (fun=> (B + A)%type) idfun inr)) \o f) a
+    while ((M # (sum_rect (fun=> (B + A)%type) up_idfun inr)) \o f) a
     ≈ while (while f) a ;
   uniformwB : forall (A B C : UU0) (f : A -> M (B + A)%type)
       (g : C -> M (B + C)%type) (h : C -> A),
diff --git a/theories/core/monad_transformer.v b/theories/core/monad_transformer.v
index 56723ae7..62450f9c 100644
--- a/theories/core/monad_transformer.v
+++ b/theories/core/monad_transformer.v
@@ -96,7 +96,7 @@ Variables (S : UU0) (M : monad).
 
 Definition MS := fun A : UU0 => S -> M (A * S)%type.
 
-Definition retS : idfun ~~> MS := fun A : UU0 => curry Ret.
+Definition retS : up_idfun ~~> MS := fun A : UU0 => curry Ret.
 
 Definition bindS (A B : UU0) (m : MS A) f : MS B := fun s => m s >>= uncurry f.
 
@@ -216,7 +216,7 @@ Variables (Z : UU0) (* the type of exceptions *) (M : monad).
 Definition MX := fun X : UU0 => M (Z + X)%type.
 
 (* unit and bind operator of the transformed monad *)
-Definition retX : idfun ~~> MX := fun X x => Ret (inr x).
+Definition retX : up_idfun ~~> MX := fun X x => Ret (inr x).
 
 Definition bindX X Y (t : MX X) (f : X -> MX Y) : MX Y :=
   t >>= fun c => match c with inl z => Ret (inl z) | inr x => f x end.
@@ -336,7 +336,7 @@ Variables (R : UU0) (M : monad).
 
 Definition MEnv := fun A : UU0 => R -> M A.
 
-Definition retEnv : idfun ~~> MEnv := fun (A : UU0) a r => Ret a.
+Definition retEnv : up_idfun ~~> MEnv := fun (A : UU0) a r => Ret a.
 
 Definition bindEnv A B (m : MEnv A) f : MEnv B :=
   fun r => m r >>= (fun a => f a r).
@@ -388,7 +388,7 @@ Variables (R : UU0) (M : monad).
 
 Definition MO (X : UU0) := M (X * seq R)%type.
 
-Definition retO : idfun ~~> MO := fun (A : UU0) a => Ret (a, [::]).
+Definition retO : up_idfun ~~> MO := fun (A : UU0) a => Ret (a, [::]).
 
 Definition bindO A B (m : MO A) (f : A -> MO B) : MO B :=
   m >>= (fun o => let: (x, w) := o in f x >>=
@@ -462,7 +462,7 @@ Variables (r : UU0) (M : monad).
 
 Definition MC : UU0 -> UU0 := fun A => (A -> M r) -> M r %type.
 
-Definition retC : idfun ~~> MC := fun (A : UU0) (a : A) k => k a.
+Definition retC : up_idfun ~~> MC := fun (A : UU0) (a : A) k => k a.
 
 Definition bindC A B (m : MC A) f : MC B := fun k => m (f^~ k).
 
@@ -647,8 +647,8 @@ Definition psi' (n : E ~~> M) : E \o M ~~> M := fun X => Join \o n (M X).
 Lemma natural_psi' (n : E ~> M) : naturality [the functor of E \o M] M (psi' n).
 Proof.
 move=> A B h; rewrite /psi'.
-rewrite -/(Join \o n (M A)) [LHS]compA natural.
-by rewrite -compA (natural n).
+rewrite -/(Join \o n (M A)) [LHS]compA (natural join).
+by rewrite /= -compA (natural n).
 Qed.
 
 HB.instance Definition _ (n : E ~> M) := isNatural.Build
diff --git a/theories/core/preamble.v b/theories/core/preamble.v
index 910236a1..6696251a 100644
--- a/theories/core/preamble.v
+++ b/theories/core/preamble.v
@@ -5,19 +5,14 @@ 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         *)
 (*                                                                            *)
 (* ```                                                                        *)
-(*                foldr1                                                      *)
-(*         curry/uncurry == currying for pairs                                *)
+(*     up_idfun, up_comp == universe-polymorphic equivalents of               *)
+(*                          ssrfun.idfun and ssrfun.comp                      *)
+(*                foldr1 == right-recursive application of a binary operation *)
+(*                          on a list                                         *)
 (*       curry3/uncurry3 == currying for triples                              *)
 (*        comparePc/eqPc == computable version of equality axioms             *)
 (*  coerce T1 (v : f T1) == some (f T2) if T1 = T2 and None o.w.              *)
@@ -29,6 +24,46 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+(* We use a universe-polymorphic version of idfun and comp
+   (in place of ssrfun.idfun and ssrfun.comp)
+   so that we can avoid universe inconsistencies. *)
+Polymorphic Definition up_idfun (T : Type) (x : T) := x.
+Arguments up_idfun {T} x /.
+
+Polymorphic Definition up_comp (A B C : Type) (f : B -> A) (g : C -> B) :=
+  fun x => f (g x).
+Arguments up_comp {A B C} f g x /.
+Notation "f1 \o f2" := (up_comp f1 f2) : function_scope.
+
+Section comp_lemmas.
+
+(* This compA is equivalent of ssrfun.compA for up_comp.
+   There are more lemmas for ssrfun.comp, such as
+   bij_comp, inj_comp, etc.  They should be added once in need *)
+Lemma compA {A B C D} (f : C -> D) (g : B -> C) (h : A -> B) :
+  f \o (g \o h) = (f \o g) \o h.
+Proof. by []. Qed.
+
+Lemma compfid A B (f : A -> B) : f \o id = f. Proof. by []. Qed.
+
+Lemma compidf A B (f : A -> B) : id \o f = f. Proof. by []. Qed.
+
+Lemma compE A B C (g : B -> C) (f : A -> B) a : (g \o f) a = g (f a).
+Proof. by []. Qed.
+
+End comp_lemmas.
+
+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).
@@ -143,17 +178,6 @@ Definition const A B (b : B) := fun _ : A => b.
 
 Definition wrap {A} (a : A) := [:: a].
 
-Lemma compA {A B C D} (f : C -> D) (g : B -> C) (h : A -> B) :
-  f \o (g \o h) = (f \o g) \o h.
-Proof. by []. Qed.
-
-Lemma compfid A B (f : A -> B) : f \o id = f. Proof. by []. Qed.
-
-Lemma compidf A B (f : A -> B) : id \o f = f. Proof. by []. Qed.
-
-Lemma compE A B C (g : B -> C) (f : A -> B) a : (g \o f) a = g (f a).
-Proof. by []. Qed.
-
 Lemma if_pair A B b (x : A) y (u : A) (v : B) :
   (if b then (x, y) else (u, v)) = (if b then x else u, if b then y else v).
 Proof. by case: ifPn. Qed.
diff --git a/theories/lib/alt_lib.v b/theories/lib/alt_lib.v
index c5bcea8e..b3973246 100644
--- a/theories/lib/alt_lib.v
+++ b/theories/lib/alt_lib.v
@@ -126,9 +126,9 @@ Lemma arbitrary_naturality (T U : UU0) (a : T) (b : U) (f : T -> U) :
   forall x, 0 < size x -> (M # f \o arbitrary a) x = (arbitrary b \o map f) x.
 Proof.
 elim=> // x [_ _ | x' xs /(_ isT)].
-  by rewrite [in LHS]compE fmapE bindretf.
+  by rewrite /= fmapE bindretf.
 rewrite [in X in X -> _]/= fmapE => ih _.
-rewrite [in RHS]compE [in RHS]/= [in RHS](arbitrary_cons b) // [in LHS]compE.
+rewrite [in RHS]/= [in RHS](arbitrary_cons b) //=.
 by rewrite [in LHS]arbitrary_cons // fmapE /= alt_bindDl bindretf /= ih.
 Qed.
 
@@ -138,7 +138,7 @@ Lemma mpair_arbitrary_base_case (T : UU0) a x (y : seq T) :
 Proof.
 move=> y0; rewrite cp1.
 transitivity (arbitrary a y >>= (fun y' => Ret (x, y')) : M _).
-  by rewrite -(compE (arbitrary _)) -(arbitrary_naturality a) // compE fmapE.
+  by rewrite -(compE (arbitrary _)) -(arbitrary_naturality a) //= fmapE.
 transitivity (do z <- Ret x; do y' <- arbitrary a y; Ret (z, y') : M _)%Do.
   by rewrite bindretf.
 by [].
@@ -311,7 +311,7 @@ Lemma insert_map (A B : UU0) (f : A -> B) (a : A) :
   insert (f a) \o map f = map f (o) insert a :> (_ -> M _).
 Proof.
 apply boolp.funext; elim => [|y xs IH].
-  by rewrite fcompE insertE -(compE (fmap (map f))) (natural ret) compE insertE.
+  by rewrite fcompE insertE -(compE (fmap (map f))) (natural ret) /= insertE.
 apply/esym.
 rewrite fcompE insertE alt_fmapDr.
 (* first branch *)
diff --git a/theories/lib/fail_lib.v b/theories/lib/fail_lib.v
index 58adc208..480a7682 100644
--- a/theories/lib/fail_lib.v
+++ b/theories/lib/fail_lib.v
@@ -181,11 +181,11 @@ rewrite 2![in RHS]insertE.
 rewrite [in LHS]alt_fmapDr ![in LHS]altA [in LHS](altC (Ret [:: a, b, h & t])).
 rewrite -!altA; congr (_ [~] _); first by rewrite fmapE bindretf.
 rewrite alt_fmapDr -!altA; congr (_ [~] _); first by rewrite fmapE bindretf.
-rewrite [in LHS]altC bind_fmap /= [in LHS]/comp /=.
+rewrite [in LHS]altC bind_fmap /= [in LHS]/(_ \o _) /=.
 under eq_bind do rewrite insertE.
 rewrite alt_bindDr.
 under [in X in (_ [~] X) [~] _]eq_bind do rewrite fmapE.
-rewrite -bindA [in LHS]ih // [in RHS]altC bind_fmap /= [in RHS]/comp /=.
+rewrite -bindA [in LHS]ih // [in RHS]altC bind_fmap /= [in RHS]/(_ \o _) /=.
 under [in RHS]eq_bind do rewrite insertE.
 rewrite alt_bindDr [in RHS]altC -!altA; congr (_ [~] _).
   rewrite !fmapE !bindA.
@@ -287,7 +287,7 @@ move=> [/= _ x y|h t].
   by rewrite !bindA !bindretf /= bindA bindretf [in RHS]insertE bindretf.
 rewrite ltnS /= => tn x y.
 rewrite bindA iperm_rcons /= !bindA [in RHS]insertE alt_bindDl bindretf /=.
-rewrite bindA iperm_rcons /= bindA bind_fmap /comp /= -[in X in _ [~]X]bindA.
+rewrite bindA iperm_rcons /= bindA bind_fmap /(_ \o _) /= -[in X in _ [~]X]bindA.
 rewrite -ih// bindA iperm_rcons /= !bindA -alt_bindDr; bind_ext => s'.
 rewrite -alt_bindDr; bind_ext => t'.
 by rewrite insertC altmm.
@@ -309,7 +309,7 @@ elim: s => [|h t ih]; first by rewrite /= bindretf.
 rewrite /= -[in RHS]ih !bindA; bind_ext.
 elim/last_ind => [|s x _].
   by rewrite insertE /= !bindretf insertE /= bindretf insertE.
-rewrite iperm_insertC insert_rcons alt_bindDl bind_fmap /= /comp /=.
+rewrite iperm_insertC insert_rcons alt_bindDl bind_fmap /= /(_ \o _) /=.
 under [in RHS]eq_bind do rewrite iperm_rcons_bind.
 rewrite bindretf (@perm_eq_iperm _ _ (h :: rcons s x)); last first.
   by rewrite -cats1 -cat1s catA perm_catC.
@@ -704,7 +704,7 @@ Lemma liftM2_isNondet A B C (f : A -> B -> C) (ma : M A) (mb : M B) :
 Proof.
 move=> [s1 s1_ma] [s2 s2_mb].
 exists (ndBind s1 (fun a => ndBind s2 (fun b => ndRet (f a b)))).
-by rewrite /= s1_ma /comp /= s2_mb.
+by rewrite /= s1_ma /(_ \o _) /= s2_mb.
 Qed.
 
 Lemma guard_isNondet (b : bool) : plus_isNondet (guard b : M _).
diff --git a/theories/lib/monad_lib.v b/theories/lib/monad_lib.v
index 1da08eb7..f4b9fa2c 100644
--- a/theories/lib/monad_lib.v
+++ b/theories/lib/monad_lib.v
@@ -301,7 +301,7 @@ Lemma fmap_oE (M : functor) (A B C : UU0) (f : A -> B) (g : C -> A) (m : M C) :
   (M # (f \o g)) m = (M # f) ((M # g) m).
 Proof. by rewrite functor_o. Qed.
 
-Definition NId (C : functor) := fun A => @idfun (C A).
+Definition NId (C : functor) := fun A => @up_idfun (C A).
 
 Section id_natural_transformation.
 Variables C : functor.
@@ -393,18 +393,18 @@ Lemma functor_app_natural_hcomp (S F G : functor) (nt : F ~> G) :
   S ## nt = [the _ ~> _ of NId S] \h nt.
 Proof. by apply nattrans_ext => a; rewrite functor_app_naturalE. Qed.
 
-Definition fork : idfun ~~> squaring := fun (A : UU0) (a : A) => (a, a).
+Definition fork : up_idfun ~~> squaring := fun (A : UU0) (a : A) => (a, a).
 
 Section natural_transformation_example.
 
 Let fork_natural : naturality _ _ fork. Proof. by []. Qed.
 
-HB.instance Definition _ := isNatural.Build idfun squaring fork fork_natural.
+HB.instance Definition _ := isNatural.Build up_idfun squaring fork fork_natural.
 
 End natural_transformation_example.
 
-Definition eta_type (f g : functor) := idfun ~> g \o f.
-Definition eps_type (f g : functor) := f \o g ~> idfun.
+Definition eta_type (f g : functor) := up_idfun ~> g \o f.
+Definition eps_type (f g : functor) := f \o g ~> up_idfun.
 
 Module TriangularLaws.
 Section triangularlaws.
@@ -436,16 +436,16 @@ Notation "F -| G" := (AdjointFunctor.t F G).
 Section adjoint_example.
 Variable (X : UU0).
 
-Definition curry_eps : curryF X \o uncurryF X ~~> idfun :=
+Definition curry_eps : curryF X \o uncurryF X ~~> up_idfun :=
   fun (A : UU0) (af : X * (X -> A)) => af.2 af.1.
 
-Let curry_eps_naturality : naturality (curryF X \o uncurryF X) idfun curry_eps.
+Let curry_eps_naturality : naturality (curryF X \o uncurryF X) up_idfun curry_eps.
 Proof. by []. Qed.
 
 HB.instance Definition _ := isNatural.Build
-  (curryF X \o uncurryF X) idfun curry_eps curry_eps_naturality.
+  (curryF X \o uncurryF X) up_idfun curry_eps curry_eps_naturality.
 
-Definition curry_eta : idfun ~~> uncurryF X \o curryF X :=
+Definition curry_eta : up_idfun ~~> uncurryF X \o curryF X :=
   fun (A : UU0) (a : A) => pair^~ a.
 
 Let curry_eta_naturality : naturality _ (uncurryF X \o curryF X) curry_eta.
@@ -459,7 +459,7 @@ Proof.
 apply: (@AdjointFunctor.mk _ _ curry_eta curry_eps).
 by move=> A; rewrite /TriangularLaws.left; apply boolp.funext => -[].
 move=> A; rewrite /TriangularLaws.right /uncurryF /curry_eps /curry_eta /uncurryF.
-by rewrite /= /uncurry_actm /= /comp /=; apply boolp.funext => f; apply boolp.funext.
+by rewrite /= /uncurry_actm /= ; apply boolp.funext => f; apply boolp.funext.
 Qed.
 
 End adjoint_example.
@@ -546,10 +546,10 @@ Hypothesis H : F -| U.
 Let eta : eta_type F U := AdjointFunctor.eta H.
 Let eps : eps_type F U := AdjointFunctor.eps H.
 
-Definition uni : idfun ~~> (U0 \o U) \o (F \o F0) :=
+Definition uni : up_idfun ~~> (U0 \o U) \o (F \o F0) :=
   fun A : UU0 => U0 # eta (F0 A) \o eta0 A.
 
-Let uni_naturality : naturality idfun ((U0 \o U) \o (F \o F0)) uni.
+Let uni_naturality : naturality up_idfun ((U0 \o U) \o (F \o F0)) uni.
 Proof.
 move=> A B h; rewrite FIdE.
 rewrite -[RHS]compA.
@@ -558,13 +558,13 @@ rewrite [LHS]compA.
 rewrite [RHS]compA.
 congr (_ \o _).
 rewrite (FCompE U0 F0) -[in RHS](@functor_o U0) -[in LHS](@functor_o U0).
-congr (_ # _).
+congr (U0 # _).
 by rewrite -(natural (AdjointFunctor.eta H)).
 Qed.
 
 HB.instance Definition _ := isNatural.Build _ _ uni uni_naturality.
 
-Definition couni : (F \o F0) \o (U0 \o U) ~~> idfun :=
+Definition couni : (F \o F0) \o (U0 \o U) ~~> up_idfun :=
   fun A : UU0 => eps A \o F # eps0 (U A).
 
 Let couni_naturality : naturality ((F \o F0) \o (U0 \o U)) _ couni.
@@ -594,7 +594,7 @@ apply: (@AdjointFunctor.mk _ _ uni couni).
 rewrite /TriangularLaws.right => A.
 rewrite /couni /uni /=.
 rewrite compA -[RHS](AdjointFunctor.tri_right H0 (U A)); congr (_ \o _).
-rewrite FCompE -functor_o; congr (_ # _).
+rewrite FCompE -functor_o; congr (U0 # _).
 rewrite functor_o -compA -FCompE.
 rewrite (natural (AdjointFunctor.eta H)) FIdE.
 by rewrite compA (AdjointFunctor.tri_right H) compidf.
@@ -640,11 +640,11 @@ Qed.
 
 End algebraic_operation_interface.
 
-(*Lemma monad_of_ret_bind_ext (F G : functor) (RET1 : idfun ~> F) (RET2 : idfun ~> G)
+(*Lemma monad_of_ret_bind_ext (F G : functor) (RET1 : up_idfun ~> F) (RET2 : up_idfun ~> G)
   (bind1 : forall A B : UU0, F A -> (A -> F B) -> F B)
   (bind2 : forall A B : UU0, G A -> (A -> G B) -> G B) :
   forall (FG : F = G),
-  RET1 = eq_rect _ (fun m : functor => idfun ~> m) RET2 _ ((*beuh*) (esym FG)) ->
+  RET1 = eq_rect _ (fun m : functor => up_idfun ~> m) RET2 _ ((*beuh*) (esym FG)) ->
   bind1 = eq_rect _ (fun m : functor => forall A B : UU0, m A -> (A -> m B) -> m B) bind2 _ (esym FG) ->
   forall H1 K1 H2 K2 H3 K3,
   Monad_of_ret_bind F RET1 bind1 H1 H2 H3 =
@@ -698,10 +698,9 @@ Proof. by []. Qed.
 Lemma naturality_mpair (M : monad) (A B : UU0) (f : A -> B) (g : A -> M A):
   (M # f^`2) \o (mpair \o g^`2) = mpair \o ((M # f) \o g)^`2.
 Proof.
-apply boolp.funext => -[a0 a1].
-rewrite compE fmap_bind.
-rewrite compE mpairE compE bind_fmap; bind_ext => a2.
-rewrite fcompE fmap_bind 2!compE bind_fmap; bind_ext => a3.
+apply/boolp.funext => -[a0 a1]/=.
+rewrite fmap_bind bind_fmap; bind_ext => a2/=.
+rewrite fcompE fmap_bind bind_fmap; bind_ext => a3/=.
 by rewrite fcompE -(compE (M # f^`2)) (natural ret) FIdE.
 Qed.
 
diff --git a/theories/lib/proba_lib.v b/theories/lib/proba_lib.v
index e2c3f4dc..35a2a16d 100644
--- a/theories/lib/proba_lib.v
+++ b/theories/lib/proba_lib.v
@@ -173,15 +173,15 @@ Lemma uniform_naturality (M : probMonad R) (A B : Type) (a : A) (b : B) (f : A -
   forall x, (0 < size x)%nat ->
   ((@uniform M _ b) \o map f) x = ((M # f) \o uniform a) x.
 Proof.
-elim=> // x [_ _|x' xs]; first by rewrite [in RHS]compE fmapE bindretf.
+elim=> // x [_ _|x' xs]; first by rewrite /= fmapE bindretf.
 move/(_ isT) => IH _.
-rewrite compE [in RHS]compE.
+rewrite (compE (uniform b)) (compE _ (uniform a)).
 rewrite [x' :: xs]lock [in LHS]uniform_cons -/(map _ _) [in LHS]/= -lock.
 rewrite [x' :: xs]lock [in RHS]uniform_cons -/(map _ _) [in RHS]/= -lock.
 set p := (X in _ <| X |> _ = _).
 rewrite (_ : probinvn _ = p); last first.
   by apply val_inj; rewrite /= size_map.
-move: IH; rewrite 2!compE => ->.
+move: IH => /= ->.
 by rewrite [in RHS]fmapE choice_bindDl bindretf fmapE.
 Qed.
 Arguments uniform_naturality {M A B}.
@@ -192,7 +192,7 @@ Lemma mpair_uniform_base_case (M : probMonad R) (A : Type) a x (y : seq A) :
 Proof.
 move=> y0; rewrite cp1.
 transitivity (@uniform M _ a y >>= (fun y' => Ret (x, y'))).
-  by rewrite -(compE (uniform _)) (uniform_naturality a) // compE fmapE.
+  by rewrite -(compE (uniform _)) (uniform_naturality a) //= fmapE.
 transitivity (do z <- Ret x; do y' <- uniform a y; Ret (z, y') : M _)%Do.
   by rewrite bindretf.
 by [].
diff --git a/theories/lib/state_lib.v b/theories/lib/state_lib.v
index 6dc2ae76..b8590cf2 100644
--- a/theories/lib/state_lib.v
+++ b/theories/lib/state_lib.v
@@ -446,8 +446,8 @@ Lemma promote_assert_sufficient_condition (M : failMonad) (A : UU0) :
 Proof.
 move=> right_z p q promotable_pq.
 rewrite /promote_assert; apply: boolp.funext => -[x1 x2].
-rewrite 3![in RHS]compE [in RHS]fmapE.
-rewrite 2![in LHS]compE {1}/bassert [in LHS]bind_fmap !bindA.
+rewrite /= [in RHS]fmapE.
+rewrite /= {1}/bassert [in LHS]bind_fmap !bindA.
 bind_ext => s.
 rewrite bindA; under eq_bind do rewrite bindretf.
 case: assertPn => ps; last first.
@@ -566,16 +566,16 @@ Proof.
 apply: boolp.funext => -[n1 n2].
 elim: n1 => [|n1 IH].
   rewrite [in LHS]compE uaddnE add0n.
-  rewrite compE [in X in _ = _ X]/= squaringE symbols0.
-  rewrite compE [in RHS]fmapE bindA bindretf.
+  rewrite -[RHS]/(fmap _ _) squaringE symbols0.
+  rewrite [in RHS]fmapE bindA bindretf.
   rewrite -fmapE fmap_bind.
   Open (X in _ >>= X).
     rewrite fcompE fmapE bindretf /=; reflexivity.
   by rewrite bindmret.
-rewrite compE uaddnE addSn symbolsS -uaddnE -(compE symbols) {}IH.
-rewrite [in RHS]compE [in X in _ = _ X]/= squaringE symbolsS.
-rewrite [in RHS]compE -/(fmap _ _) fmap_bind bindA; bind_ext => a.
-rewrite 2![in LHS]compE [in LHS]fmap_bind [in LHS]bindA [in RHS]bindA.
+rewrite [in LHS]compE uaddnE addSn symbolsS -uaddnE -(compE symbols) {}IH.
+rewrite -[RHS]/(fmap _ _) squaringE symbolsS.
+rewrite -/(fmap _ _) fmap_bind bindA; bind_ext => a.
+rewrite /= [in LHS]fmap_bind [in LHS]bindA [in RHS]bindA.
 bind_ext => s.
 rewrite [in RHS]bindretf [in RHS]fcompE [in RHS]fmap_bind.
 rewrite [in LHS]fcompE [in LHS]bind_fmap [in LHS]bindA.
diff --git a/theories/models/elgot_model.v b/theories/models/elgot_model.v
index 24ae7c66..c50646a8 100644
--- a/theories/models/elgot_model.v
+++ b/theories/models/elgot_model.v
@@ -3,7 +3,7 @@
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require boolp.
 From HB Require Import structures.
-Require Import hierarchy monad_lib fail_lib state_lib trace_lib.
+Require Import preamble hierarchy monad_lib fail_lib state_lib trace_lib.
 Require Import monad_transformer monad_model.
 
 (**md**************************************************************************)
@@ -148,7 +148,7 @@ case: sba => [[b''|a''] s''] /=.
 Qed.
 
 Lemma codiagonal {A B} (f : A -> elgotS ((B + A) + A)) (a : A) :
-  while ((elgotS # ((sum_rect (fun => (B + A)%type) idfun inr))) \o f) a
+  while ((elgotS # ((sum_rect (fun => (B + A)%type) up_idfun inr))) \o f) a
   ≈
   while (while f) a.
 Proof.
@@ -160,8 +160,8 @@ apply: wBisim_trans.
 rewrite -codiagonalwB elgotS_map.
 apply: whilewB => -[] a'' s'' //=.
 rewrite //= !fmapE.
-have -> : ((reader S \o M) \o writer S) # sum_rect (fun=> (B + A)%type) idfun inr =
-          reader S # (M # (writer S # sum_rect (fun=> (B + A)%type) idfun inr)).
+have -> : ((reader S \o M) \o writer S) # sum_rect (fun=> (B + A)%type) up_idfun inr =
+          reader S # (M # (writer S # sum_rect (fun=> (B + A)%type) up_idfun inr)).
   by rewrite -compA FCompE.
 rewrite reader_map /= fmapE !bindA.
 by apply: bindfwB => -[[[bl|al']|al] sl]; rewrite !bindretf /= fmapE !bindretf.
@@ -275,7 +275,7 @@ move=> [u|[b''|a'']] /=.
 Qed.
 
 Lemma codiagonal {A B} (f : A -> elgotX ((B + A) + A)) (a : A) :
-  while ((elgotX # (sum_rect (fun => (B + A)%type) idfun inr)) \o f ) a
+  while ((elgotX # (sum_rect (fun => (B + A)%type) up_idfun inr)) \o f ) a
   ≈
   while (while f) a.
 Proof.
@@ -387,7 +387,7 @@ case: (StopP (ElgotX.while f x)) =>
 - rewrite steps_Now in Hs.
   move: x x' Hx Hs.
   elim: n => [/=|n IH] x x' Hx;
-             rewrite ElgotXwhileE whileE /ElgotX.elgotXA functions.compE fmapE.
+             rewrite ElgotXwhileE whileE /ElgotX.elgotXA compE fmapE.
   + case Hb: (f x) => [uxx|d].
     * case: uxx Hb => [u//|[y/=|y/=]] Hb;
                       rewrite bindretf/=bindretf.
diff --git a/theories/models/gcm_model.v b/theories/models/gcm_model.v
index 8c1c1ca4..680cff01 100644
--- a/theories/models/gcm_model.v
+++ b/theories/models/gcm_model.v
@@ -128,7 +128,7 @@ End free_choiceType_functor.
 
 Section forget_choiceType_functor.
 
-Let m : CC -> CT := idfun.
+Let m : CC -> CT := up_idfun.
 
 Let h (a b : CC) (f : {hom a -> b}) : {hom[CT] m a -> m b} :=
   Hom.Pack (Hom.Class (isHom.Axioms_ (a : CT) (b : _) (FId # f) I)).
@@ -152,7 +152,7 @@ Local Notation FC := free_choiceType.
 Local Notation UC := forget_choiceType.
 
 Let epsC' : FC \O UC ~~> FId := fun A : CC => Hom.Pack (Hom.Class
-  (isHom.Axioms_ ((FC \O UC) A) (FId A) idfun I)).
+  (isHom.Axioms_ ((FC \O UC) A) (FId A) up_idfun I)).
 
 Lemma epsC'_natural : naturality _ _ epsC'. Proof. by []. Qed.
 
@@ -160,11 +160,11 @@ HB.instance Definition _ := isNatural.Build _ _ _ _ _ epsC'_natural.
 
 Definition epsC := locked [the _ ~> _ of epsC'].
 
-Lemma epsCE (T : choiceType) : epsC T = idfun :> (_ -> _).
+Lemma epsCE (T : choiceType) : epsC T = up_idfun :> (_ -> _).
 Proof. by rewrite /epsC; unlock. Qed.
 
 Let etaC' : FId ~~> UC \O FC :=
-      fun (_ : CT) => Hom.Pack (Hom.Class (isHom.Axioms_ (FId _) ((UC \O FC) _) idfun I)).
+      fun (_ : CT) => Hom.Pack (Hom.Class (isHom.Axioms_ (FId _) ((UC \O FC) _) up_idfun I)).
 
 Lemma etaC'_natural : naturality _ _ etaC'.
 Proof. by []. Qed.
@@ -173,7 +173,7 @@ HB.instance Definition _ := isNatural.Build _ _ _ _ _ etaC'_natural.
 
 Definition etaC := locked [the _ ~> _ of etaC'].
 
-Lemma etaCE (T : Type) : etaC T = idfun :> (_ -> _).
+Lemma etaCE (T : Type) : etaC T = up_idfun :> (_ -> _).
 Proof. by rewrite /etaC; unlock. Qed.
 
 Import comps_notation.
@@ -191,7 +191,7 @@ Local Obligation Tactic := idtac.
 
 Variable R : realType.
 
-Let affine_idfun' (U : convType R) : affine (@idfun U). Proof. by []. Qed.
+Let affine_idfun' (U : convType R) : affine (@up_idfun U). Proof. by []. Qed.
 
 Let affine_comp' (a b c : convType R) (f : a -> b) (g : b -> c) :
   affine f -> affine g -> affine (g \o f).
@@ -264,7 +264,7 @@ End free_convType_functor.
 Section forget_convType_functor.
 Variable R : realType.
 
-Let m1 : CV R -> CC := idfun.
+Let m1 : CV R -> CC := up_idfun.
 
 Let h1 := fun (a b : CV R) (f : {hom[CV R] a -> b}) =>
   Hom.Pack (Hom.Class (isHom.Axioms_ (m1 a) (m1 b) f I)).
@@ -373,8 +373,12 @@ by move=> ? ? /=; rewrite af ag.
 Qed.
 
 Let idfun_is_biglub_affine (a : semiCompSemiLattConvType R) :
-  biglub_affine (@idfun a).
-Proof. by split => //; exact: biglub_morph. Qed.
+  biglub_affine (@up_idfun a).
+Proof.
+(* rewrite idfun -> ssrfun.idfun is necessary here because BiglubMorph is
+   instantiated only for ssrfun.idfun, not for polymorphic up_idfun *)
+by split => //; rewrite (_ : up_idfun = ssrfun.idfun)//; exact: biglub_morph.
+Qed.
 
 HB.instance Definition _ := isCategory.Build (semiCompSemiLattConvType R)
   (fun U : semiCompSemiLattConvType R => U) biglub_affine idfun_is_biglub_affine
@@ -517,7 +521,7 @@ End free_semiCompSemiLattConvType_functor.
 Section forget_semiCompSemiLattConvType_functor.
 Variable R : realType.
 
-Let m2 : CS R -> CV R := idfun.
+Let m2 : CS R -> CV R := up_idfun.
 
 Let h2 := fun (a b : CS R) (f : {hom[CS R] a -> b}) => Hom.Pack (Hom.Class
   (isHom.Axioms_ (m2 a) (m2 b) f (scsl_hom_is_affine f))).
@@ -737,7 +741,7 @@ apply/necset_ext.
 rewrite /= /join_ /= /Monad_of_category_monad.join /= !HCompId !HIdComp eps1E.
 rewrite functor_o NEqE functor_id compfid.
 rewrite 2!VCompE_nat HCompId HIdComp.
-set E := epsC _; have->: E = [hom idfun] by apply/hom_ext; rewrite epsCE.
+set E := epsC _; have->: E = [hom up_idfun] by apply/hom_ext; rewrite epsCE.
 rewrite functor_id_hom.
 rewrite !functor_o functor_id !compfid.
 set F1J := F1 # _.
@@ -783,7 +787,7 @@ congr fsdistbind.
 by apply: funext => x; rewrite fsdist1bind.
 Qed.
 
-Lemma RetE T : (Ret : idfun T -> N T) = (Ret : FId T -> M R T).
+Lemma RetE T : (Ret : up_idfun T -> N T) = (Ret : FId T -> M R T).
 Proof.
 apply: funext => t /=.
 rewrite /ret_ [in LHS]/=.
diff --git a/theories/models/monad_model.v b/theories/models/monad_model.v
index e08e0233..46bea624 100644
--- a/theories/models/monad_model.v
+++ b/theories/models/monad_model.v
@@ -149,12 +149,12 @@ End assoc.
 Module IdentityMonad.
 Section identitymonad.
 Let bind := fun A B (a : A) (f : A -> B) => f a.
-Let left_neutral : BindLaws.left_neutral bind (NId idfun).
+Let left_neutral : BindLaws.left_neutral bind (NId up_idfun).
 Proof. by []. Qed.
-Let right_neutral : BindLaws.right_neutral bind (NId idfun).
+Let right_neutral : BindLaws.right_neutral bind (NId up_idfun).
 Proof. by []. Qed.
 Let associative : BindLaws.associative bind. Proof. by []. Qed.
-Let acto := (@idfun UU0).
+Let acto := (@up_idfun UU0).
 HB.instance Definition _ := isMonad_ret_bind.Build
   acto left_neutral right_neutral associative.
 End identitymonad.
@@ -165,7 +165,7 @@ Module ListMonad.
 Section listmonad.
 Definition acto := fun A : UU0 => seq A.
 Local Notation M := acto.
-Let ret : idfun ~~> M := fun (A : UU0) x => (@cons A) x [::].
+Let ret : up_idfun ~~> M := fun (A : UU0) x => (@cons A) x [::].
 Let bind := fun A B (m : M A) (f : A -> M B) => flatten (map f m).
 Let left_neutral : BindLaws.left_neutral bind ret.
 Proof. by move=> A B m f; rewrite /bind /ret /= cats0. Qed.
@@ -191,7 +191,7 @@ Section setmonad.
 Local Open Scope classical_set_scope.
 Definition acto := set.
 Local Notation M := acto.
-Let ret : idfun ~~> M := @set1.
+Let ret : up_idfun ~~> M := @set1.
 Let bind := fun A B => @bigcup B A.
 Let left_neutral : BindLaws.left_neutral bind ret.
 Proof. move=> ? ? ? ?; exact: bigcup_set1. Qed.
@@ -216,7 +216,7 @@ Section exceptmonad.
 Variable E : UU0.
 Definition acto := fun A : UU0 => (E + A)%type.
 Local Notation M := acto.
-Let ret : idfun ~~> M := @inr E.
+Let ret : up_idfun ~~> M := @inr E.
 Let bind := fun A B (m : M A) (f : A -> M B) =>
   match m with inl z => inl z | inr b => f b end.
 Let left_neutral : BindLaws.left_neutral bind ret.
@@ -264,7 +264,7 @@ Section output.
 Variable L : UU0.
 Definition acto := fun X : UU0 => (X * seq L)%type.
 Local Notation M := acto.
-Let ret : idfun ~~> M := fun A a => (a, [::]).
+Let ret : up_idfun ~~> M := fun A a => (a, [::]).
 Let bind := fun (A B : UU0) (m : M A) (f : A -> M B) =>
   let: (x, w) := m in let: (x', w') := f x in (x', w ++ w').
 Let left_neutral : BindLaws.left_neutral bind ret.
@@ -292,7 +292,7 @@ Section reader.
 Variable E : UU0.
 Definition acto := fun A : UU0 => E -> A.
 Local Notation M := acto.
-Definition ret : idfun ~~> M := fun A x => fun e => x.
+Definition ret : up_idfun ~~> M := fun A x => fun e => x.
 (* computation that ignores the environment *)
 Let bind := fun (A B : UU0) (m : M A) (f : A -> M B) => fun e => f (m e) e.
 (* binds m f applied the same environment to m and to the result of f *)
@@ -318,7 +318,7 @@ Section state.
 Variable S : UU0. (* type of states *)
 Definition acto := fun A : UU0 => S -> A * S.
 Local Notation M := acto.
-Let ret : idfun ~~> M := fun A a => fun s => (a, s).
+Let ret : up_idfun ~~> M := fun A a => fun s => (a, s).
 Let bind := fun (A B : UU0) (m : M A) (f : A -> M B) => uncurry f \o m.
 Let left_neutral : BindLaws.left_neutral bind ret.
 Proof. by move=> A B a f; apply boolp.funext. Qed.
@@ -348,7 +348,7 @@ Section cont.
 Variable r : UU0. (* the type of answers *)
 Definition acto := fun A : UU0 => (A -> r) -> r.
 Local Notation M := acto.
-Let ret : idfun ~~> M := fun A a => fun k => k a.
+Let ret : up_idfun ~~> M := fun A a => fun k => k a.
 Let bind := fun (A B : UU0) (m : M A) (f : A -> M B) => fun k => m (fun a => f a k).
 Let left_neutral : BindLaws.left_neutral bind ret.
 Proof. by move=> A B a f; apply boolp.funext => Br. Qed.
@@ -1135,7 +1135,7 @@ Proof. by rewrite /addM bindretf; apply boolp.funext. Abort.
 Fixpoint list_iter (M : monad) A (f : A -> M unit) (s : seq A) : M unit :=
   if s is h :: t then f h >> list_iter f t else Ret tt.
 
-Compute (@list_iter [the monad of idfun] nat (fun a => Ret tt) [:: O; 1; 2]).
+Compute (@list_iter [the monad of up_idfun] nat (fun a => Ret tt) [:: O; 1; 2]).
 
 Definition list_find (M : contMonad) (A : UU0) (p : pred A) (s : seq A) : M _ :=
   callcc (fun k => list_iter (fun x => if p x then (*Throw*) k (Some x) else Ret tt) s >> Ret None).
@@ -1251,7 +1251,7 @@ Proof.
 move=> A B m0 f s.
 rewrite state_bindE.
 rewrite /uncurry /=.
-rewrite /comp /= /reify /=.
+rewrite /(_ \o _) /= /reify /=.
 by case (m0 s).
 Qed.
 HB.instance Definition _ := isMonadReify.Build state_trace (StateMonad.acto state_trace)
@@ -1291,7 +1291,7 @@ Definition acto : Type -> Type :=
   fun A => S -> {fset (choice_of_Type A * choice_of_Type S)}.
 Local Notation M := acto.
 
-Let ret : idfun ~~> M := fun A (a : A) s =>
+Let ret : up_idfun ~~> M := fun A (a : A) s =>
   [fset (a : choice_of_Type A, s : choice_of_Type S)].
 
 Let bind := fun A B (m : acto A)
@@ -1572,7 +1572,7 @@ Variable (S : UU0) (I : eqType).
 Implicit Types i j : I.
 Definition acto (A : UU0) := (I -> S) -> SetMonad.acto (A * (I -> S))%type.
 Local Notation M := acto.
-Let ret : idfun ~~> M := fun A a => fun s => [set (a, s)].
+Let ret : up_idfun ~~> M := fun A a => fun s => [set (a, s)].
 Let bind := fun A B (m : M A) (f : A -> M B) => fun s => m s >>= uncurry f.
 Let left_neutral : BindLaws.left_neutral bind ret.
 Proof.
@@ -1740,7 +1740,7 @@ Variable (S : UU0) (I : eqType).
 Implicit Types i j : I.
 Definition acto (A : UU0) := unit.
 Local Notation M := acto.
-Let ret : idfun ~~> M := fun A a => tt.
+Let ret : up_idfun ~~> M := fun A a => tt.
 Let bind := fun A B (m : M A) (f : A -> M B) => tt : M B.
 Let left_neutral : BindLaws.left_neutral bind ret.
 Proof. by move=> ? ? x f; case: (f x). Qed.
@@ -1883,7 +1883,7 @@ End eq_rect_bind.
 (*Section instantiations_with_the_identity_monad.
 
 Lemma stateT_id_ModelState S :
-  stateT S [the monad of idfun] = [the monad of StateMonad.acto S].
+  stateT S [the monad of up_idfun] = [the monad of StateMonad.acto S].
 Proof.
 rewrite /= /stateTmonadM /=.
 have FG : MS_functor S ModelMonad.identity = ModelMonad.State.functor S.
@@ -1924,7 +1924,7 @@ End instantiations_with_the_identity_monad.*)
 
 Section monad_transformer_calcul.
 
-Let contTi T := MC T [the monad of idfun].
+Let contTi T := MC T [the monad of up_idfun].
 
 Definition break_if_none (m : monad) (break : _) (acc : nat) (x : option nat) : m nat :=
   if x is Some x then Ret (x + acc) else break acc.
diff --git a/theories/models/typed_store_transformer.v b/theories/models/typed_store_transformer.v
index b6bd67c0..409eabd8 100644
--- a/theories/models/typed_store_transformer.v
+++ b/theories/models/typed_store_transformer.v
@@ -490,7 +490,7 @@ Local Notation coq_type := (@coq_type MLU N).
 
 Local Notation ml_type := (MLU : Type).
 
-Definition acto := ModelTypedStore.acto ml_type N idfun.
+Definition acto := ModelTypedStore.acto ml_type N up_idfun.
 Local Notation M := acto.
 
 Local Notation loc := (@loc ml_type locT_nat).