diff --git a/Modules/NonRawSignatures/FullArToRaw.v b/Modules/NonRawSignatures/FullArToRaw.v
index 7e810a4..47f4b3f 100644
--- a/Modules/NonRawSignatures/FullArToRaw.v
+++ b/Modules/NonRawSignatures/FullArToRaw.v
@@ -35,13 +35,13 @@ Require Import Modules.Signatures.HArityDerivation.
 (* Require Import Modules.Signatures.CheckCorrespondanceAdjonction. *)
 Require Import UniMath.SubstitutionSystems.BindingSigToMonad.
 
-Require Import UniMath.CategoryTheory.categories.category_hset.
+Require Import UniMath.CategoryTheory.Categories.category_hset.
 
-Require Import UniMath.CategoryTheory.categories.category_hset_structures.
-Require Import UniMath.CategoryTheory.limits.coproducts.
-Require Import UniMath.CategoryTheory.limits.binproducts.
-Require Import UniMath.CategoryTheory.limits.bincoproducts.
-Require Import UniMath.CategoryTheory.limits.terminal.
+Require Import UniMath.CategoryTheory.Categories.category_hset_structures.
+Require Import UniMath.CategoryTheory.Limits.Coproducts.
+Require Import UniMath.CategoryTheory.Limits.BinProducts.
+Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
 
 Require Import Modules.Prelims.deriveadj.
 
@@ -71,7 +71,7 @@ Section CoBindingArity.
 (** Content of this section:
     - translate a natural number into a half-arity
 *)
-  
+
 Fixpoint nat_deriv_HAr {C : category} bcp T (n :nat) : arity C :=
   match n with
     0 => tautological_harity
@@ -88,7 +88,7 @@ Definition nat_prod_HAr {C : category} (bp : BinProducts C) (n : nat) : arity C
   iter_functor (prodHAr bp) n tautological_harity.
 
 Definition CoBinding_to_FullArity {C : category} bcp T ( a : HAr.arity C)
-           (n : nat) 
+           (n : nat)
   : FullArity C
   :=  a ,, nat_deriv_HAr bcp T n.
 
@@ -96,7 +96,7 @@ Context {C : category} .
 Hypothesis ( bp : BinProducts C).
 Let bpHAr := harity_BinProducts (C := C) bp.
 Local Notation BPO := (BinProductObject _).
-  
+
   (* Let prodHAr  := *)
   (*   (functor_fix_snd_arg _ _ _  (binproduct_functor  (harity_BinProducts bp )) *)
   (*                        (tautological_harity)). *)
@@ -105,7 +105,7 @@ Local Notation BPO := (BinProductObject _).
 (*   iter_functor prodHAr n a. *)
 
 (** Input: an arity [a] and a natural number
-    Output: [a × θ × θ × ... × θ] 
+    Output: [a × θ × θ × ... × θ]
 *)
 Fixpoint DeBind_HArity  (a : HAr.arity C) (n : nat) : HAr.arity C :=
   match n with
@@ -155,13 +155,13 @@ Section NoSetGenNat.
   (* Local Notation "×ℜ" :=  (bpM. *)
   Local Notation Θ :=  (tautological_LModule).
 
-  Let deriv_pb_iso {R S : Monad C} (f : Monad_Mor R S) 
+  Let deriv_pb_iso {R S : Monad C} (f : Monad_Mor R S)
       : ∏ M, iso (C := MOD R) (pb_LModule f (M ')) ((pb_LModule f M) ')
     :=
     pb_deriv_to_deriv_pb_iso Tset bcp (D := C) f.
 
-  Let bp_pb_iso {R S : Monad C} (f : Monad_Mor R S) 
-    : ∏ M N, iso (C := MOD R) 
+  Let bp_pb_iso {R S : Monad C} (f : Monad_Mor R S)
+    : ∏ M N, iso (C := MOD R)
                  (bpM _ (pb_LModule f M)(pb_LModule f N) )
                  (pb_LModule f (bpM _ M N))
     :=
@@ -240,7 +240,7 @@ M×R ---------> f* A x f* S ------> f*(A x S) -------> f* B
   Let c_n n : HalfArity := DeBind_HArity bp   a n.
   Let d_n n : FullArity C := c_n n ,, tautological_harity.
 
-  Definition equiv_is_rep_ar_one_to_raw (a' : HalfArity) n R : 
+  Definition equiv_is_rep_ar_one_to_raw (a' : HalfArity) n R :
                  LModule_Mor R (a' R)(nat_d_HAr (S n) R) ≃
                              LModule_Mor R (BPO (LMOD_bp R (a' R) (tautological_LModule R)))
                              (nat_d_HAr n R).
@@ -248,7 +248,7 @@ M×R ---------> f* A x f* S ------> f*(A x S) -------> f* B
     apply adj1.
   Defined.
 
-  Definition equiv_is_rep_ar_to_raw (a' : HalfArity) n R : 
+  Definition equiv_is_rep_ar_to_raw (a' : HalfArity) n R :
                  LModule_Mor R (a' R)( nat_d_HAr n R) ≃
                              LModule_Mor R ((DeBind_HArity bp a' n : HAr.arity _) R)
                              (tautological_LModule R).
@@ -357,7 +357,7 @@ M×R ---------> f* A x f* S ------> f*(A x S) -------> f* B
       apply (transport_arity_mor _ _ _ _ _ e xx yy ff).
   Defined.
 
-  
+
   Definition FAr_to_HAr_one_functor n : (rep_disp C)[{a_n (S n)}] ⟶ (rep_disp C)[{b_n n}] :=
     _ ,, FAr_to_HAr_one_is_functor n.
 
@@ -371,7 +371,7 @@ M×R ---------> f* A x f* S ------> f*(A x S) -------> f* B
 End NoSetGenNat.
 
 Section FAR_ToHAR_Rep.
-  
+
   Context {C : category}.
   Hypothesis ( bp : BinProducts C).
   Hypothesis ( bcp : BinCoproducts C).
@@ -401,13 +401,13 @@ Section FAR_ToHAR_Rep.
   (* Local Notation "×ℜ" :=  (bpM. *)
   Local Notation Θ :=  (tautological_LModule).
 
-  Let deriv_pb_iso {R S : Monad C} (f : Monad_Mor R S) 
+  Let deriv_pb_iso {R S : Monad C} (f : Monad_Mor R S)
       : ∏ M, iso (C := MOD R) (pb_LModule f (M ')) ((pb_LModule f M) ')
     :=
     pb_deriv_to_deriv_pb_iso Tset bcp (D := C) f.
 
-  Let bp_pb_iso {R S : Monad C} (f : Monad_Mor R S) 
-    : ∏ M N, iso (C := MOD R) 
+  Let bp_pb_iso {R S : Monad C} (f : Monad_Mor R S)
+    : ∏ M N, iso (C := MOD R)
                  (bpM _ (pb_LModule f M)(pb_LModule f N) )
                  (pb_LModule f (bpM _ M N))
     :=
@@ -438,7 +438,7 @@ Par l'adjonction ça doit devenir
 M x R ----> N --------> f*A
 
 *)
-  
+
   Hypothesis adj_law1 :
                 ∏ R S (f : Monad_Mor (C := C) R S)
                   (M N : LModule R _) (A : LModule S _)
@@ -520,7 +520,7 @@ Section NoSet.
   Lemma HAr_rep_ar_mor_law_nt {a b : HAr.arity _} (M : HAr.rep_ar _ a)
              (N : HAr.rep_ar _ b)
            (f : arity_Mor a b) (g : Monad_Mor M N) :
-  HAr.rep_ar_mor_law _ M N f g ≃ 
+  HAr.rep_ar_mor_law _ M N f g ≃
                      ((HAr.rep_τ _ M : (MOD _ ⟦_,_⟧))  · (monad_mor_to_lmodule g)  =
                       ((#a g)%ar : MOD _ ⟦_,_⟧)  ·
                                                  pb_LModule_Mor g
@@ -546,12 +546,12 @@ Section NoSet.
 
   (*inutile TODO suppriemr *)
 Definition FAr_rep_ar_mor_law_nt {a b : FullArity C} (M : rep_ar _ a) (N : rep_ar _ b)
-           (f : FullArity C ⟦ a,  b⟧) (g : Monad_Mor M N) : 
+           (f : FullArity C ⟦ a,  b⟧) (g : Monad_Mor M N) :
   rep_ar_mor_law C M N f g ≃ (
    (rep_τ _ M : MOD _ ⟦_ , _⟧)  · ((#(codom a) g)%ar)  =
             ((#(dom a) g)%ar : MOD _ ⟦_ , _⟧)  · pb_LModule_Mor g (dom_mor f N)  ·
                                                pb_LModule_Mor g (rep_τ _ N)  ·
-                                               pb_LModule_Mor g (codom_mor f N) 
+                                               pb_LModule_Mor g (codom_mor f N)
                    ).
 Proof.
     apply weqinvweq.
@@ -630,7 +630,7 @@ Defined.
   Local Notation BPO := (BinProductObject _).
   Let b n : HalfArity := BPO (bpHAr a (nat_p_HAr n)).
 
-  Definition equiv_is_rep_ar_to_raw R : 
+  Definition equiv_is_rep_ar_to_raw R :
                  LModule_Mor R (a R)(nat_d_HAr 1 R) ≃
                              LModule_Mor R (b 1 R)(tautological_LModule R).
   Proof.
@@ -664,13 +664,13 @@ Defined.
 (*   rep_ar_mor_law  M N f g ≃  (rep_τ M : nat_trans _ _) · ((#(codom a) g)%ar:nat_trans _ _)  = *)
 (*             ((#(dom a) g)%ar:nat_trans _ _)  · dom_mor f N  · *)
 (*                                             rep_τ N c · codom_mor f N c. *)
-  Let deriv_pb_iso {R S : Monad C} (f : Monad_Mor R S) 
+  Let deriv_pb_iso {R S : Monad C} (f : Monad_Mor R S)
       : ∏ M, iso (C := MOD R) (pb_LModule f (M ')) ((pb_LModule f M) ')
     :=
     pb_deriv_to_deriv_pb_iso Tset bcp (D := C) f.
 
-  Let bp_pb_iso {R S : Monad C} (f : Monad_Mor R S) 
-    : ∏ M N, iso (C := MOD R) 
+  Let bp_pb_iso {R S : Monad C} (f : Monad_Mor R S)
+    : ∏ M N, iso (C := MOD R)
                  (bpM _ (pb_LModule f M)(pb_LModule f N) )
                  (pb_LModule f (bpM _ M N))
     :=
@@ -720,7 +720,7 @@ M×R ---------> f* A x f* S ------> f*(A x S) -------> f* B
                                                       · pb_LModule_Mor f (adj1 _ _ _ v)
 
                 (* (# ×ℜ (dirprodpair (u : MOD R ⟦_,_⟧) (monad_mor_to_lmodule f : MOD R ⟦_,_⟧))) *)
-                
+
 
                 (* adj1 R  _ _  ((u : MOD R ⟦_,_⟧) · (pb_LModule_Mor f v) · deriv_pb_iso f _) *)
              ).
@@ -750,7 +750,7 @@ M×R ---------> f* A x f* S ------> f*(A x S) -------> f* B
     apply idweq.
   Qed.
 
-  Definition equiv_raw_ar_mor_law 
+  Definition equiv_raw_ar_mor_law
      {R S : rep_ar _ (a_n 1)} (f : Monad_Mor R S) :
                       rep_ar_mor_law _ R S (identity _) f ≃
                                      HAr.rep_ar_mor_law _ (Fob R) (Fob S)
@@ -811,6 +811,6 @@ M×R ---------> f* A x f* S ------> f*(A x S) -------> f* B
   Definition iso_FAr_HAr_rep : catiso _ _ :=
      FS,, (λ x y  , weqproperty (Fmor x y)),, weqproperty Fob.
 End NoSet.
-  
+
 
 *)
diff --git a/Modules/NonRawSignatures/HArityCoproductFromColims.v b/Modules/NonRawSignatures/HArityCoproductFromColims.v
index 88e1e44..180bebe 100644
--- a/Modules/NonRawSignatures/HArityCoproductFromColims.v
+++ b/Modules/NonRawSignatures/HArityCoproductFromColims.v
@@ -17,8 +17,8 @@ Require Import UniMath.CategoryTheory.DisplayedCats.Auxiliary.
 Require Import UniMath.CategoryTheory.DisplayedCats.Core.
 Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
 
-Require Import UniMath.CategoryTheory.limits.coproducts.
-Require Import UniMath.CategoryTheory.limits.graphs.colimits.
+Require Import UniMath.CategoryTheory.Limits.Coproducts.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
 
 Require Import Modules.Prelims.lib.
 Require Import Modules.Prelims.modules.
@@ -110,7 +110,7 @@ Section pullback_coprod.
     etrans;[apply assoc|].
 
     etrans;[apply id_left|apply id_right].
-  
+
   Definition coprod_pbm_to_pbm_coprod : LModule_Mor  _ coprod_pbm pbm_coprod.
     use tpair.
     - use tpair
@@ -150,4 +150,4 @@ Section Coprod.
     : arity_on_morphisms  (R : Monad C) : LModule R C :=
     CoproductObject _ _ (LModule_coproducts_from_Colims R (fun o => α o R)).
 
-  Definition harity_coprod : HalfSignature.
\ No newline at end of file
+  Definition harity_coprod : HalfSignature.
diff --git a/Modules/NonRawSignatures/PresentableRawSig.v b/Modules/NonRawSignatures/PresentableRawSig.v
index 675f103..151657a 100644
--- a/Modules/NonRawSignatures/PresentableRawSig.v
+++ b/Modules/NonRawSignatures/PresentableRawSig.v
@@ -14,8 +14,8 @@ Require Import UniMath.CategoryTheory.DisplayedCats.Auxiliary.
 Require Import UniMath.CategoryTheory.DisplayedCats.Core.
 Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
 
-Require Import UniMath.CategoryTheory.limits.coproducts.
-Require Import UniMath.CategoryTheory.limits.initial.
+Require Import UniMath.CategoryTheory.Limits.Coproducts.
+Require Import UniMath.CategoryTheory.Limits.Initial.
 
 Require Import Modules.Prelims.lib.
 Require Import Modules.Prelims.modules.
@@ -29,9 +29,9 @@ Require Import Modules.Signatures.RawSigToHAr.
 Require Import Modules.Signatures.PresentableHArityCoproducts.
 Require Import Modules.Signatures.PresentableArity.
 Require  Modules.Signatures.FullSignatures.
-Require Import UniMath.CategoryTheory.categories.category_hset.
+Require Import UniMath.CategoryTheory.Categories.category_hset.
 
-Require Import UniMath.CategoryTheory.categories.category_hset_structures.
+Require Import UniMath.CategoryTheory.Categories.category_hset_structures.
 Module FAr := FullSignatures.
 
 Section RawSigRep.
@@ -54,14 +54,14 @@ Local Notation EndSet := [hset_category, hset_category].
 
     (** This uses univalence to transform an isomorphism of category into an equality
        Another proof could be used without univalence though
-       
+
      *)
   Lemma initial_presentable_raw_sig (ax:  AxiomOfChoice.AxiomOfChoice_surj): Initial (precategory_rep_sig (rawSigToSig rawsig)).
   Proof.
     eapply (transportb (fun X => Initial X)).
     apply catiso_to_precategory_path.
     - intros ? ? .
-      apply isaset_rep_a_sig_mor. 
+      apply isaset_rep_a_sig_mor.
     - unshelve apply iso_a_sig_har_rep.
       apply cp.
       apply setproperty.
diff --git a/Modules/NonRawSignatures/PresentableSig.v b/Modules/NonRawSignatures/PresentableSig.v
index a9dd65b..6efe675 100644
--- a/Modules/NonRawSignatures/PresentableSig.v
+++ b/Modules/NonRawSignatures/PresentableSig.v
@@ -14,8 +14,8 @@ Require Import UniMath.CategoryTheory.DisplayedCats.Auxiliary.
 Require Import UniMath.CategoryTheory.DisplayedCats.Core.
 Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
 
-Require Import UniMath.CategoryTheory.limits.coproducts.
-Require Import UniMath.CategoryTheory.limits.initial.
+Require Import UniMath.CategoryTheory.Limits.Coproducts.
+Require Import UniMath.CategoryTheory.Limits.Initial.
 Require Import UniMath.CategoryTheory.EpiFacts.
 Require Import UniMath.CategoryTheory.Epis.
 
@@ -38,9 +38,9 @@ Require  Modules.Signatures.FullSignatures.
 Require Import Modules.Signatures.FullArToRaw.
 Require Import Modules.Signatures.SigEquivRep.
 Require Import Modules.Prelims.SetCatComplements.
-Require Import UniMath.CategoryTheory.categories.category_hset.
+Require Import UniMath.CategoryTheory.Categories.category_hset.
 
-Require Import UniMath.CategoryTheory.categories.category_hset_structures.
+Require Import UniMath.CategoryTheory.Categories.category_hset_structures.
 Module FAr := FullSignatures.
 
 Section RawSigRep.
@@ -63,17 +63,17 @@ Local Notation bpSET := BinProductsHSET.
     : hSet := pr1 S.
 Local Notation O := base_of_pres_sig.
 
-Definition ar_of_pres_sig 
+Definition ar_of_pres_sig
              {C} {bpC} {bcpC} {Tc} {cpC}
              (S : PresentableSignature (C:=C)bpC bcpC Tc cpC)
   : O S -> arity C := fun o => (pr1 (pr1 (pr2 S o))).
-Definition ar_of_pres_sig_isPresentable 
+Definition ar_of_pres_sig_isPresentable
              {C} {bpC} {bcpC} {Tc} {cpC}
              (S : PresentableSignature (C:=C)bpC bcpC Tc cpC)
   : ∏ o,   isPresentable bpC bcpC Tc cpC (ar_of_pres_sig S o):= fun o => (pr2 (pr1 (pr2 S o))).
 
 Local Notation α := ar_of_pres_sig.
-Definition nat_of_pres_sig 
+Definition nat_of_pres_sig
              {C} {bpC} {bcpC} {Tc} {cpC}
              (S : PresentableSignature (C:=C)bpC bcpC Tc cpC)
   : O S -> nat := fun o => ( (pr2 (pr2 S o))).
@@ -104,7 +104,7 @@ Import FullSignatures.
 
     (** This uses univalence to transform an isomorphism of category into an equality
        Another proof could be used without univalence though
- (@DeBind_HArity SET bpSET a n',, @tautological_harity SET)      
+ (@DeBind_HArity SET bpSET a n',, @tautological_harity SET)
 (@DeBind_HArity SET bpSET a n',, @tautological_harity SET)
      *)
 
@@ -160,14 +160,14 @@ Lemma initial_presentable_raw_sig sig (ax:  AxiomOfChoice.AxiomOfChoice_surj) :
              (PresentableSignature_to_signature (C:=SET) bp bcp T
                                                 (fun I => cp _ (setproperty I))  sig)).
 Proof.
-  set (sig' := PresentableSignature_to_signature _ _  _ _ sig). 
+  set (sig' := PresentableSignature_to_signature _ _  _ _ sig).
   eapply (transportb (fun X => Initial X)).
   apply catiso_to_precategory_path.
   - intros ? ? .
-    apply isaset_rep_a_sig_mor. 
+    apply isaset_rep_a_sig_mor.
   - exact (catiso_Presentable_Raw sig).
   - (* This is a presentable raw signature, so it is representable *)
-    set (rawS := 
+    set (rawS :=
            tpair (T := hSet) (fun z => z -> arity _)
                  (O sig)
                  (λ o : O sig, DeBind_HArity (C := SET) bpSET (α _ o) (nat_of_pres_sig _ o)) : rawSig).
diff --git a/Modules/NonRawSignatures/RawSigToHAr.v b/Modules/NonRawSignatures/RawSigToHAr.v
index c97a5ec..d5d72e4 100644
--- a/Modules/NonRawSignatures/RawSigToHAr.v
+++ b/Modules/NonRawSignatures/RawSigToHAr.v
@@ -31,7 +31,7 @@ Require Import UniMath.CategoryTheory.DisplayedCats.Auxiliary.
 Require Import UniMath.CategoryTheory.DisplayedCats.Core.
 Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
 
-Require Import UniMath.CategoryTheory.limits.coproducts.
+Require Import UniMath.CategoryTheory.Limits.Coproducts.
 
 Require Import Modules.Prelims.lib.
 Require Import Modules.Prelims.modules.
@@ -74,7 +74,7 @@ Check ((fun a => idpath _):  ∏ a, (rep_ar C a) = (FAr.rep_ar C (toAr a))).
 
 
 (* useless *)
-Lemma half_arity_to_arity_is_rep_weq (a : HalfArity) (M N : rep_ar C a) f : 
+Lemma half_arity_to_arity_is_rep_weq (a : HalfArity) (M N : rep_ar C a) f :
   FAr.rep_ar_mor_law C (a := toAr a) (b:=toAr a) M N (identity _) f
                      ≃
   rep_ar_mor_law C (a :=  a) (b:= a) M N (identity (C := arity_category) _) f.
@@ -150,7 +150,7 @@ Definition sig_to_har_rep_on_mor_weq (R S : a_sig_rep) : a_sig_rep ⟦ R , S ⟧
     split.
     + intro  h .
       intro x.
-      
+
       cbn.
       unfold coproduct_nat_trans_data.
       repeat rewrite id_right.
diff --git a/Modules/NonRawSignatures/SigEquivRep.v b/Modules/NonRawSignatures/SigEquivRep.v
index d1da5e1..6f7547a 100644
--- a/Modules/NonRawSignatures/SigEquivRep.v
+++ b/Modules/NonRawSignatures/SigEquivRep.v
@@ -9,16 +9,16 @@ Require Import UniMath.Foundations.Propositions.
 Require Import UniMath.Foundations.Sets.
 
 Require Import UniMath.CategoryTheory.Categories.
-Require Import UniMath.CategoryTheory.categories.category_hset.
+Require Import UniMath.CategoryTheory.Categories.category_hset.
 
-Require Import UniMath.CategoryTheory.categories.category_hset_structures.
+Require Import UniMath.CategoryTheory.Categories.category_hset_structures.
 Require Import UniMath.CategoryTheory.functor_categories.
 
 Require Import UniMath.CategoryTheory.Epis.
-Require Import UniMath.CategoryTheory.limits.coproducts.
-Require Import UniMath.CategoryTheory.limits.bincoproducts.
-Require Import UniMath.CategoryTheory.limits.binproducts.
-Require Import UniMath.CategoryTheory.limits.terminal.
+Require Import UniMath.CategoryTheory.Limits.Coproducts.
+Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
+Require Import UniMath.CategoryTheory.Limits.BinProducts.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
 Require Import UniMath.CategoryTheory.EpiFacts.
 Require Import UniMath.Combinatorics.Lists.
 Require Import UniMath.CategoryTheory.whiskering.
@@ -33,7 +33,7 @@ Require Import UniMath.CategoryTheory.catiso.
 
 
 Require Import UniMath.CategoryTheory.Monads.Monads.
-Require Import UniMath.CategoryTheory.Monads.LModules. 
+Require Import UniMath.CategoryTheory.Monads.LModules.
 Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
 Require Import UniMath.CategoryTheory.DisplayedCats.Auxiliary.
 Open Scope cat.
@@ -76,7 +76,7 @@ Section SigEquiv.
   Let Σ' : signature C := _ ,, α'.
 
   (* inspiré de rawsigtohar *)
-  Definition sig_to_sig_rep_weq : sig_rep Σ ≃ sig_rep Σ'. 
+  Definition sig_to_sig_rep_weq : sig_rep Σ ≃ sig_rep Σ'.
   Proof.
     apply weqfibtototal.
     intro R.
@@ -156,7 +156,7 @@ Section SigEquivRawSig.
 
 Local Notation toAr := half_arity_to_arity.
 (* bizarre qu'on en ait pas besoin avant *)
-Lemma half_arity_to_arity_is_rep_weq (a : HAr.arity _) (M N : HAr.rep_ar C a) f : 
+Lemma half_arity_to_arity_is_rep_weq (a : HAr.arity _) (M N : HAr.rep_ar C a) f :
   HAr.rep_ar_mor_law C (a := a) (b:= a) M N (identity (C := arity_category) _) f
                      ≃
   rep_ar_mor_law C (a := toAr a) (b:=toAr a) M N (identity _) f.
@@ -176,7 +176,7 @@ Defined.
 
   (* TODO : refaire la suite avec ce qu'il y a dasn RawSigToHAr *)
   (* inspiré de rawsigtohar *)
-  Definition sig_to_sig_rep_weq : sig_rep Σ ≃ sig_rep Σ'. 
+  Definition sig_to_sig_rep_weq : sig_rep Σ ≃ sig_rep Σ'.
   Proof.
     apply weqfibtototal.
     intro R.
@@ -222,4 +222,4 @@ Defined.
   Definition iso_sig_sig_rep : catiso (sig_rep Σ) (sig_rep Σ')
     := FS,, (λ x y : sig_rep Σ, weqproperty (FSmor x y)),, weqproperty FSob.
 End SigEquivRawSig.
-*)
\ No newline at end of file
+*)
diff --git a/Modules/Prelims/BinCoproductComplements.v b/Modules/Prelims/BinCoproductComplements.v
index 4be2978..398d205 100644
--- a/Modules/Prelims/BinCoproductComplements.v
+++ b/Modules/Prelims/BinCoproductComplements.v
@@ -8,8 +8,8 @@ Require Import UniMath.Foundations.Sets.
 
 Require Import UniMath.CategoryTheory.Core.Prelude.
 
-Require Import UniMath.CategoryTheory.limits.coproducts.
-Require Import UniMath.CategoryTheory.limits.bincoproducts.
+Require Import UniMath.CategoryTheory.Limits.Coproducts.
+Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
 
 
 
@@ -35,4 +35,4 @@ Definition BinCoproducts_from_CoproductsBool {C : category} (bc : Coproducts boo
       * use (CoproductInCommutes _ _ _ CC _ _ true).
     + intros h; apply isapropdirprod; apply homset_property.
     + (intros h [H1 H2]; apply CoproductArrowUnique; intro x; induction x); assumption.
-Defined.
\ No newline at end of file
+Defined.
diff --git a/Modules/Prelims/BinProductComplements.v b/Modules/Prelims/BinProductComplements.v
index 7ee1ca0..ae42585 100644
--- a/Modules/Prelims/BinProductComplements.v
+++ b/Modules/Prelims/BinProductComplements.v
@@ -14,21 +14,21 @@ Require Import UniMath.SubstitutionSystems.SignatureCategory.
 Require Import UniMath.SubstitutionSystems.BinProductOfSignatures.
 
 Require Import UniMath.CategoryTheory.Core.Prelude.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 
 Require Import UniMath.CategoryTheory.Epis.
-Require Import UniMath.CategoryTheory.limits.coproducts.
-Require Import UniMath.CategoryTheory.limits.bincoproducts.
-Require Import UniMath.CategoryTheory.limits.coproducts.
-Require Import UniMath.CategoryTheory.limits.binproducts.
-Require Import UniMath.CategoryTheory.limits.terminal.
+Require Import UniMath.CategoryTheory.Limits.Coproducts.
+Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
+Require Import UniMath.CategoryTheory.Limits.Coproducts.
+Require Import UniMath.CategoryTheory.Limits.BinProducts.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
 Require Import UniMath.CategoryTheory.EpiFacts.
 
 Open Scope cat.
 
 Section BinProdComplements.
   Context {C : category}.
-  
+
   Definition BinProductOfArrows_eq (CC : BinProducts C) a b c d (f f' : a --> c) (g g' : b --> d)
     : f = f' → g = g' →
       BinProductOfArrows _ _ _ f g = BinProductOfArrows _ (CC _ _) (CC _ _) f' g'.
@@ -37,8 +37,8 @@ Section BinProdComplements.
     induction 1.
     apply idpath.
   Qed.
-  
-  
+
+
   Definition BinProduct_commutative {a b : C} (bpab : BinProduct _ a b) (bpba : BinProduct _ b a)
     : C ⟦BinProductObject _ bpab, BinProductObject _ bpba ⟧
    := BinProductArrow C bpba (BinProductPr2 C bpab) (BinProductPr1 C bpab).
@@ -68,13 +68,13 @@ Section BinProdComplements.
   Definition BinProduct_pw_iso_mor {a b a' b' : C} (bp_ab : BinProduct _ a b)
              (bp_ab' : BinProduct _ a' b') (isoa : iso a a') (isob : iso b b') :
     C ⟦ BPO bp_ab, BPO bp_ab'⟧ :=
-    BinProductOfArrows C bp_ab' bp_ab isoa isob. 
+    BinProductOfArrows C bp_ab' bp_ab isoa isob.
 
   Lemma BinProduct_pw_eq_id  {a b a' b' : C} (bp_ab : BinProduct _ a b)
              (bp_ab' : BinProduct _ a' b') (isoa : iso a a') (isob : iso b b') :
     BinProduct_pw_iso_mor bp_ab bp_ab' isoa isob · BinProduct_pw_iso_mor bp_ab' bp_ab
-                          (iso_inv_from_iso isoa) 
-                          (iso_inv_from_iso isob) = 
+                          (iso_inv_from_iso isoa)
+                          (iso_inv_from_iso isob) =
     identity (BPO bp_ab).
   Proof.
    etrans;[apply postcompWithBinProductArrow|].
@@ -92,7 +92,7 @@ Section BinProdComplements.
   Proof.
     - use make_is_inverse_in_precat.
       + apply BinProduct_pw_eq_id.
-      + 
+      +
         etrans.
         {
         apply cancel_precomposition.
diff --git a/Modules/Prelims/CoproductsComplements.v b/Modules/Prelims/CoproductsComplements.v
index 7aee12c..5c8f44e 100644
--- a/Modules/Prelims/CoproductsComplements.v
+++ b/Modules/Prelims/CoproductsComplements.v
@@ -16,8 +16,8 @@ Require Import UniMath.MoreFoundations.Tactics.
 
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.ProductCategory.
-Require Import UniMath.CategoryTheory.limits.coproducts.
-Require Import UniMath.CategoryTheory.limits.binproducts.
+Require Import UniMath.CategoryTheory.Limits.Coproducts.
+Require Import UniMath.CategoryTheory.Limits.BinProducts.
 
 Require Import UniMath.CategoryTheory.Epis.
 Require Import UniMath.CategoryTheory.EpiFacts.
@@ -169,9 +169,9 @@ Section CoprodSigma.
   (* We show that cp2 is a coproduct *)
   Definition sigma_coprod_In o  : C ⟦ BS o , CPO cp2 ⟧ :=
     CoproductIn _ C (cp1 (pr1 o)) (pr2 o) · CoproductIn O C cp2 (pr1 o).
-    
+
   (** Is it possible to define it without using the homset property ? *)
-  Definition sigma_coprod_isCoproduct : isCoproduct _ _ _ _ sigma_coprod_In. 
+  Definition sigma_coprod_isCoproduct : isCoproduct _ _ _ _ sigma_coprod_In.
     intros c f.
     use unique_exists.
     -  apply CoproductArrow.
@@ -219,7 +219,7 @@ Section CoprodEpis.
           (cpa : Coproduct _ _ a)
           (cpb : Coproduct _ _ b).
 
-  Context {ff : ∏ i, C ⟦ a i, b i ⟧} (epif : ∏ i, isEpi (ff i)). 
+  Context {ff : ∏ i, C ⟦ a i, b i ⟧} (epif : ∏ i, isEpi (ff i)).
 
   Lemma CoproductOfArrows_isEpi : isEpi (CoproductOfArrows _ _ cpa cpb ff).
   Proof.
@@ -262,18 +262,18 @@ Section CoprodBinprod.
   Definition bp_coprod_mor  : C ⟦ CPO (cpBX) , BPO bpCX ⟧ :=
     CoproductArrow _ _ _ bp_coprod_In.
 
-    
+
 
 
 End CoprodBinprod.
 
 Definition bp_coprod_isDistributive {C : category} {I : UU}
-           (bp : BinProducts C) (cp : Coproducts I C) 
+           (bp : BinProducts C) (cp : Coproducts I C)
   : UU :=
   ∏ B X, is_iso (bp_coprod_mor (cp B) (fun o => bp _ X) (bp _ _) (cp _) ).
 
 Definition iso_from_isDistributive  {C : category} {I : UU}
-           (bp : BinProducts C) (cp : Coproducts I C) 
+           (bp : BinProducts C) (cp : Coproducts I C)
            (h :  bp_coprod_isDistributive bp cp) B X :
   iso _ _ :=
   make_iso (bp_coprod_mor (cp B) (fun o => bp _ X) (bp _ _) (cp _) )
@@ -317,7 +317,7 @@ Section CoprodPwIso.
       intro i.
       rewrite <- h.
       do 2 rewrite assoc.
-      rewrite iso_after_iso_inv. 
+      rewrite iso_after_iso_inv.
       apply cancel_postcomposition.
       apply pathsinv0.
       apply id_left.
@@ -328,10 +328,10 @@ Section CoprodPwIso.
   Definition coprod_pw_iso : iso (CPO cpB) (CPO cpB') :=
     (iso_from_Coproduct_to_Coproduct _ cpB cpB'2).
   End CoprodPwIso.
-    
 
 
 
 
 
-  
+
+
diff --git a/Modules/Prelims/DerivationIsFunctorial.v b/Modules/Prelims/DerivationIsFunctorial.v
index cd1c716..cce2224 100644
--- a/Modules/Prelims/DerivationIsFunctorial.v
+++ b/Modules/Prelims/DerivationIsFunctorial.v
@@ -20,7 +20,7 @@ Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.
 
 Require Import UniMath.CategoryTheory.Adjunctions.Core.
 Require Import UniMath.CategoryTheory.whiskering.
-Require Import UniMath.CategoryTheory.limits.bincoproducts.
+Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
 Require Import UniMath.CategoryTheory.UnitorsAndAssociatorsForEndofunctors.
 
 Require Import Modules.Prelims.lib.
@@ -29,7 +29,7 @@ Require Import UniMath.SubstitutionSystems.ModulesFromSignatures.
 Section DerivFunctor.
   Context {C : category}
           (o : C) (* derivation X ↦ X + o *)
-          (bcpC : limits.bincoproducts.BinCoproducts C )
+          (bcpC : Limits.BinCoproducts.BinCoproducts C )
           {D : category}
           (T : Monad C).
 
@@ -94,7 +94,7 @@ MR(X+o)) --------->  NR(X+o)
       apply pre_whisker_composition.
   Qed.
 
-  Definition LModule_deriv_functor  : functor LMOD LMOD := make_functor _ LModule_deriv_is_functor. 
+  Definition LModule_deriv_functor  : functor LMOD LMOD := make_functor _ LModule_deriv_is_functor.
 
   Local Notation "∂" := LModule_deriv_functor.
 
diff --git a/Modules/Prelims/EpiComplements.v b/Modules/Prelims/EpiComplements.v
index 7224782..97aff7d 100644
--- a/Modules/Prelims/EpiComplements.v
+++ b/Modules/Prelims/EpiComplements.v
@@ -23,15 +23,15 @@ Require Import UniMath.CategoryTheory.Epis.
 
 Require Import UniMath.CategoryTheory.HorizontalComposition.
 
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 Require Import UniMath.CategoryTheory.Epis.
 Require Import UniMath.CategoryTheory.EpiFacts.
 Require Import UniMath.CategoryTheory.SplitMonicsAndEpis.
-Require Import UniMath.CategoryTheory.limits.graphs.colimits.
-Require Import UniMath.CategoryTheory.limits.binproducts.
-Require Import UniMath.CategoryTheory.limits.bincoproducts.
-Require Import UniMath.CategoryTheory.limits.terminal.
-Require Import UniMath.CategoryTheory.limits.coproducts.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
+Require Import UniMath.CategoryTheory.Limits.BinProducts.
+Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
+Require Import UniMath.CategoryTheory.Limits.Coproducts.
 
 Require Import Modules.Prelims.lib.
 
@@ -96,15 +96,15 @@ Lemma productEpisFunc {B C : category} bpC
 Proof.
   red.
   intros a b f a' b' f' epif epif'.
-  apply is_nat_trans_epi_from_pointwise_epis. 
-  intro X. 
+  apply is_nat_trans_epi_from_pointwise_epis.
+  intro X.
   apply prEpi; apply pwEpi;[exact epif| exact epif'].
 Qed.
 
-                                                          
+
 (**
  morphisms between  colimits of same shape preserve epis *)
-Lemma colimOfArrows_Epi 
+Lemma colimOfArrows_Epi
            {C : precategory} {g : graph} {d1 d2 : diagram g C}
            (CC1 : ColimCocone d1) (CC2 : ColimCocone d2)
            (f : ∏ u : vertex g, C ⟦ dob d1 u, dob d2 u ⟧)
@@ -155,7 +155,7 @@ Qed.
 
 (** Again, a corrollary, in principle *)
 Lemma bincoproduct_Epis {C : category} {a b a' b'}
-      (ab : BinCoproduct a b) 
+      (ab : BinCoproduct a b)
       (a'b' : BinCoproduct a' b')
       (f : C ⟦a , a'⟧)(g : C ⟦b , b'⟧)
       (epif : isEpi f)(epig : isEpi g) :
@@ -267,7 +267,7 @@ Proof.
   apply product_epis; [apply epiF|apply epiG]; exact epif.
 Qed.
 
-Definition preserveEpi_binProdFuncSET {B  : category} 
+Definition preserveEpi_binProdFuncSET {B  : category}
       (F F' : functor B SET) :
   preserves_Epi F -> preserves_Epi F' -> preserves_Epi (BinProduct_of_functors _ _ _ F F') :=
   preserveEpi_binProdFunc productEpisSET F F'.
@@ -291,7 +291,7 @@ Qed.
 
 
 (** a corollary *)
-Lemma preserveEpi_sumFuncs {B C : category} {I : UU}(cp : Coproducts I C) 
+Lemma preserveEpi_sumFuncs {B C : category} {I : UU}(cp : Coproducts I C)
       Fs (epiFs : ∏ i, preserves_Epi (Fs i)) :
     preserves_Epi (coproduct_of_functors  I B C cp Fs).
 Proof.
@@ -303,7 +303,7 @@ Proof.
 Qed.
 
 (** Corollary *)
-Lemma preserveEpi_binCoprodFunc {B C : category} (bcp : BinCoproducts C) 
+Lemma preserveEpi_binCoprodFunc {B C : category} (bcp : BinCoproducts C)
       Fs Gs (epiFs : preserves_Epi Fs)(epiGs : preserves_Epi Gs) :
     preserves_Epi (BinCoproduct_of_functors B C bcp  Fs Gs).
 Proof.
@@ -329,7 +329,7 @@ Lemma preserves_Epi_option {B : category} (bcp : BinCoproducts B) (T : Terminal
 Proof.
   intros R S f epif.
   intros c u v eq.
-  apply BinCoproductArrowsEq; [apply (identity_isEpi _ (x := T))| apply epif]; 
+  apply BinCoproductArrowsEq; [apply (identity_isEpi _ (x := T))| apply epif];
     do 2 rewrite assoc;
     [erewrite <- BinCoproductOfArrowsIn1|erewrite <- BinCoproductOfArrowsIn2];
     do 2 rewrite <- assoc;
diff --git a/Modules/Prelims/FaithfulFibrationEqualizer.v b/Modules/Prelims/FaithfulFibrationEqualizer.v
index 59519ef..b688cfb 100644
--- a/Modules/Prelims/FaithfulFibrationEqualizer.v
+++ b/Modules/Prelims/FaithfulFibrationEqualizer.v
@@ -15,17 +15,17 @@ Require Import UniMath.Foundations.Propositions.
 Require Import UniMath.Foundations.Sets.
 
 Require Import UniMath.CategoryTheory.Core.Prelude.
-Require Import UniMath.CategoryTheory.limits.pushouts.
-Require Import UniMath.CategoryTheory.limits.initial.
+Require Import UniMath.CategoryTheory.Limits.Pushouts.
+Require Import UniMath.CategoryTheory.Limits.Initial.
 
 
 Require Import UniMath.CategoryTheory.DisplayedCats.Core.
 Require Import UniMath.CategoryTheory.DisplayedCats.Total.
 Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.
-Require Import UniMath.CategoryTheory.limits.graphs.colimits.
-Require Import UniMath.CategoryTheory.limits.graphs.limits.
-Require Import UniMath.CategoryTheory.limits.graphs.equalizers.
-Require Import UniMath.CategoryTheory.limits.graphs.coequalizers.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Limits.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Equalizers.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Coequalizers.
 
 Require Import Modules.Prelims.Opfibration.
 
@@ -86,7 +86,7 @@ This can be reformulated as [faithful pr1_category) as in [faithful_pr1_category
         * cbn -[isaprop].
           intro y.
           apply (homset_property (total_category D)).
-        * 
+        *
           intros h'2 eqh'2.
           apply faithful_reformulated.
           cbn.
@@ -148,7 +148,7 @@ This can be reformulated as [faithful pr1_category) as in [faithful_pr1_category
         * cbn -[isaprop].
           intro y.
           apply (homset_property (total_category D)).
-        * 
+        *
           intros h'2 eqh'2.
           apply faithful_reformulated.
           cbn.
diff --git a/Modules/Prelims/FibrationInitialPushout.v b/Modules/Prelims/FibrationInitialPushout.v
index f1bfbed..67feb28 100644
--- a/Modules/Prelims/FibrationInitialPushout.v
+++ b/Modules/Prelims/FibrationInitialPushout.v
@@ -39,8 +39,8 @@ Require Import UniMath.Foundations.PartD.
 Require Import UniMath.Foundations.Propositions.
 Require Import UniMath.Foundations.Sets.
 Require Import UniMath.CategoryTheory.Core.Prelude.
-Require Import UniMath.CategoryTheory.limits.pushouts.
-Require Import UniMath.CategoryTheory.limits.initial.
+Require Import UniMath.CategoryTheory.Limits.Pushouts.
+Require Import UniMath.CategoryTheory.Limits.Initial.
 
 
 Require Import UniMath.CategoryTheory.DisplayedCats.Core.
@@ -68,7 +68,7 @@ If there is a morphism f : x → y  in C, then there is a unique morphism over f
 *)
   Definition disp_InitialArrow {x y : C} {xx : dC x} {yy : dC y}
         (init : isInitial  (fiber_category _ _) xx)
-        (f : C ⟦ x, y ⟧) := 
+        (f : C ⟦ x, y ⟧) :=
                                             transportf _ (id_left f)
                                             (iscontrpr1 (init _);; (cl _ _ f yy ))%mor_disp.
 
@@ -92,7 +92,7 @@ If there is a morphism f : x → y  in C, then there is a unique morphism over f
       apply (maponpaths (fun x => (x;; _)%mor_disp)) .
       apply iscontr_uniqueness.
   Qed.
-  
+
 
   Context
           {c0 c1 c2 c' : C}
diff --git a/Modules/Prelims/LModulesBinProducts.v b/Modules/Prelims/LModulesBinProducts.v
index cd8f390..5f2b912 100644
--- a/Modules/Prelims/LModulesBinProducts.v
+++ b/Modules/Prelims/LModulesBinProducts.v
@@ -23,8 +23,8 @@ Require Import UniMath.MoreFoundations.Tactics.
 
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.whiskering.
-Require Import UniMath.CategoryTheory.limits.terminal.
-Require Import UniMath.CategoryTheory.limits.binproducts.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
+Require Import UniMath.CategoryTheory.Limits.BinProducts.
 Require Import UniMath.CategoryTheory.Monads.Monads.
 Require Import UniMath.CategoryTheory.Monads.LModules.
 
diff --git a/Modules/Prelims/LModulesColims.v b/Modules/Prelims/LModulesColims.v
index cf0edff..7e5714e 100644
--- a/Modules/Prelims/LModulesColims.v
+++ b/Modules/Prelims/LModulesColims.v
@@ -26,8 +26,8 @@ Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.FunctorCategory.
 
 Require Import UniMath.CategoryTheory.whiskering.
-Require Import UniMath.CategoryTheory.limits.graphs.limits.
-Require Import UniMath.CategoryTheory.limits.graphs.colimits.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Limits.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
 Require Import UniMath.CategoryTheory.Monads.Monads.
 Require Import UniMath.CategoryTheory.Monads.LModules.
 
@@ -37,11 +37,11 @@ Require Import UniMath.CategoryTheory.Monads.LModules.
 Local Open Scope cat.
 
 (*
-Lemma compfNat 
-   {C : precategory} {g : graph} {d1 d2 d3 : diagram g C}  
-   
+Lemma compfNat
+   {C : precategory} {g : graph} {d1 d2 d3 : diagram g C}
+
    {f : ∏ u : vertex g, C ⟦ dob d1 u, dob d2 u ⟧}
-  (fNat : ∏ (u v : vertex g) (e : edge u v), dmor d1 e · f v = f u · dmor d2 e) 
+  (fNat : ∏ (u v : vertex g) (e : edge u v), dmor d1 e · f v = f u · dmor d2 e)
    {f2 : ∏ u : vertex g, C ⟦ dob d2 u, dob d3 u ⟧}
    (fNat2 : ∏ (u v : vertex g) (e : edge u v), dmor d2 e · f2 v = f2 u · dmor d3 e)
    (f3 := fun u => f u · f2 u)
@@ -58,12 +58,12 @@ Qed.
 *)
 (*
 Lemma compColimOfArrows
-   (C : precategory) (g : graph) (d1 d2 d3 : diagram g C) (CC1 : ColimCocone d1) 
+   (C : precategory) (g : graph) (d1 d2 d3 : diagram g C) (CC1 : ColimCocone d1)
    (CC2 : ColimCocone d2)(CC3 : ColimCocone d3)
    (f : ∏ u : vertex g, C ⟦ dob d1 u, dob d2 u ⟧)
-  (fNat : ∏ (u v : vertex g) (e : edge u v), dmor d1 e · f v = f u · dmor d2 e) 
+  (fNat : ∏ (u v : vertex g) (e : edge u v), dmor d1 e · f v = f u · dmor d2 e)
    (f2 : ∏ u : vertex g, C ⟦ dob d2 u, dob d3 u ⟧)
-  (fNat2 : ∏ (u v : vertex g) (e : edge u v), dmor d2 e · f2 v = f2 u · dmor d3 e) 
+  (fNat2 : ∏ (u v : vertex g) (e : edge u v), dmor d2 e · f2 v = f2 u · dmor d3 e)
   (x : C) (cc : cocone d2 x) :
   colimOfArrows CC1 CC2 f fNat · colimOfArrows CC2 CC3 f2 fNat2 =
   colimOfArrows CC1 CC3 (fun z => f z · f2 z) (compfNat  fNat fNat2).
@@ -81,7 +81,7 @@ Lemma compColimOfArrows
 
   reflexivity.
 .fNat · colimOfArrows CC2 CC3 f2 fNat2 .
-  colimOfArrows CC1 CC3 (fun 
+  colimOfArrows CC1 CC3 (fun
   colimArrow CC1 x
     (make_cocone (λ u : vertex g, f u · coconeIn cc u)
        (preCompWithColimOfArrows_subproof CC1 CC2 f fNat x cc)).
@@ -90,7 +90,7 @@ Lemma compColimOfArrows
 (* TODO déplacer ça dans LModule.v *)
 
 Section ColimsModule.
-  Context 
+  Context
           {C : category}
           {g : graph} (colims_g : Colims_of_shape g C)
           (lims_g : Lims_of_shape g C)
@@ -120,7 +120,7 @@ Section ColimsModule.
   Definition LModule_colim_mult_data (x : B) : C ⟦ (R ∙ F) x, F x ⟧.
     use colimOfArrows.
     - intro v.
-       exact ( lm_mult R (dob d v : LModule _ _) x). 
+       exact ( lm_mult R (dob d v : LModule _ _) x).
     - intros u v e.
       cbn.
         now apply  LModule_Mor_σ.
@@ -129,7 +129,7 @@ Section ColimsModule.
   Definition LModule_lim_mult_data (x : B) : C ⟦ (R ∙ F') x, F' x ⟧.
     use limOfArrows.
     - intro v.
-       exact ( lm_mult R (dob d v : LModule _ _) x). 
+       exact ( lm_mult R (dob d v : LModule _ _) x).
     - intros u v e.
       cbn.
       apply pathsinv0.
@@ -143,7 +143,7 @@ Section ColimsModule.
     - intro v.
       eapply compose; revgoals.
       + apply (colimIn _ v).
-      + exact ( lm_mult R (dob d v : LModule _ _) x). 
+      + exact ( lm_mult R (dob d v : LModule _ _) x).
     - intros u v e.
       cbn.
       (*
@@ -193,7 +193,7 @@ qu'on complète par propriété de [d e] en temps que morphisme de module
     apply colimArrowUnique.
     intro v.
     cbn.
-    
+
     apply pathsinv0.
     etrans;[apply assoc|].
     etrans.
@@ -201,7 +201,7 @@ qu'on complète par propriété de [d e] en temps que morphisme de module
       apply cancel_postcomposition.
       apply (nat_trans_ax (lm_mult R (dob d v : LModule _ _))).
     }
-    
+
     apply pathsinv0.
     etrans;[apply assoc|].
     etrans.
@@ -232,7 +232,7 @@ qu'on complète par propriété de [d e] en temps que morphisme de module
     apply limArrowUnique.
     intro v.
     cbn.
-    
+
     (* apply pathsinv0. *)
     etrans;[|apply assoc].
     etrans; revgoals.
@@ -241,7 +241,7 @@ qu'on complète par propriété de [d e] en temps que morphisme de module
       apply pathsinv0.
       apply (nat_trans_ax (lm_mult R (dob d v : LModule _ _))).
     }
-    
+
     apply pathsinv0.
     etrans;[|apply assoc].
     etrans; revgoals.
@@ -269,7 +269,7 @@ qu'on complète par propriété de [d e] en temps que morphisme de module
 
   Definition LModule_lim_mult : R ∙ F' ⟹ F' :=
     (_ ,, LModule_lim_mult_is_nat_trans).
-  
+
 
   Definition LModule_colim_data : LModule_data R C :=
     (F ,, LModule_colim_mult).
@@ -395,7 +395,7 @@ qu'on complète par propriété de [d e] en temps que morphisme de module
   Definition LModule_colim : LModule R C := (_ ,, LModule_colim_laws).
   Definition LModule_lim : LModule R C := (_ ,, LModule_lim_laws).
 
-  Lemma LModule_coconeIn_laws v : 
+  Lemma LModule_coconeIn_laws v :
     LModule_Mor_laws R
                      (T := (dob d v : LModule _ _)) (T' := LModule_colim)
       ((coconeIn (colimCocone (coFunc d')) v : nat_trans _ _) ).
@@ -407,9 +407,9 @@ qu'on complète par propriété de [d e] en temps que morphisme de module
     set (CC2 := colims_g _ ).
     apply (colimOfArrowsIn _ _ CC1 CC2).
   Defined.
-  Lemma LModule_coneOut_laws v : 
+  Lemma LModule_coneOut_laws v :
     LModule_Mor_laws R
-                    (T := LModule_lim) (T' := (dob d v : LModule _ _)) 
+                    (T := LModule_lim) (T' := (dob d v : LModule _ _))
       ((coneOut (limCone (limFunc d')) v : nat_trans _ _) ).
   Proof.
     intro c.
@@ -474,7 +474,7 @@ qu'on complète par propriété de [d e] en temps que morphisme de module
 
   Definition LModule_limArrow_laws {M : LModule R C} (cc : cone d M) :
     LModule_Mor_laws
-      _ (T := M)(T' := LModule_lim) 
+      _ (T := M)(T' := LModule_lim)
       (limArrow  (limFunc d') (M : functor _ _) (@mapcone (category_LModule R C) _ FORGET _ d _ cc) : nat_trans _ _ ).
   Proof.
     intro c.
@@ -566,12 +566,12 @@ Definition LModule_Lims_of_shape (C : category) {B : category}
            (d : diagram g (category_LModule R C))
             : LimCone d :=
   LModule_LimCone  lims_g d.
-                                         
+
 
 
 
 Section pullback_lims.
-  Context 
+  Context
           {D : category}
           {g : graph} (colims_g : Colims_of_shape g D)
           (lims_g : Lims_of_shape g D)
diff --git a/Modules/Prelims/LModulesCoproducts.v b/Modules/Prelims/LModulesCoproducts.v
index 66d78e3..3200086 100644
--- a/Modules/Prelims/LModulesCoproducts.v
+++ b/Modules/Prelims/LModulesCoproducts.v
@@ -12,7 +12,7 @@ Require Import UniMath.MoreFoundations.Tactics.
 
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.whiskering.
-Require Import UniMath.CategoryTheory.limits.coproducts.
+Require Import UniMath.CategoryTheory.Limits.Coproducts.
 Require Import UniMath.CategoryTheory.Monads.Monads.
 Require Import UniMath.CategoryTheory.Monads.LModules.
 Local Open Scope cat.
diff --git a/Modules/Prelims/Opfibration.v b/Modules/Prelims/Opfibration.v
index 0c52870..749f98a 100644
--- a/Modules/Prelims/Opfibration.v
+++ b/Modules/Prelims/Opfibration.v
@@ -10,7 +10,7 @@ of this file)
 Require Import UniMath.Foundations.Sets.
 Require Import UniMath.MoreFoundations.PartA.
 Require Import UniMath.CategoryTheory.Core.Prelude.
-Require Import UniMath.CategoryTheory.limits.pullbacks.
+Require Import UniMath.CategoryTheory.Limits.Pullbacks.
 Require Import UniMath.CategoryTheory.Adjunctions.Core.
 Require Import UniMath.CategoryTheory.Equivalences.Core.
 Require Import UniMath.CategoryTheory.opp_precat.
@@ -22,8 +22,8 @@ Require Import UniMath.CategoryTheory.DisplayedCats.Isos.
 Require Import UniMath.CategoryTheory.DisplayedCats.Univalence.
 Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.
 
-Require Import UniMath.CategoryTheory.limits.graphs.colimits.
-Require Import UniMath.CategoryTheory.limits.graphs.coequalizers.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Coequalizers.
 
 Local Open Scope cat.
 Local Open Scope type_scope.
@@ -291,7 +291,7 @@ Defined.
 
 Definition cocartesian_lifts_z_iso_commutes {C : category} {D : disp_cat C}
     {c'} {d' : D c'} {c : C} {f : c' --> c} (fd fd' : cocartesian_lift d' f)
-  : fd ;; (cocartesian_lifts_z_iso fd fd') 
+  : fd ;; (cocartesian_lifts_z_iso fd fd')
   = transportb _ (id_right _) (fd' : _ -->[_] _).
 Proof.
   cbn. apply cocartesian_factorisation_commutes'.
diff --git a/Modules/Prelims/PushoutsFromCoeqBinCoproducts.v b/Modules/Prelims/PushoutsFromCoeqBinCoproducts.v
index bf72392..4b3ab03 100644
--- a/Modules/Prelims/PushoutsFromCoeqBinCoproducts.v
+++ b/Modules/Prelims/PushoutsFromCoeqBinCoproducts.v
@@ -21,21 +21,21 @@ Require Import UniMath.Foundations.Propositions.
 Require Import UniMath.Foundations.Sets.
 
 Require Import UniMath.CategoryTheory.Core.Prelude.
-Require Import UniMath.CategoryTheory.limits.pushouts.
-Require Import UniMath.CategoryTheory.limits.initial.
+Require Import UniMath.CategoryTheory.Limits.Pushouts.
+Require Import UniMath.CategoryTheory.Limits.Initial.
 
 
 Require Import UniMath.CategoryTheory.DisplayedCats.Core.
-Require Import UniMath.CategoryTheory.limits.graphs.colimits.
-Require Import UniMath.CategoryTheory.limits.graphs.limits.
-Require Import UniMath.CategoryTheory.limits.graphs.equalizers.
-Require Import UniMath.CategoryTheory.limits.graphs.coequalizers.
-Require Import UniMath.CategoryTheory.limits.bincoproducts.
-Require Import UniMath.CategoryTheory.limits.pushouts.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Limits.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Equalizers.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Coequalizers.
+Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
+Require Import UniMath.CategoryTheory.Limits.Pushouts.
 
 Local Open Scope cat.
 Section d.
-  Context {C : category} {g : graph} 
+  Context {C : category} {g : graph}
           (bc : BinCoproducts C)
           (coeq : Coequalizers C).
 
diff --git a/Modules/Prelims/SetCatComplements.v b/Modules/Prelims/SetCatComplements.v
index 0070db0..6b96e6f 100644
--- a/Modules/Prelims/SetCatComplements.v
+++ b/Modules/Prelims/SetCatComplements.v
@@ -25,15 +25,15 @@ Require Import Modules.Prelims.lib.
 Require Import Modules.Prelims.BinProductComplements.
 Require Import Modules.Prelims.CoproductsComplements.
 Require Import UniMath.SubstitutionSystems.ModulesFromSignatures.
-Require Import UniMath.CategoryTheory.limits.binproducts.
-Require Import UniMath.CategoryTheory.limits.bincoproducts.
-Require Import UniMath.CategoryTheory.limits.terminal.
+Require Import UniMath.CategoryTheory.Limits.BinProducts.
+Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
 Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
 Require Import UniMath.CategoryTheory.whiskering.
 Require Import UniMath.CategoryTheory.Epis.
 Require Import UniMath.CategoryTheory.EpiFacts.
 
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 
 Lemma hset_category_isDistributive (I : hSet)  :
    bp_coprod_isDistributive BinProductsHSET (CoproductsHSET  I (setproperty I)).
@@ -48,7 +48,7 @@ Defined.
 
 Lemma isEpiBinProdHSET {X X' Y Y' : hSet} (f : X -> Y)(g : X' -> Y') :
   isEpi (C := SET) f -> isEpi (C:=SET) g -> isEpi (C:=SET)
-                                                (BinProductOfArrows _ 
+                                                (BinProductOfArrows _
                                                                     (BinProductsHSET Y Y')
                                                                     (BinProductsHSET X X')
                                                             f g).
diff --git a/Modules/Prelims/deriveadj.v b/Modules/Prelims/deriveadj.v
index 02ddfea..73f0097 100644
--- a/Modules/Prelims/deriveadj.v
+++ b/Modules/Prelims/deriveadj.v
@@ -26,13 +26,13 @@ Require Import Modules.Prelims.LModulesComplements.
 Require Import Modules.Prelims.LModulesBinProducts.
 Require Import Modules.Prelims.DerivationIsFunctorial.
 Require Import UniMath.SubstitutionSystems.ModulesFromSignatures.
-Require Import UniMath.CategoryTheory.limits.binproducts.
-Require Import UniMath.CategoryTheory.limits.bincoproducts.
-Require Import UniMath.CategoryTheory.limits.terminal.
+Require Import UniMath.CategoryTheory.Limits.BinProducts.
+Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
 Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
 Require Import UniMath.CategoryTheory.whiskering.
 Require Import UniMath.CategoryTheory.UnitorsAndAssociatorsForEndofunctors.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 
 
 (* Question pour Benedikt : est ce bien utile ce abstract (exact HH) *)
@@ -59,7 +59,7 @@ This is defined as M' x R -> MR -> M
   Local Notation bpS := BinProductsHSET.
   Local Notation bcpS := BinCoproductsHSET.
   Local Notation T := TerminalHSET.
-  Local Notation hsS := has_homsets_HSET. 
+  Local Notation hsS := has_homsets_HSET.
 Section substitution.
   Context {R : Monad SET}.
   Local Infix "+" := setcoprod : set_scope.
@@ -71,7 +71,7 @@ Section substitution.
   Local Notation TFunc := (option_functor bcpS T).
 
   Definition pre_subst_nt_data (M : functor SET SET) (X : hSet)
-             (* already known (isasetcoprod) but needed 
+             (* already known (isasetcoprod) but needed
   otherwise pre_subst_is_nat_trans does not typecheck*)
              {h : isaset (coprod unit X)}
                                                           :
@@ -104,7 +104,7 @@ pre_sub_X|                            | pre_subst_Y
 but this is the same as the following diagram, when seeing t as a morphism 1 -> RX
 <<<
                 M(1+f)
-       M(1+X)  -------------->    M (1+Y) 
+       M(1+X)  -------------->    M (1+Y)
          |                            |
          |                            |
  M[η,t]  |                            | M[η,Rf∘t]
@@ -128,7 +128,7 @@ and now we show the same diagram without the application of M
     cbn -[isasetcoprod]; unfold pre_subst_nt_data ; cbn -[isasetcoprod].
     etrans;rewrite comp_cat_comp.
     apply idpath.
-    
+
     revert x.
     use toforallpaths.
     do 2 rewrite <- (functor_comp M).
@@ -176,13 +176,13 @@ and now we show the same diagram without the application of M
 t : 1 --> RRX
 top right is right hand side
 <<<
-       x         M[t,η]    
+       x         M[t,η]
     M(1+RX) -----------------------------> MRR X
         |                                     |
         |                                     |
         |                                     | σ_RX
         |                                     |
-M[ηi1,Ri2]|                                   M RX 
+M[ηi1,Ri2]|                                   M RX
         |                                     |
         |                                     | σ
         V                                     V
@@ -193,7 +193,7 @@ M[ηi1,Ri2]|                                   M RX
 by naturality of σ_R, we can rewrite the bottom arrow:
 <<<
 MR(1+X) --------> M(1+X) ----> MRX
-          σ_1+X        M[μ∘t,η]  
+          σ_1+X        M[μ∘t,η]
 >>>
 
 as
@@ -226,8 +226,8 @@ and then we eliminate the application of M
     intros x.
     induction x as [p|x]; cbn -[isasetcoprod].
     -  pose (t' := (fun _ => t) : SET ⟦unitset , R (R X)⟧).
-      (* 
-       i1       
+      (*
+       i1
     1 ---> 1 + X
     |         |
  η  |         | η
@@ -238,11 +238,11 @@ and then we eliminate the application of M
 donc ça donne
 1 ---> R 1 ---------> R R R X ------->  R R X --> R X
   η         R t                 R μ          μ
-et encoer par naturalité de η,                 
+et encoer par naturalité de η,
 1 ---> R R X ---------> R R R X ------->  R R X --> R X
   t          η t                 R μ             μ
 et on utilise les 2 lois de monades
-         
+
 *)
       etrans; revgoals.
       {
@@ -345,7 +345,7 @@ et on utilise les 2 lois de monades
     revert x.
     apply toforallpaths.
     apply pathsinv0.
-    apply (nat_trans_ax m). 
+    apply (nat_trans_ax m).
   Qed.
 
   Definition substitution_nat_trans : nat_trans (∂ ∙ ×ℜ) (functor_identity _)
@@ -365,7 +365,7 @@ Section DerivCounit.
 
   Local Notation hsC := (homset_property C).
 
-    
+
   (* functors that are in stake *)
   Local Notation LMOD_bp := (LModule_BinProducts R bpC).
   Local Notation "∂" := (LModule_deriv_functor (TerminalObject T) bcpC R).
@@ -441,13 +441,13 @@ Top right is right hand side.
   T --------------> R(T+X)
   |                  |
 in|     composition  |  id
-  |                  |   
+  |                  |
   V                  V
   T+RX ----------> R(T+X)
   |    [f,Rin₂]      ^
-  |                  |   
+  |                  |
 η |     nat of η     |   μ
-  |   & monad law    |   
+  |   & monad law    |
   V                  |
 R(T+RX) -------> RR(T+X)
         R[f,Rin₂]
@@ -458,7 +458,7 @@ R(T+RX) -------> RR(T+X)
     {
       apply cancel_precomposition.
       etrans;[apply assoc|].
-      (* η natural & monad law *) 
+      (* η natural & monad law *)
       etrans.
       - (* η natural *)
         apply cancel_postcomposition.
@@ -652,7 +652,7 @@ Section derivadj.
   Defined.
 
 
-  
+
 End derivadj.
 Section Functoriality.
   Local Notation LMOD_bp := (LModule_BinProducts _ bpS hsS).
@@ -782,7 +782,7 @@ Local Lemma adj_law2 :
    (u : LModule_Mor R M (pb_LModule f A))
    (v : LModule_Mor S A (Derivative.LModule_deriv TerminalHSET BinCoproductsHSET B)),
    (adj1 R M (pb_LModule f B))
-     ((u : (λ R0 : Monad SET, precategory_LModule R0 SET) R ⟦ M, pb_LModule f A ⟧) · 
+     ((u : (λ R0 : Monad SET, precategory_LModule R0 SET) R ⟦ M, pb_LModule f A ⟧) ·
       pb_LModule_Mor f v · (λ (R0 S0 : Monad SET) (f0 : Monad_Mor R0 S0),
                             (* LModPbCommute.pb_deriv_to_deriv_pb_iso *)
                             pb_LModule_deriv_iso
@@ -799,7 +799,7 @@ Local Lemma adj_law2 :
       (λ R0 : Monad SET, precategory_LModule R0 SET) R ⟦ tautological_LModule R,
       pb_LModule f (tautological_LModule S) ⟧) · (λ (R0 S0 : Monad SET) (f0 : Monad_Mor R0 S0),
                                                   binprod_pbm_to_pbm_iso f0) R S f A
-                                                   (tautological_LModule S) · 
+                                                   (tautological_LModule S) ·
    pb_LModule_Mor f ((adj1 S A B) v)).
 Proof.
   intros.
diff --git a/Modules/Prelims/lib.v b/Modules/Prelims/lib.v
index 9aa4609..2ed2aca 100644
--- a/Modules/Prelims/lib.v
+++ b/Modules/Prelims/lib.v
@@ -20,11 +20,11 @@ Require Import UniMath.CategoryTheory.Epis.
 
 Require Import UniMath.CategoryTheory.HorizontalComposition.
 
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 Require Import UniMath.CategoryTheory.Epis.
 Require Import UniMath.CategoryTheory.EpiFacts.
-Require Import UniMath.CategoryTheory.limits.binproducts.
-Require Import UniMath.CategoryTheory.limits.initial.
+Require Import UniMath.CategoryTheory.Limits.BinProducts.
+Require Import UniMath.CategoryTheory.Limits.Initial.
 Require Import UniMath.CategoryTheory.catiso.
 
 Require Import UniMath.CategoryTheory.Adjunctions.Core.
@@ -103,8 +103,8 @@ Proof.
     apply id_right.
 Defined.
 
- 
-                 
+
+
 (** common generalization to [maponpaths] and [toforallpaths] *)
 
 Lemma changef_path   {T1 T2 : UU} (f g : T1 → T2) (t1 t2 : T1) :
@@ -122,9 +122,9 @@ Qed.
 
 
 (** Associativity of horizontal composition of natural transformations *)
-Lemma horcomp_assoc 
+Lemma horcomp_assoc
   : ∏ {B C D E : category} {H H' : functor B C}
-      {F F' : functor C D} {G G' : functor D E} 
+      {F F' : functor C D} {G G' : functor D E}
       (a : nat_trans H H') (b : nat_trans F F') (c : nat_trans G G') x,
     ((c ∙∙ b) ∙∙ a) x = (c ∙∙( b ∙∙ a)) x.
 Proof.
@@ -156,8 +156,8 @@ Qed.
 (*
 Lemma isEpi_pre_whisker (B C :precategory)(D : category)
       (G H : functor C D) (K : functor B C) (f : nat_trans G H)
-  : (∏ x, isEpi (f x)) 
-    -> 
+  : (∏ x, isEpi (f x))
+    ->
     isEpi (C:=functor_category B D )
           (x:= (G □ K)) (y:= (H □ K))
           (pre_whisker K f).
@@ -182,7 +182,7 @@ Lemma isEpi_post_whisker_pw (B :precategory)(C D : category)
   (KpreservesEpis : forall a b (g : (C ⟦ a, b⟧)%Cat), isEpi g -> isEpi ((#K g)%cat)) :
     (forall x, isEpi (C:=  _ ) (f x))
     -> ∏ b,
-    isEpi 
+    isEpi
             (post_whisker f K b).
 Proof.
   intros epif b.
@@ -209,7 +209,7 @@ Lemma isEpi_post_whisker_HSET (choice : AxiomOfChoice.AxiomOfChoice_surj)
       (B :precategory) (C:=hset_category) ( D : category)
       (G H : functor B C) (K : functor C D) (f : nat_trans G H) :
     (forall b, isEpi  (f b))
-    -> 
+    ->
     isEpi (C:=functor_category B D)
             (x:= (K □ G)) (y:= (K □ H))
             (post_whisker f K).
@@ -235,7 +235,7 @@ Proof.
   apply homset_property.
   intros;
     apply idpath.
-Qed.    
+Qed.
 *)
 
 
@@ -321,6 +321,6 @@ Lemma lock A x : x = locked x :> A.
 Proof.
   unfold locked.
   now destruct master_key.
-Qed.    
+Qed.
 
 *)
diff --git a/Modules/Prelims/quotientmonad.v b/Modules/Prelims/quotientmonad.v
index 7896912..7bdf685 100644
--- a/Modules/Prelims/quotientmonad.v
+++ b/Modules/Prelims/quotientmonad.v
@@ -15,7 +15,7 @@ Require Import UniMath.CategoryTheory.SetValuedFunctors.
 Require Import UniMath.CategoryTheory.HorizontalComposition.
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.FunctorCategory.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 
 Require Import UniMath.Foundations.Sets.
 Require Import UniMath.CategoryTheory.Epis.
@@ -29,7 +29,7 @@ Local Notation "'SET'" := hset_category.
 Local Notation "F ;;; G" := (nat_trans_comp _ _ _ F G) (at level 35).
 
 Open Scope cat.
-    
+
 Set Automatic Introduction.
 
 (* TODO: move in lib.v *)
@@ -40,7 +40,7 @@ Section QuotientMonad.
 
 
 (** We start by just considering the quotient of the monad [R] as a functor.  Further
-    compatibility for the monad composition are assumed later. *) 
+    compatibility for the monad composition are assumed later. *)
   Context {R : Monad SET}.
 
 (**
@@ -52,13 +52,13 @@ Section QuotientMonad.
  *)
 Context (R_epi : preserves_Epi R).
 
-  Context 
+  Context
           {eqrel_equivc : ∏ c, eqrel (R c : hSet)}
         (congr_equivc : ∏ (x y : SET) (f : SET⟦x,y⟧),
                         iscomprelrelfun (eqrel_equivc x) (eqrel_equivc y) (# R f)).
 
 Let equivc {c:hSet} x y := eqrel_equivc c x y.
- 
+
 (** We define the quotient functor of R by these equivalence relations
 
 The following comment may be outdated
@@ -145,13 +145,13 @@ Definition R'_η : (functor_identity SET) ⟹ R' := η R ;;; projR .
     equivalence relation.  Note that, no condition are needed for the the compatibility
     of the unit of the monad.  *)
 
-Definition compat_μ_projR_def 
+Definition compat_μ_projR_def
   := ∏ (X : SET) (x y : pr1 ((pr1 (R ∙ R)) X)),
      (projR ∙∙ projR) X x = (projR ∙∙ projR) X y →
      (μ R;;; projR) X x = (μ R;;; projR) X y.
 
 Variable compat_μ_projR : compat_μ_projR_def.
-  
+
 Definition R'_μ  : R' ∙  R' ⟹ R'.
 Proof.
   apply (univ_surj_nt (A:= R ∙ R) (B:= R'∙ R')
@@ -171,7 +171,7 @@ Qed.
 
 Definition R'_Monad_data : disp_Monad_data R' := (R'_μ ,, R'_η).
 
- 
+
 
 Lemma R'_Monad_law_η1 : ∏ c : SET, R'_η (R' c) · R'_μ c = identity (R' c).
 Proof.
@@ -180,12 +180,12 @@ Proof.
   apply isEpi_projR.
   repeat rewrite assoc.
   etrans.
-  { apply cancel_postcomposition. 
+  { apply cancel_postcomposition.
     unfold R'_η.
     etrans;[apply assoc|].
     apply cancel_postcomposition.
     apply (nat_trans_ax (η  R)).
-  }  
+  }
   rewrite <- assoc.
   rewrite <- assoc.
   etrans.
@@ -204,7 +204,7 @@ Lemma R'_Monad_law_η2 : ∏ c : SET, # R' (R'_η c) · R'_μ c = identity (R' c
 Proof.
   intro c.
   etrans.
-  { apply cancel_postcomposition.    
+  { apply cancel_postcomposition.
     apply functor_comp. }
   use (is_pointwise_epi_from_set_nat_trans_epi _ _ _ projR isEpi_projR).
   repeat rewrite assoc.
@@ -225,9 +225,9 @@ Proof.
   rewrite id_left. apply idpath.
 Qed.
 
-Lemma assoc_ppprojR c 
+Lemma assoc_ppprojR c
   : (projR ∙∙ projR) ( R c) · # (R' ∙ R') (projR c)
-    = 
+    =
     (projR ∙∙ (projR ∙∙ projR)) c.
 Proof.
   apply (horcomp_assoc projR projR projR c).
@@ -237,15 +237,15 @@ Lemma isEpi_projR_projR_projR_pw c : isEpi ((projR ∙∙ (projR ∙∙ projR))
 Proof.
   apply isEpi_horcomp_pw2.
   - apply isEpi_projR_pw.
-  - apply isEpi_R_projR_projR_pw. 
+  - apply isEpi_R_projR_projR_pw.
 Defined.
 
 Lemma R'_Monad_law_μ : ∏ c : SET,
                              # R' (R'_μ  c) · R'_μ c = R'_μ (R' c) · R'_μ c.
 Proof.
   intro c.
- 
-      (* Note : 
+
+      (* Note :
 
 If I write instead :
   assert (epi :isEpi (horcomp projR (horcomp projR projR)  c)).
@@ -255,7 +255,7 @@ then 'apply epi' takes a huge amount of time for Coq !!
 This is due to the fact that Coq takes a long time to show that
    ((R' □ R') □ R') c = R' ((R' □ R') c)
 because it has a very bad computing strategy. He tries to evaluates R'
-which is bad idea. Probably because somewhere there is a Defined instead of 
+which is bad idea. Probably because somewhere there is a Defined instead of
 Qed for some proof, and I suspect somewhere in the section about
 quotients in basics/Sets.v
 
@@ -269,20 +269,20 @@ Legend of the diagram :
 - μ = μ R
 - ν = R'_μ
 - i = projR
-*)      
+*)
 
   etrans.
   (* First equality *)
   { etrans.
     apply (assoc (C:=SET)).
-    rewrite horcomp_pre_post.    
+    rewrite horcomp_pre_post.
     etrans.
-    { 
-      apply cancel_postcomposition.       
+    {
+      apply cancel_postcomposition.
       etrans. use (! assoc _ _ _ ).
       apply (cancel_precomposition SET).
       etrans; [ apply (!functor_comp R' _ _ ) | ].
-      apply maponpaths.      
+      apply maponpaths.
       apply R'_μ_def.
     }
     rewrite functor_comp,assoc.
@@ -290,29 +290,29 @@ Legend of the diagram :
     symmetry.
     apply cancel_postcomposition.
     apply (nat_trans_ax (projR)).
-  }  
+  }
   (* second equality *)
   etrans.
-  { 
+  {
     rewrite <- assoc.
     rewrite <- assoc.
-    apply (cancel_precomposition (SET)).     
+    apply (cancel_precomposition (SET)).
     apply (R'_μ_def c).
   }
   (* third equality *)
   etrans.
   { rewrite assoc.
     etrans. { apply cancel_postcomposition, (Monad_law3 (T:=R) c). }
-    
+
     (* Fourth equality *)
     rewrite <- assoc.
-  
+
     etrans.
     { apply cancel_precomposition. symmetry. apply R'_μ_def. }
-  
-    rewrite assoc.      
+
+    rewrite assoc.
     apply cancel_postcomposition.
-  
+
     (* Fifth equality *)
     etrans.
     { cbn -[projR compose].
@@ -322,19 +322,19 @@ Legend of the diagram :
       symmetry.
       apply R'_μ_def.
     }
-  
+
   (* Close to the end *)
     etrans.
     { rewrite <- assoc.
       apply (cancel_precomposition SET).
       symmetry.
-      apply (nat_trans_ax (R'_μ) ( R c)). 
+      apply (nat_trans_ax (R'_μ) ( R c)).
     }
     rewrite assoc.
     reflexivity.
   }
   etrans; [apply (!assoc _ _ _ ) |].
-  apply cancel_postcomposition.  
+  apply cancel_postcomposition.
   (* association of horcomposition *)
   apply assoc_ppprojR.
 Qed.
@@ -369,7 +369,7 @@ Definition projR_monad : Monad_Mor (R) (R'_monad) :=
   (_ ,, projR_monad_laws).
 
 Lemma isEpi_projR_monad : isEpi (C:=category_Monad _) projR_monad.
-Proof.    
+Proof.
   apply (faithful_reflects_epis (forgetfunctor_Monad _));
   [ apply forgetMonad_faithful|apply isEpi_projR].
 Qed.
@@ -384,9 +384,9 @@ Qed.
 
   (* FIN DE LA SECONDE ETAPE *)
 
-Variables (S : Monad SET) 
+Variables (S : Monad SET)
           (m : Monad_Mor R S)
-          (compatm : ∏ (X:SET) (x y : (R X : hSet)), 
+          (compatm : ∏ (X:SET) (x y : (R X : hSet)),
                      projR X x = projR X y → m X x = m X y).
 
 Local Definition u : nat_trans R' S.
@@ -402,13 +402,13 @@ Proof.
 Qed.
 
 (** not used here but nevermind *)
-Lemma u_def_nt :  (m : nat_trans _ _) = (compose (C := [SET,SET]) (projR : nat_trans _ _)  u)  . 
+Lemma u_def_nt :  (m : nat_trans _ _) = (compose (C := [SET,SET]) (projR : nat_trans _ _)  u)  .
 Proof.
   symmetry.
   apply univ_surj_nt_ax.
 Qed.
 
-Lemma u_monad_mor_law1 
+Lemma u_monad_mor_law1
   : ∏ a : SET, (μ R'_monad) a · u a = u (R'_monad a) · # S (u a) · (μ S) a.
 Proof.
   intro X.
@@ -418,27 +418,27 @@ Proof.
     apply isEpi_projR_projR.
   }
   apply epi.
-    
+
   (* Now the real work begins *)
   etrans.
   {  apply cancel_postcomposition.
     apply (nat_trans_ax (projR)).
   }
   etrans. (* use the monadicity of μ *)
-  { rewrite assoc.        
+  { rewrite assoc.
     apply cancel_postcomposition.
     symmetry.
     apply (Monad_Mor_μ (projR_monad)).
   }
-    
+
   (* definition of u *)
   etrans. { rewrite <- assoc. cpre _. symmetry. apply u_def. }
-    
+
   (* m is a morphism of monad *)
   etrans; [ apply (Monad_Mor_μ m) |].
-    
+
   (* Definition of u *)
-  etrans.  
+  etrans.
   { cpost _.
     etrans.
     { etrans. { cpost _.  apply u_def. }
@@ -446,8 +446,8 @@ Proof.
       etrans.
       { apply maponpaths. apply u_def. }
       apply functor_comp.
-    }    
-    (* il s'agit de rememmtre les termes dans l'ordre *)    
+    }
+    (* il s'agit de rememmtre les termes dans l'ordre *)
     rewrite assoc.
     cpost _.
     rewrite <- assoc.
@@ -492,7 +492,7 @@ Qed.
     uniqueness of the natural transformation for the underlying quotient functor. *)
 
 End QuotientMonad.
-  
+
 Arguments projR : simpl never.
 Arguments R' : simpl never.
 Arguments u_monad  [R] _ [ _ _]  _ [_] _ .
diff --git a/Modules/Prelims/quotientmonadslice.v b/Modules/Prelims/quotientmonadslice.v
index bbd96ef..2d9a273 100644
--- a/Modules/Prelims/quotientmonadslice.v
+++ b/Modules/Prelims/quotientmonadslice.v
@@ -4,21 +4,21 @@
 
 (* ----------------------------------------------------------------------------------- *)
 (** Description: This module construct the quotient of a monad (on Set) with respect to
-    some elements of its coslice category 
+    some elements of its coslice category
     More precisely: let (f_j : R --> d_j) for j in a (possibly large) set J be a collection of
     morphisms of monads. We quotient R(X) by the following relation: x ~ y
-    if and only if for all j, f_j(x) = f_j(y) 
+    if and only if for all j, f_j(x) = f_j(y)
 
     Pairs of related elements can be characterized as the (possibly large) limit L of the
-    following diagram in the category of endofunctors: 
+    following diagram in the category of endofunctors:
 <<<
   R ----> d_j
    \      ^
     \     |
      \    /
       \  /
-        / .. 
-       / 
+        / ..
+       /
       /  \
      /    \
     /     |
@@ -39,7 +39,7 @@ Require Import UniMath.CategoryTheory.HorizontalComposition.
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.FunctorCategory.
 
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 
 Require Import UniMath.Foundations.Sets.
 Require Import UniMath.CategoryTheory.Epis.
@@ -54,7 +54,7 @@ Local Notation "'SET'" := hset_category.
 Local Notation "F ;;; G" := (nat_trans_comp _ _ _ F G) (at level 35).
 
 Open Scope cat.
-    
+
 
 Section QuotientMonad.
 
@@ -138,8 +138,8 @@ Qed.
 
 Let R' := R'  congr_equivc.
 Let projR := projR  congr_equivc.
-(** Two elements that are equal in the quotient 
-    get mapped to equal elements by any morphism 
+(** Two elements that are equal in the quotient
+    get mapped to equal elements by any morphism
     of actions
 *)
 Lemma compat_slice (j : J) ( m := ff j)
@@ -164,13 +164,13 @@ Proof.
   apply (quotientmonad.u_def).
 Qed.
 
-Lemma u_def_nt (j : J) :  (ff j : nat_trans _ _) = (compose (C := [SET,SET]) (projR : nat_trans _ _)  (u j))  . 
+Lemma u_def_nt (j : J) :  (ff j : nat_trans _ _) = (compose (C := [SET,SET]) (projR : nat_trans _ _)  (u j))  .
 Proof.
   apply quotientmonad.u_def_nt.
 Qed.
 
 (** We show that the relation induced by a morphism of models
-    satisfies the conditions necessary to induce a quotient monad 
+    satisfies the conditions necessary to induce a quotient monad
 *)
 Corollary compat_μ_slice : compat_μ_projR_def congr_equivc.
 Proof.
@@ -210,7 +210,7 @@ Proof.
     do 3 apply maponpaths.
     exact (!hxy).
 Qed.
-  
+
 (** Short notations for the quotient monad and the projection as a monad morphism *)
 Definition R'_monad : Monad SET := R'_monad R_epi congr_equivc compat_μ_slice.
 Definition projR_monad
@@ -229,6 +229,6 @@ Proof.
 Qed.
 
 End QuotientMonad.
-  
+
 Arguments projR : simpl never.
 Arguments R' : simpl never.
diff --git a/Modules/Signatures/BindingSig.v b/Modules/Signatures/BindingSig.v
index d2ab360..1378d1a 100644
--- a/Modules/Signatures/BindingSig.v
+++ b/Modules/Signatures/BindingSig.v
@@ -21,13 +21,13 @@ sigs
 Require Import UniMath.Foundations.PartD.
 Require Import UniMath.Foundations.Propositions.
 Require Import UniMath.Foundations.Sets.
-Require Import UniMath.CategoryTheory.limits.bincoproducts.
+Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
 (* Require Import UniMath.SubstitutionSystems.FromBindingSigsToMonads_Summary. *)
 Require Import UniMath.SubstitutionSystems.BindingSigToMonad.
 Require Import UniMath.SubstitutionSystems.Signatures.
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.FunctorCategory.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 
 Require Import UniMath.CategoryTheory.Epis.
 Require Import UniMath.CategoryTheory.EpiFacts.
@@ -36,16 +36,16 @@ Require Import UniMath.Combinatorics.Lists.
 Require Import UniMath.CategoryTheory.whiskering.
 Require Import Modules.Prelims.lib.
 Require Import Modules.Prelims.CoproductsComplements.
-Require Import UniMath.CategoryTheory.limits.initial.
+Require Import UniMath.CategoryTheory.Limits.Initial.
 Require Import UniMath.CategoryTheory.DisplayedCats.Fiber.
 Require Import Modules.Signatures.SigWithStrengthToSignature.
 Require Import Modules.Signatures.Signature.
 Require Import Modules.Signatures.HssInitialModel.
 Require Import UniMath.SubstitutionSystems.ModulesFromSignatures.
 Require Import UniMath.CategoryTheory.Monads.Monads.
-Require Import UniMath.CategoryTheory.limits.binproducts.
-Require Import UniMath.CategoryTheory.limits.coproducts.
-Require Import UniMath.CategoryTheory.limits.terminal.
+Require Import UniMath.CategoryTheory.Limits.BinProducts.
+Require Import UniMath.CategoryTheory.Limits.Coproducts.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
 Require Import UniMath.CategoryTheory.Chains.Chains.
 Require Import UniMath.CategoryTheory.Chains.Adamek.
 Require Import UniMath.CategoryTheory.Chains.OmegaCocontFunctors.
@@ -69,9 +69,9 @@ Definition arity_to_one_sig {C : category} bpC bcpC  TC S : signature C :=
 (** specific definition for the hSet category *)
 Definition binding_to_one_sigHSET S :=
   (sigWithStrength_to_sig (C := SET)
-     (BindingSigToSignatureHSET S)). 
+     (BindingSigToSignatureHSET S)).
 
-Definition Arity_to_SignatureHSET := 
+Definition Arity_to_SignatureHSET :=
   Arity_to_Signature BinProductsHSET BinCoproductsHSET TerminalHSET.
 
 Definition arity_to_one_sigHSET S :=
@@ -90,7 +90,7 @@ Section EpiSignatureSig.
   Definition alg_initialR (sig : BindingSig) : (rep_disp SET) [{binding_to_one_sigHSET sig}] :=
     hss_initial_model (Cset sig).
 
-       
+
 
   Theorem algebraic_sig_effective (sig : BindingSig)
     : isInitial _ (alg_initialR sig).
@@ -132,17 +132,17 @@ Section EpiSignatureSig.
                                                      HSET
                                                      BinProductsHSET).
 
-  Local Notation binProdFunc := 
-      (binproducts.BinProduct_of_functors [HSET, HSET, hom_SET] [HSET, HSET, hom_SET]
-       (binproducts.BinProducts_functor_precat HSET HSET BinProductsHSET hom_SET)).
+  Local Notation binProdFunc :=
+      (BinProducts.BinProduct_of_functors [HSET, HSET, hom_SET] [HSET, HSET, hom_SET]
+       (BinProducts.BinProducts_functor_precat HSET HSET BinProductsHSET hom_SET)).
 
   Local Notation sumFuncs I Ihset :=
-    (coproducts.coproduct_of_functors I [HSET, HSET, hom_SET] [HSET, HSET, hom_SET]
-       (coproducts.Coproducts_functor_precat I HSET HSET (CoproductsHSET I Ihset) hom_SET)
+    (Coproducts.coproduct_of_functors I [HSET, HSET, hom_SET] [HSET, HSET, hom_SET]
+       (Coproducts.Coproducts_functor_precat I HSET HSET (CoproductsHSET I Ihset) hom_SET)
        ).
 
 
-  
+
   Lemma isEpi_binProdSig S S' : isEpiSig S -> isEpiSig S' -> isEpiSig (binProdSig S S').
   Proof.
     use preserveEpi_binProdFunc.
diff --git a/Modules/Signatures/EpiArePointwise.v b/Modules/Signatures/EpiArePointwise.v
index 6816f3b..4be4305 100644
--- a/Modules/Signatures/EpiArePointwise.v
+++ b/Modules/Signatures/EpiArePointwise.v
@@ -13,15 +13,15 @@ Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.FunctorCategory.
 Require Import UniMath.CategoryTheory.Epis.
 Require Import UniMath.CategoryTheory.EpiFacts.
-Require Import UniMath.CategoryTheory.limits.graphs.pushouts.
-Require Import UniMath.CategoryTheory.limits.graphs.eqdiag.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Pushouts.
+Require Import UniMath.CategoryTheory.Limits.Graphs.EqDiag.
 
-Require Import UniMath.CategoryTheory.limits.graphs.limits.
-Require Import UniMath.CategoryTheory.limits.graphs.colimits.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Limits.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
 Require Import UniMath.CategoryTheory.Monads.Monads.
-Require Import UniMath.CategoryTheory.Monads.LModules. 
+Require Import UniMath.CategoryTheory.Monads.LModules.
 
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 
 Require Import Modules.Prelims.lib.
 Require Import Modules.Prelims.LModulesColims.
@@ -33,8 +33,8 @@ Section pwEpiAr.
   Context {C : category}  .
   Local Notation MOD R := (category_LModule R C).
 
-  Context 
-          (pos : colimits.Colims_of_shape pushout_graph C)
+  Context
+          (pos : Colimits.Colims_of_shape pushout_graph C)
           {A B : signature C} (F : signature_Mor A  B).
 
   Lemma pwEpiSig_isEpi : (∏ (R : Monad C) , isEpi (C := [C,C] ) (F R:nat_trans _ _)) -> isEpi (C := SIG) F.
@@ -51,9 +51,9 @@ Section pwEpiAr.
   Context    (epiF : isEpi (C:=SIG) F).
 
 
-  Lemma PO_eqdiag (R : Monad C) X : 
+  Lemma PO_eqdiag (R : Monad C) X :
     eq_diag
-  (diagram_pointwise 
+  (diagram_pointwise
                      (mapdiagram (LModule_forget_functor R C) (mapdiagram (forget_Sig R) (pushout_diagram SIG F F))) X)
    (pushout_diagram C (F R X) (F R X) ).
   Proof.
@@ -73,7 +73,7 @@ Section pwEpiAr.
          (diagram_pointwise
             (mapdiagram (LModule_forget_functor R C)
                         (mapdiagram (forget_Sig R) (pushout_diagram signature_category F F))) X)).
-    
+
 
   Lemma epiSig_is_pwEpi (R : Monad C) : isEpi (C := [C,C] ) (F R:nat_trans _ _).
   Proof.
diff --git a/Modules/Signatures/EpiSigRepresentability.v b/Modules/Signatures/EpiSigRepresentability.v
index fcf5686..b11d6b5 100644
--- a/Modules/Signatures/EpiSigRepresentability.v
+++ b/Modules/Signatures/EpiSigRepresentability.v
@@ -4,8 +4,8 @@ In this file :
 
 - Proof that HSET has effective epis
 
-- Proof that given a category D with pushouts, if a natural transformation 
-between two functors of codomain D is an epi, then it is pointwise an epi 
+- Proof that given a category D with pushouts, if a natural transformation
+between two functors of codomain D is an epi, then it is pointwise an epi
 (Colims_pw_epi).
 
 
@@ -19,7 +19,7 @@ to the previously mentionned for surjections.
 - Proof that pointwise epimorphisms of signature preserve representability
  if the domain is an epi-signature
 
-Section leftadjoint : 
+Section leftadjoint :
 Preuve d'André à traduire.
 
 *)
@@ -34,17 +34,17 @@ Require Import UniMath.CategoryTheory.Adjunctions.Core.
 Require Import UniMath.CategoryTheory.Epis.
 Require Import UniMath.CategoryTheory.EpiFacts.
 Require Import Modules.Prelims.EpiComplements.
-Require Import UniMath.CategoryTheory.limits.initial.
+Require Import UniMath.CategoryTheory.Limits.Initial.
 
 Require Import UniMath.CategoryTheory.Monads.Monads.
-Require Import UniMath.CategoryTheory.Monads.LModules. 
+Require Import UniMath.CategoryTheory.Monads.LModules.
 
 Require Import UniMath.CategoryTheory.DisplayedCats.Core.
 Require Import UniMath.CategoryTheory.DisplayedCats.Fiber.
 Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.
 Require Import UniMath.CategoryTheory.HorizontalComposition.
 
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 Require Import UniMath.CategoryTheory.SetValuedFunctors.
 
 Require Import Modules.Signatures.Signature.
@@ -60,17 +60,17 @@ Set Automatic Introduction.
 
 
 Section all_purpose.
-  
-(** First a general-purpose lemma: 
-    equal monad morphisms are mapped to 
+
+(** First a general-purpose lemma:
+    equal monad morphisms are mapped to
     equal module morphisms by any
     signature
 *)
 Lemma cancel_ar_on {sig : signature SET}
-      {T : Monad SET} 
+      {T : Monad SET}
       {S' : Monad SET}
       (m m' : Monad_Mor T S')
-      (X : SET) 
+      (X : SET)
   : m = m' ->  (# sig)%ar m X = (# sig)%ar m' X .
 Proof.
   intro e; induction e.
@@ -100,7 +100,7 @@ Proof.
     + apply choice.
     + apply hf.
 Qed.
-   
+
 
 End all_purpose.
 
@@ -134,20 +134,20 @@ Context (ab_epi : preserves_Epi (a ( R : model _)) ⨿ (∏ S, preserves_Epi (b
 Local Notation "## F" := (pr1 (pr1 F))(at level 3).
 
 (**
-On any set X we define the following equivalence relation on R X : 
+On any set X we define the following equivalence relation on R X :
    x ~ y
 iff for any model morphism f : R -> F*(S) (where S is a b-model)
   f x = f y.
 
 
-We will show that this relation satisfies the conditions necessary to 
+We will show that this relation satisfies the conditions necessary to
 define the quotient of a monad, and of a module over a monad.
 
 *)
 
 
 (** Define two elements in R to be related if they are mapped
-    to the same element by any morphism f of models 
+    to the same element by any morphism f of models
 *)
 
 
@@ -163,7 +163,7 @@ Arguments projR : simpl never.
 
 Section Instantiating_Quotient_Constructions.
 
-(** We define short identifiers for the quotient constructions for 
+(** We define short identifiers for the quotient constructions for
     functors, monads, and modules (defined in previous files),
     for the equivalence relation induced by a morphism of models [m]
     over a morphism of arities [F].
@@ -217,7 +217,7 @@ End Instantiating_Quotient_Constructions.
 
 (** Some helper lemmas *)
 
-(** Any morphism of representations factors, 
+(** Any morphism of representations factors,
     as a monad morphism, via the monad projection *)
 Lemma Rep_mor_is_composition
       {S : REP b} (m : R -->[ F] S)
@@ -230,7 +230,7 @@ Proof.
     apply (u_def m).
 Qed.
 
-(** 
+(**
 <<
                  model_τ R
             a R  ----->  R
@@ -248,9 +248,9 @@ Qed.
 
 Lemma eq_mr
       {S : REP b} (m : R -->[ F] S) (X : SET)
-  : model_τ R X · pr1 (## m) X 
+  : model_τ R X · pr1 (## m) X
     =
-    pr1 (# a projR)%ar X · (F (R' ))%ar X 
+    pr1 (# a projR)%ar X · (F (R' ))%ar X
         ·
         pr1 (# b (u m))%ar X · model_τ S X.
 Proof.
@@ -338,7 +338,7 @@ The diagonal of the following square, which commutes by naturality of F:
 
 where π := projR
 
-The R-module morphism 
+The R-module morphism
     #a R · Pullback (π)(F R') : a(R) ---> π^*(b R')
 *)
 Definition hab :
@@ -364,14 +364,14 @@ Qed.
                τ
     a(R) -----------------> R
      |                      |
-hab  |                      | π 
+hab  |                      | π
      |                      |
      v                      v
    π^*(b R')                R'
 
 >>
 *)
-Lemma compat_model_τ_projR 
+Lemma compat_model_τ_projR
   : ∏ (X : SET) x y,
     (pr1 hab) X x
     (* =       ( pr1 (# a projR )%ar X ;; (F `` R') X) y *)
@@ -386,7 +386,7 @@ Proof.
   apply rel_eq_projR.
   intros [S m].
   assert (h := eq_mr m X); apply toforallpaths in h.
-  etrans; [ apply h |].  
+  etrans; [ apply h |].
   apply pathsinv0.
   etrans; [ apply h |].
   cbn.
@@ -425,7 +425,7 @@ Proof.
 Qed.
 
 
-Definition R'_model_τ_module 
+Definition R'_model_τ_module
   : LModule_Mor _ (b R') (tautological_LModule R') .
 Proof.
   use quotientrep.R'_model_τ_module; revgoals.
@@ -434,7 +434,7 @@ Proof.
   - apply ab_epi2.
 Defined.
 
-(** 
+(**
 <<
            a(π)
     a(R)-------> a(R')
@@ -443,17 +443,17 @@ Defined.
      |            v
    τ |           b(R')
      |            |
-     |            | τ 
+     |            | τ
      v            v
      R ---------> R'
-          π 
+          π
 >>
 *)
 
-Definition R'_model_τ_def 
+Definition R'_model_τ_def
   : ∏ (X : SET),
-    (# a (projR)%ar) X · (F R') X · R'_model_τ_module X  
-    = 
+    (# a (projR)%ar) X · (F R') X · R'_model_τ_module X
+    =
     model_τ R X · projR X .
 Proof.
   intro X.
@@ -491,7 +491,7 @@ Context {S : REP b} (m : R -->[ F] S).
 Context (cond_F : cond_isEpi_hab).
 
 Open Scope signature_scope.
-  
+
 
 (* TODO  : foutre ça dans quotientrep *)
 Lemma u_rep_laws
@@ -529,7 +529,7 @@ Proof.
 Qed.
 
 
-Definition u_rep : (rep_of_b_in_R' cond_F) -->[identity (b: CAT_SIGNATURE)] S 
+Definition u_rep : (rep_of_b_in_R' cond_F) -->[identity (b: CAT_SIGNATURE)] S
   := _ ,, u_rep_laws.
 
 
@@ -548,7 +548,7 @@ Proof.
     + apply has_homsets_HSET.
     + intro X.
       apply hu'.
-Qed.      
+Qed.
 
 
 End uModel.
@@ -578,12 +578,12 @@ Proof.
   intros u' x.
   apply pathsinv0.
   etrans ; [
-      apply (@transport_signature_mor SET a a 
+      apply (@transport_signature_mor SET a a
                                   (identity (a:CAT_SIGNATURE) · identity (a:CAT_SIGNATURE))
-                                  (identity (a:CAT_SIGNATURE)) (id_right (identity (a:CAT_SIGNATURE))) 
-                                  R 
+                                  (identity (a:CAT_SIGNATURE)) (id_right (identity (a:CAT_SIGNATURE)))
+                                  R
                                   (FF S)
-                                  _ 
+                                  _
             ) |].
   apply (cancel_precomposition HSET _ _ _ _ _ ((projR R _ x))).
   cbn.
@@ -594,7 +594,7 @@ Qed.
 Lemma u_rep_universal (R : model _)
     (Repi : preserves_Epi (R : model a))
     (epiab :  preserves_Epi (a (R : model _)) ⨿ (∏ S : Monad SET, preserves_Epi (b S)))
-    (cond_R : 
+    (cond_R :
        (isEpi (C := [_, _]) (pr1 (F (R' _ Repi) )) × sig_preservesNatEpiMonad a)
          ⨿ (isEpi (C := [_, _]) (pr1 (F (pr1 R))) × sig_preservesNatEpiMonad b))
   :
@@ -603,10 +603,10 @@ Lemma u_rep_universal (R : model _)
     (projR_rep R Repi epiab cond_R).
 Proof.
     intros S m. cbn in S, m.
-    use unique_exists. 
-    + unshelve use (u_rep _ _ _ m). 
+    use unique_exists.
+    + unshelve use (u_rep _ _ _ m).
     + (* Ici ca devrait être apply quotientmonad.u_def *)
-      apply pathsinv0. 
+      apply pathsinv0.
       apply model_mor_mor_equiv.
       intro x.
       etrans. { apply u_def. }
@@ -621,10 +621,10 @@ Proof.
 Qed.
 
 Theorem push_initiality_weaker
-        (R : Rep_a) 
+        (R : Rep_a)
         (R_epi : preserves_Epi ( R : model _))
         (epiab :  preserves_Epi (a (R : model _)) ⨿ (∏ S : Monad SET, preserves_Epi (b S)))
-        (cond_R : 
+        (cond_R :
            (isEpi (C := [_, _]) (pr1 (F (R' _ R_epi) )) × sig_preservesNatEpiMonad a)
              ⨿ (isEpi (C := [_, _]) (pr1 (F (pr1 R))) × sig_preservesNatEpiMonad b))
   : isInitial _ R -> Initial Rep_b.
@@ -637,7 +637,7 @@ Qed.
 
 Theorem push_initiality
         (** R is a model of a *)
-        (R : Rep_a) 
+        (R : Rep_a)
         (R_epi : preserves_Epi ( R : model _))
         (epiaR :  preserves_Epi (a (R : model _)))
         (** a is an epi-signature *)
@@ -682,17 +682,17 @@ Definition is_right_adjoint_functor_of_reps
 Proof.
   set (cond_F := fun R R_epi => inl ((Fepi R R_epi),, aepi) : cond_isEpi_hab R R_epi).
   use right_adjoint_left_from_partial.
-  - intro R. 
+  - intro R.
     use (rep_of_b_in_R' R _ _ (cond_F R _ )).
     + apply epiall.
-    + apply ii1. 
+    + apply ii1.
       apply epiall.
   - intro R. apply projR_rep.
   - intro R.
     apply u_rep_universal.
 Qed.
-  
-Corollary is_right_adjoint_functor_of_reps_from_pw_epi 
+
+Corollary is_right_adjoint_functor_of_reps_from_pw_epi
             (aepi : sig_preservesNatEpiMonad a)
            (epiall : ∏ (R : functor SET SET), preserves_Epi R)
           (Fepi : forall R : Monad SET, isEpi (C:=functor_precategory HSET HSET has_homsets_HSET)
@@ -705,7 +705,7 @@ Proof.
   - intros; apply Fepi.
 Qed.
 
-Corollary is_right_adjoint_functor_of_reps_from_pw_epi_choice 
+Corollary is_right_adjoint_functor_of_reps_from_pw_epi_choice
            (choice : AxiomOfChoice.AxiomOfChoice_surj)
            (aepi : sig_preservesNatEpiMonad a)
           (Fepi : forall R : Monad SET, isEpi (C:=functor_precategory HSET HSET has_homsets_HSET)
diff --git a/Modules/Signatures/HssInitialModel.v b/Modules/Signatures/HssInitialModel.v
index c284164..67da565 100644
--- a/Modules/Signatures/HssInitialModel.v
+++ b/Modules/Signatures/HssInitialModel.v
@@ -7,26 +7,26 @@ case.
 Require Import UniMath.Foundations.PartD.
 Require Import UniMath.Foundations.Propositions.
 Require Import UniMath.Foundations.Sets.
-Require Import UniMath.CategoryTheory.limits.bincoproducts.
+Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
 Require Import UniMath.SubstitutionSystems.Signatures.
 
 Require Import UniMath.CategoryTheory.Core.Prelude.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 Require Import UniMath.CategoryTheory.FunctorCategory.
 
 Require Import UniMath.Combinatorics.Lists.
 Require Import UniMath.CategoryTheory.whiskering.
 Require Import Modules.Prelims.lib.
 Require Import Modules.Prelims.CoproductsComplements.
-Require Import UniMath.CategoryTheory.limits.initial.
+Require Import UniMath.CategoryTheory.Limits.Initial.
 Require Import UniMath.CategoryTheory.DisplayedCats.Fiber.
 Require Import Modules.Signatures.SigWithStrengthToSignature.
 Require Import Modules.Signatures.Signature.
 Require Import UniMath.SubstitutionSystems.ModulesFromSignatures.
 Require Import UniMath.CategoryTheory.Monads.Monads.
-Require Import UniMath.CategoryTheory.limits.binproducts.
-Require Import UniMath.CategoryTheory.limits.coproducts.
-Require Import UniMath.CategoryTheory.limits.terminal.
+Require Import UniMath.CategoryTheory.Limits.BinProducts.
+Require Import UniMath.CategoryTheory.Limits.Coproducts.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
 Require Import UniMath.CategoryTheory.Chains.Chains.
 Require Import UniMath.CategoryTheory.Chains.Adamek.
 Require Import UniMath.CategoryTheory.Chains.OmegaCocontFunctors.
@@ -47,7 +47,7 @@ Section EpiSignatureSig.
   Local Notation Sig := (Signature SET SET HSET).
   Local Notation EndSet := [hset_category, hset_category].
   (* Local Notation toSig := SigToSignatureHSET . *)
-  
+
   Local Notation iniHSS sig hsig  := (InitialHSS SET BinCoproductsHSET InitialHSET
                                         (ColimsHSET_of_shape nat_graph)
                                         sig
@@ -79,7 +79,7 @@ Section EpiSignatureSig.
     apply j_mor_rep.
   Qed.
 
-  Definition hss_initial_arrow {sig : Sig}(hsig : is_omega_cocont sig) 
+  Definition hss_initial_arrow {sig : Sig}(hsig : is_omega_cocont sig)
     (b : model (sigWithStrength_to_sig (C := SET)( sig))) :
     (rep_disp SET) [{(sigWithStrength_to_sig sig)}] ⟦ hss_initial_model hsig, b ⟧
     := hss_initial_arrow_mon hsig b,, hss_initial_arrow_law hsig b.
@@ -116,9 +116,9 @@ Section EpiSignatureSig.
       apply ht.
   Qed.
 
-    
-    
-  
+
+
+
   Definition rep_mor_to_alg_mor {sig : Sig}
              (hsig : is_omega_cocont sig)
              (b : model (sigWithStrength_to_sig sig))
@@ -132,7 +132,7 @@ Section EpiSignatureSig.
 
 
 
-  Lemma hss_initial_arrow_unique  {sig : Sig} 
+  Lemma hss_initial_arrow_unique  {sig : Sig}
         (hsig : is_omega_cocont sig)
     (b : model (sigWithStrength_to_sig sig)) :
     ∏ t : (rep_disp SET) [{(sigWithStrength_to_sig sig)}] ⟦ hss_initial_model hsig, b ⟧,
@@ -143,16 +143,16 @@ Section EpiSignatureSig.
     (* TODO : mettre ce lemme d'unicité qui vient de la définition de j avec sa définition
  dans ModulesFromSignatures *)
     assert (h := (InitialArrowUnique
-     (colimAlgInitial 
+     (colimAlgInitial
         (Initial_functor_precat HSET HSET InitialHSET)
         (is_omega_cocont_Id_H HSET BinCoproductsHSET ( sig)
            hsig)
-        (colimits.ColimsFunctorCategory_of_shape nat_graph 
+        (Colimits.ColimsFunctorCategory_of_shape nat_graph
            HSET HSET (ColimsHSET_of_shape nat_graph)
            (initChain (Initial_functor_precat HSET HSET InitialHSET)
               (Id_H HSET BinCoproductsHSET ( sig)))))
      (ModulesFromSignatures.M_alg HSET BinCoproductsHSET ( sig) b (model_τ b)))).
-   
+
     specialize (h (rep_mor_to_alg_mor hsig b t)).
     apply model_mor_mor_equiv.
     intro c.
@@ -161,8 +161,8 @@ Section EpiSignatureSig.
     apply toforallpaths in h.
     apply h.
   Qed.
-       
-       
+
+
 
   Theorem hss_sig_effective {sig : Sig}(hsig : is_omega_cocont sig)
     : isInitial _ (hss_initial_model hsig).
diff --git a/Modules/Signatures/HssSignatureCommutation.v b/Modules/Signatures/HssSignatureCommutation.v
index c1f053b..7871bbe 100644
--- a/Modules/Signatures/HssSignatureCommutation.v
+++ b/Modules/Signatures/HssSignatureCommutation.v
@@ -20,14 +20,14 @@ Require Import UniMath.SubstitutionSystems.SignatureExamples.
 Require Import UniMath.SubstitutionSystems.BinProductOfSignatures.
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.FunctorCategory.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 
 Require Import UniMath.CategoryTheory.Epis.
-Require Import UniMath.CategoryTheory.limits.coproducts.
-Require Import UniMath.CategoryTheory.limits.bincoproducts.
-Require Import UniMath.CategoryTheory.limits.coproducts.
-Require Import UniMath.CategoryTheory.limits.binproducts.
-Require Import UniMath.CategoryTheory.limits.terminal.
+Require Import UniMath.CategoryTheory.Limits.Coproducts.
+Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
+Require Import UniMath.CategoryTheory.Limits.Coproducts.
+Require Import UniMath.CategoryTheory.Limits.BinProducts.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
 Require Import UniMath.CategoryTheory.EpiFacts.
 Require Import UniMath.Combinatorics.Lists.
 Require Import UniMath.CategoryTheory.whiskering.
@@ -46,7 +46,7 @@ Require Import Modules.Signatures.SignatureDerivation.
 Require Import Modules.Prelims.BinProductComplements.
 
 Require Import UniMath.CategoryTheory.Monads.Monads.
-Require Import UniMath.CategoryTheory.Monads.LModules. 
+Require Import UniMath.CategoryTheory.Monads.LModules.
 Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
 Open Scope cat.
 
@@ -81,7 +81,7 @@ Section GenericStrat.
   Let S1 : signature C := _ ,, isS1.
   Let S2 : signature C := _ ,, isS2.
 
-  Let S1_S2_R_iso (R : Monad C) : 
+  Let S1_S2_R_iso (R : Monad C) :
     iso (C := category_LModule R _)
         (S1 R)
         ( S2 R) :=
@@ -152,7 +152,7 @@ Section commuteBinProdSig.
   Let ar_b :=  sigWithStrength_to_sig b.
   Local Notation BPO := (BinProductObject _ ).
 
-  (**  to get this statment, I first tried to use LModule_M1_M2_iso  
+  (**  to get this statment, I first tried to use LModule_M1_M2_iso
   Lemma  binprod_sigs_har_mod_iso R :
     iso (C := category_LModule R _)
         ( sigWithStrength_to_sig (BPO (hss_bpSig a b)) R)
@@ -174,9 +174,9 @@ Section commuteBinProdSig.
     apply idpath.
   Defined.
 
-  Lemma binprod_sigs_har_eq (R S : Monad C) (f : Monad_Mor R S) (c : C) : 
+  Lemma binprod_sigs_har_eq (R S : Monad C) (f : Monad_Mor R S) (c : C) :
     (signature_BinProduct_on_morphisms ar_a ar_b R S f) c =
-    (lift_lmodule_mor (BPO (hss_bpSig a b)) R (monad_mor_to_lmodule f) c) · (lift_pb_LModule 
+    (lift_lmodule_mor (BPO (hss_bpSig a b)) R (monad_mor_to_lmodule f) c) · (lift_pb_LModule
                                                                                  (BPO (hss_bpSig a b)) f) c.
   Proof.
     cbn.
@@ -188,10 +188,10 @@ Section commuteBinProdSig.
     reflexivity.
   Qed.
 
-    
 
 
-  Definition binprod_sigs_har_iso : iso (C := signature_category) 
+
+  Definition binprod_sigs_har_iso : iso (C := signature_category)
                                         ( sigWithStrength_to_sig (BPO (hss_bpSig a b)) )
                                         ( (BPO (bpSig ar_a ar_b) : signature _ ) ).
   Proof.
@@ -223,7 +223,7 @@ Section CoprodAr.
   Proof.
     cbn.
     unfold SumOfSignatures.θ_ob_fun.
-    unfold coproducts.coproduct_nat_trans_data.
+    unfold Coproducts.coproduct_nat_trans_data.
     etrans;[apply precompWithCoproductArrow|].
     unfold LModulesCoproducts.LModule_coproduct_mult_data.
     unfold CoproductOfArrows.
diff --git a/Modules/Signatures/ModelCat.v b/Modules/Signatures/ModelCat.v
index 2b296fa..e27c51a 100644
--- a/Modules/Signatures/ModelCat.v
+++ b/Modules/Signatures/ModelCat.v
@@ -1,6 +1,6 @@
 (** * Category of models of a signature
 
-- [rep_fiber_category]: Direct definition 
+- [rep_fiber_category]: Direct definition
 - [catiso_modelcat]: proof that this category is isomorphic to the definition as a fiber category
   of the fibration of the total 1-model category over the 1-signatures category,
   as defined in Signatures/Signature.v
@@ -15,7 +15,7 @@ Require Import UniMath.Foundations.Propositions.
 Require Import UniMath.Foundations.Sets.
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.FunctorCategory.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 Require Import UniMath.CategoryTheory.Epis.
 Require Import UniMath.CategoryTheory.EpiFacts.
 Require Import UniMath.CategoryTheory.Monads.Monads.
@@ -25,8 +25,8 @@ Require Import UniMath.CategoryTheory.DisplayedCats.Core.
 Require Import UniMath.CategoryTheory.DisplayedCats.Fiber.
 Require Import UniMath.CategoryTheory.DisplayedCats.Fibrations.
 
-Require Import UniMath.CategoryTheory.limits.bincoproducts.
-Require Import UniMath.CategoryTheory.limits.initial.
+Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
+Require Import UniMath.CategoryTheory.Limits.Initial.
 Require Import UniMath.CategoryTheory.whiskering.
 
 Require Import Modules.Prelims.lib.
@@ -46,14 +46,14 @@ Local Notation SIG := (signature C).
 (** This proposition states that the monad morphism [g] between two 1-models
     commutes with the action [model_τ].
  *)
-Definition rep_fiber_mor_law {a : SIG} (M N : model a) 
+Definition rep_fiber_mor_law {a : SIG} (M N : model a)
            (g : Monad_Mor M N)
   : UU
   := ∏ c : C, model_τ M c · g c = ((#a g)%ar:nat_trans _ _) c ·  model_τ N c .
 
 (** This statment is hProp *)
 Lemma isaprop_rep_fiber_mor_law {a  : SIG} (M N : model a)
-      (g : Monad_Mor M N) 
+      (g : Monad_Mor M N)
   : isaprop (rep_fiber_mor_law  M N  g).
 Proof.
   intros.
@@ -80,14 +80,14 @@ Proof.
 Qed.
 
 (** Coercion from 1-model morphism to monad morphisms *)
-Coercion monad_morphism_from_rep_fiber_mor {a : SIG} {M N : model a} 
+Coercion monad_morphism_from_rep_fiber_mor {a : SIG} {M N : model a}
           (h : rep_fiber_mor M N) : Monad_Mor M N
   := pr1 h.
 
 (** A model morphism commutes with the action *)
-Definition rep_fiber_mor_ax {a : SIG} {M N : model a} 
+Definition rep_fiber_mor_ax {a : SIG} {M N : model a}
             (h:rep_fiber_mor  M N ) :
-  ∏ c, model_τ M c · h c = (#a h)%ar c ·  model_τ N c 
+  ∏ c, model_τ M c · h c = (#a h)%ar c ·  model_τ N c
   := pr2 h.
 
 (** If two 1-model morphisms are equal as natural transformations, then they are equal *)
@@ -96,10 +96,10 @@ Lemma rep_fiber_mor_eq_nt {a : SIG} (R S:model a)
   (u : nat_trans _ _) = v -> u = v.
 Proof.
   intros.
-  use (invmap (subtypeInjectivity _ _ _ _  )). 
+  use (invmap (subtypeInjectivity _ _ _ _  )).
   - intro g.
     apply isaprop_rep_fiber_mor_law.
-  - use (invmap (Monad_Mor_equiv _ _)).  
+  - use (invmap (Monad_Mor_equiv _ _)).
      +  assumption.
 Qed.
 
@@ -177,13 +177,13 @@ Proof.
   apply make_is_precategory_one_assoc; simpl; intros.
   - unfold identity.
     simpl.
-    apply rep_fiber_mor_eq. 
+    apply rep_fiber_mor_eq.
     intro x; simpl.
     apply id_left.
-  - apply rep_fiber_mor_eq. 
+  - apply rep_fiber_mor_eq.
     intro x; simpl.
     apply id_right.
-  - apply rep_fiber_mor_eq. 
+  - apply rep_fiber_mor_eq.
     intro x; simpl.
     apply assoc.
 Qed.
@@ -359,7 +359,7 @@ M (M + Id) ---------> M R --------> M
 
 
   (** First law of (M + Id)-module for M *)
-  Lemma mod_id_M_mod_law1  : ∏ c, 
+  Lemma mod_id_M_mod_law1  : ∏ c,
        #M (mod_id_η c) · mod_id_M_mod c = identity _.
   Proof.
     intro c.
@@ -377,7 +377,7 @@ M (M + Id) ---------> M R --------> M
     (* De l'intérêt que les nat_trans sont définis entre functor_data ! En effet, ici
    les deux foncteurs ont le même functor_data. C'est la partie hProp qui diffère *)
   Definition postcomp_nt (F : functor C C) : nat_trans (F ∙ IdM)  (bcO (BC (F ∙ M) F): functor _ _) :=
-    nat_trans_id (F ∙ IdM) . 
+    nat_trans_id (F ∙ IdM) .
 
   (** Isomorphism between F (M + Id) and F M + F *)
   Lemma isoRIdM (F : functor C C) : iso (C := [C,C]) (F ∙ IdM)  ((BC (F ∙ M) F)).
@@ -390,7 +390,7 @@ M (M + Id) ---------> M R --------> M
   (** The multiplication for the monad M + Id:
 <<
 
-                                             M [ρ,η]                   
+                                             M [ρ,η]
  (M + Id) (M + Id) ~ M (M + Id) + (M + Id)  ---------> M R + (M + Id) ---> M + (M + Id) ----> M + Id
 >>
    *)
@@ -433,7 +433,7 @@ M (M + Id) ---------> M R --------> M
   Qed.
 
   (** Second (M + Id)-module law for M *)
-  Lemma mod_id_M_mod_law2  : ∏ c, 
+  Lemma mod_id_M_mod_law2  : ∏ c,
        #M (mod_id_μ _) · mod_id_M_mod c = mod_id_M_mod _ · mod_id_M_mod _.
   Proof.
     intro c.
@@ -581,7 +581,7 @@ M (M + Id) ---------> M R --------> M
         repeat rewrite id_left.
         reflexivity.
   Qed.
-  
+
 
   (** The M + Id monad *)
   Definition mod_id_monad : Monad C := _ ,, _ ,, mod_id_monad_laws.
@@ -597,7 +597,7 @@ M (M + Id) ---------> M R --------> M
               BinCoproduct_of_functors_mor
               ; cbn).
       rewrite id_left.
-      (etrans; [ apply BinCoproductArrowEta| apply pathsinv0; apply BinCoproductArrowUnique]); revgoals. 
+      (etrans; [ apply BinCoproductArrowEta| apply pathsinv0; apply BinCoproductArrowUnique]); revgoals.
       + repeat rewrite assoc.
         do 2 rewrite BinCoproductIn2Commutes.
         etrans;[|apply pathsinv0, id_left].
@@ -679,7 +679,7 @@ Definition mod_id_model {Sig : signature C} (R : model Sig) : model Sig :=
    mod_id_model_monad R ,, mod_id_model_action R.
 
 (** The monad morphism Sig(R) + Id -> R is a model morphism *)
-Definition mod_id_model_mor_laws {Sig : signature C} (R : model Sig) : 
+Definition mod_id_model_mor_laws {Sig : signature C} (R : model Sig) :
     rep_fiber_mor_law (mod_id_model R) R (mod_id_monad_mor bc (Sig  R) (model_τ R)).
 Proof.
   intro.
@@ -688,7 +688,7 @@ Proof.
   apply BinCoproductIn1Commutes.
 Qed.
 
-Definition mod_id_model_mor {Sig : signature C} (R : model Sig) : 
+Definition mod_id_model_mor {Sig : signature C} (R : model Sig) :
   rep_fiber_mor (mod_id_model R) R  :=
   _ ,, mod_id_model_mor_laws R.
 
@@ -728,7 +728,7 @@ Proof.
               exact h.
         }
         eapply (paths_rect _ _
-                (fun a eq => 
+                (fun a eq =>
                    (# Sig)%ar (Monad_composition fR (mod_id_monad_mor bc (Sig (pr1 R)) (model_τ R))) c
                    = (# Sig)%ar a c));
           [|exact (maponpaths  pr1 h1)].
@@ -740,4 +740,4 @@ Qed.
 
 End InitAlg2.
 
-                             
+
diff --git a/Modules/Signatures/Modularity.v b/Modules/Signatures/Modularity.v
index 108591b..ecd9656 100644
--- a/Modules/Signatures/Modularity.v
+++ b/Modules/Signatures/Modularity.v
@@ -4,7 +4,7 @@
 Suppose we have the following pushout diagram in the category of signatures:
 <<<
                 f1
-       a0 ------------>  a1 
+       a0 ------------>  a1
        |                 |
        |                 |
    f2  |                 | g2
@@ -12,8 +12,8 @@ Suppose we have the following pushout diagram in the category of signatures:
        |                 |
        |                 |
        V                 V
-       a2 ------------>  a' 
-                 g1 
+       a2 ------------>  a'
+                 g1
 >>>
 
 such that a0, a1, a2 and a' are effective with initial models
@@ -21,7 +21,7 @@ R0, R1, R2 and R'. Then, above this pushout there is a pushout square in the
 large category of models:
 <<<
                 ff1
-       R0 ------------>  R1 
+       R0 ------------>  R1
        |                 |
        |                 |
   ff2  |                 | gg2
@@ -29,8 +29,8 @@ large category of models:
        |                 |
        |                 |
        V                 V
-       R2 ------------>  R' 
-                 gg1 
+       R2 ------------>  R'
+                 gg1
 >>>
 
 
@@ -43,8 +43,8 @@ Require Import UniMath.Foundations.Sets.
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.FunctorCategory.
 
-Require Import UniMath.CategoryTheory.limits.pushouts.
-Require Import UniMath.CategoryTheory.limits.initial.
+Require Import UniMath.CategoryTheory.Limits.Pushouts.
+Require Import UniMath.CategoryTheory.Limits.Initial.
 
 Require Import UniMath.CategoryTheory.DisplayedCats.Core.
 Require Import UniMath.CategoryTheory.DisplayedCats.Fiber.
@@ -70,10 +70,10 @@ Definition pushout_in_big_rep
 
            (** and syntaxes for each of the signatures *)
            {R0 : rep_disp _ a0} {R1 : rep_disp _ a1} {R2 : rep_disp _ a2} {R' : rep_disp _ a'}
-           (repr_R0 : isInitial  (fiber_category _ _) R0)  
+           (repr_R0 : isInitial  (fiber_category _ _) R0)
            (repr_R1 : isInitial  (fiber_category _ _) R1)
            (repr_R2 : isInitial  (fiber_category _ _) R2)
-           (repr_R' : isInitial  (fiber_category _ _) R') 
+           (repr_R' : isInitial  (fiber_category _ _) R')
            (** Then the initial morphisms induce a pushout in the total category *)
   :  isPushout (TT (ι f1))
                (TT (ι f2))
diff --git a/Modules/Signatures/PresentableSignature.v b/Modules/Signatures/PresentableSignature.v
index cce7ea2..0629167 100644
--- a/Modules/Signatures/PresentableSignature.v
+++ b/Modules/Signatures/PresentableSignature.v
@@ -9,7 +9,7 @@ Require Import UniMath.SubstitutionSystems.BindingSigToMonad.
 Require Import UniMath.SubstitutionSystems.Signatures.
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.FunctorCategory.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 
 Require Import UniMath.CategoryTheory.Epis.
 Require Import UniMath.CategoryTheory.EpiFacts.
@@ -25,12 +25,12 @@ Require Import Modules.Signatures.PreservesEpi.
 Require Import Modules.Signatures.EpiArePointwise.
 
 Require Import UniMath.CategoryTheory.Monads.Monads.
-Require Import UniMath.CategoryTheory.Monads.LModules. 
-Require Import UniMath.CategoryTheory.limits.initial.
-Require Import UniMath.CategoryTheory.limits.bincoproducts.
-Require Import UniMath.CategoryTheory.limits.binproducts.
-Require Import UniMath.CategoryTheory.limits.coproducts.
-Require Import UniMath.CategoryTheory.limits.terminal.
+Require Import UniMath.CategoryTheory.Monads.LModules.
+Require Import UniMath.CategoryTheory.Limits.Initial.
+Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
+Require Import UniMath.CategoryTheory.Limits.BinProducts.
+Require Import UniMath.CategoryTheory.Limits.Coproducts.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
 Require Import UniMath.CategoryTheory.DisplayedCats.Fiber.
 Open Scope cat.
 
@@ -68,7 +68,7 @@ Definition p_alg_ar   : signature C :=
   sigWithStrength_to_sig (C := C) (toSig p_sig).
 
 Definition p_mor : signature_Mor (p_alg_ar ) a := pr1 (pr2 p).
-Definition epi_p_mor   : 
+Definition epi_p_mor   :
   ∏ (R : Monad C), (isEpi (C := [_, _]) (pr1 (p_mor  R)))
   := pr2 (pr2 p).
 
@@ -88,7 +88,7 @@ Local Notation toSig sig :=
 
 
 
-Lemma PresentableisEffective 
+Lemma PresentableisEffective
       {a : signature SET} (p : isPresentable (C := SET) BinProductsHSET BinCoproductsHSET TerminalHSET
                                              (fun i => CoproductsHSET _ (setproperty i)) a)
   :
diff --git a/Modules/Signatures/PresentableSignatureBinProdR.v b/Modules/Signatures/PresentableSignatureBinProdR.v
index b99f6da..bbd16ff 100644
--- a/Modules/Signatures/PresentableSignatureBinProdR.v
+++ b/Modules/Signatures/PresentableSignatureBinProdR.v
@@ -16,14 +16,14 @@ Require Import UniMath.SubstitutionSystems.BinProductOfSignatures.
 
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.FunctorCategory.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 
 Require Import UniMath.CategoryTheory.Epis.
-Require Import UniMath.CategoryTheory.limits.coproducts.
-Require Import UniMath.CategoryTheory.limits.bincoproducts.
-Require Import UniMath.CategoryTheory.limits.coproducts.
-Require Import UniMath.CategoryTheory.limits.binproducts.
-Require Import UniMath.CategoryTheory.limits.terminal.
+Require Import UniMath.CategoryTheory.Limits.Coproducts.
+Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
+Require Import UniMath.CategoryTheory.Limits.Coproducts.
+Require Import UniMath.CategoryTheory.Limits.BinProducts.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
 Require Import UniMath.CategoryTheory.EpiFacts.
 Require Import UniMath.Combinatorics.Lists.
 Require Import UniMath.CategoryTheory.whiskering.
@@ -48,7 +48,7 @@ Require Import Modules.Prelims.LModulesCoproducts.
 Require Import Modules.Prelims.BinProductComplements.
 
 Require Import UniMath.CategoryTheory.Monads.Monads.
-Require Import UniMath.CategoryTheory.Monads.LModules. 
+Require Import UniMath.CategoryTheory.Monads.LModules.
 Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
 (* Require Import Modules.Signatures.FullArToRaw. *)
 Open Scope cat.
@@ -222,7 +222,7 @@ Proof.
   eapply is_iso_qinv.
   apply Sig_isDistributive_is_inverse.
 Defined.
-  (** * The product of a presentable signature with the tautological signature is presentable 
+  (** * The product of a presentable signature with the tautological signature is presentable
 
 It requires that the base category is distributive and that bin products
 of epimorphisms are epimorphisms in the functor category.
@@ -294,20 +294,20 @@ becomes
         * intros z z' f.
           etrans;[apply TerminalArrowUnique|]; apply pathsinv0; apply TerminalArrowUnique.
       + intros c c' f.
-        apply nat_trans_eq; [  apply homset_property|]. 
+        apply nat_trans_eq; [  apply homset_property|].
         intro z.
           etrans;[apply TerminalArrowUnique|]; apply pathsinv0; apply TerminalArrowUnique.
       }
       cbn.
       intros X Y .
-      apply nat_trans_eq; [  apply homset_property|]. 
+      apply nat_trans_eq; [  apply homset_property|].
       intro z.
-      etrans;[apply TerminalArrowUnique|]; apply pathsinv0; apply TerminalArrowUnique. 
+      etrans;[apply TerminalArrowUnique|]; apply pathsinv0; apply TerminalArrowUnique.
     - intros f.
       apply SignatureMor_eq.
-      apply nat_trans_eq; [  apply (homset_property [C,C])|]. 
+      apply nat_trans_eq; [  apply (homset_property [C,C])|].
       intro z.
-      apply nat_trans_eq; [  apply homset_property|]. 
+      apply nat_trans_eq; [  apply homset_property|].
       intro z'.
       apply TerminalArrowUnique.
   Defined.
@@ -319,7 +319,7 @@ becomes
 
   Lemma Signature_to_signature_cons_iso n ar :
     iso (C := SIG) ( (Arity_to_Signature bp bcp T (cons n ar)))
-        (BinProductObject _ (bpSig 
+        (BinProductObject _ (bpSig
                                (precomp_option_iter_Signature bcp T n)
                                (Arity_to_Signature bp bcp T ar)
         )).
@@ -337,11 +337,11 @@ becomes
       apply identity_iso.
   Defined.
 
-  
 
 
 
-Definition har_binprodR_commute_mor_mod 
+
+Definition har_binprodR_commute_mor_mod
   :  iso (C := signature_category)  (p_alg_ar' )
                 ((PO (Sig_bp (sigWithStrength_to_sig (C := C) (toSig Ba)) tautological_signature) : signature C)
                 ) .
diff --git a/Modules/Signatures/PresentableSignatureCoproducts.v b/Modules/Signatures/PresentableSignatureCoproducts.v
index 951496f..1afecc6 100644
--- a/Modules/Signatures/PresentableSignatureCoproducts.v
+++ b/Modules/Signatures/PresentableSignatureCoproducts.v
@@ -12,13 +12,13 @@ Require Import UniMath.SubstitutionSystems.SignatureCategory.
 
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.FunctorCategory.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 
 Require Import UniMath.CategoryTheory.Epis.
-Require Import UniMath.CategoryTheory.limits.coproducts.
-Require Import UniMath.CategoryTheory.limits.bincoproducts.
-Require Import UniMath.CategoryTheory.limits.binproducts.
-Require Import UniMath.CategoryTheory.limits.terminal.
+Require Import UniMath.CategoryTheory.Limits.Coproducts.
+Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
+Require Import UniMath.CategoryTheory.Limits.BinProducts.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
 Require Import UniMath.CategoryTheory.EpiFacts.
 Require Import UniMath.Combinatorics.Lists.
 Require Import UniMath.CategoryTheory.whiskering.
@@ -34,7 +34,7 @@ Require Import Modules.Signatures.HssSignatureCommutation.
 
 
 Require Import UniMath.CategoryTheory.Monads.Monads.
-Require Import UniMath.CategoryTheory.Monads.LModules. 
+Require Import UniMath.CategoryTheory.Monads.LModules.
 Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
 Open Scope cat.
 
@@ -44,7 +44,7 @@ Section CoprodPresentable.
   Context {C : category} {bp : BinProducts C} {bcp : BinCoproducts C} {T : Terminal C}
           {cp : ∏ (I : hSet), Coproducts I C}.
 
-  
+
   Let toSig sig :=
     (BindingSigToSignature bp bcp T
                            sig (cp (BindingSigIndexhSet sig))).
@@ -82,7 +82,7 @@ Section CoprodPresentable.
   Proof.
     intro R.
     use isEpi_comp;[| use isEpi_comp].
-    - 
+    -
       unfold coprod_ρ_mor.
       (* TODO utiliser is_iso_pw *)
       (* use Pushouts_pw_epi. *)
diff --git a/Modules/Signatures/PreservesEpi.v b/Modules/Signatures/PreservesEpi.v
index 9a16b2e..9d19004 100644
--- a/Modules/Signatures/PreservesEpi.v
+++ b/Modules/Signatures/PreservesEpi.v
@@ -13,10 +13,10 @@ Require Import UniMath.Foundations.Sets.
 
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.FunctorCategory.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
-Require Import UniMath.CategoryTheory.limits.bincoproducts.
-Require Import UniMath.CategoryTheory.limits.terminal.
-Require Import UniMath.CategoryTheory.limits.binproducts.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
+Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
+Require Import UniMath.CategoryTheory.Limits.BinProducts.
 Require Import UniMath.CategoryTheory.Epis.
 Require Import UniMath.CategoryTheory.EpiFacts.
 
@@ -40,7 +40,7 @@ Require Import Modules.Signatures.SignatureBinproducts.
   (** An epi-signature preserves epimorphicity of natural
       transformations. Note that this is not implied by the axiom of choice
       because the retract may not be a monad morphism.
-      (see [algSig_NatEpi] in PresentableSignature for the example of algebraic signatures 
+      (see [algSig_NatEpi] in PresentableSignature for the example of algebraic signatures
    *)
 Definition sig_preservesNatEpiMonad {C : category} (c : signature C)
   : UU
@@ -70,8 +70,8 @@ Proof.
 Qed.
 
 (** Proof that an epiSig preserves natural epimorphicity *)
-Lemma epiSig_NatEpi {C : category} (S : Signature C 
-                                                  C 
+Lemma epiSig_NatEpi {C : category} (S : Signature C
+                                                  C
                                                   C)
       (epiS : preserves_Epi (S : functor _ _)) : sig_preservesNatEpiMonad (sigWithStrength_to_sig S).
 Proof.
@@ -90,7 +90,7 @@ Qed.
 Corollary  algSig_NatEpi (S : BindingSig)
   : sig_preservesNatEpiMonad
       (sigWithStrength_to_sig (C := SET)
-                 (BindingSigToSignature 
+                 (BindingSigToSignature
                                         BinProductsHSET
                                         BinCoproductsHSET TerminalHSET
                                         S
@@ -137,7 +137,7 @@ Proof.
   apply productEpis;[apply h1|apply h2]; exact epif.
 Defined.
 
-Definition binProd_epiSigSET 
+Definition binProd_epiSigSET
       (S1 S2 : signature SET)
       (h1 : sig_preservesNatEpiMonad_pw S1)
       (h2 : sig_preservesNatEpiMonad_pw S2)
diff --git a/Modules/Signatures/Signature.v b/Modules/Signatures/Signature.v
index a8d4cee..b8b74b6 100644
--- a/Modules/Signatures/Signature.v
+++ b/Modules/Signatures/Signature.v
@@ -13,7 +13,7 @@ Require Import UniMath.Foundations.Sets.
 
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.FunctorCategory.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 Require Import UniMath.CategoryTheory.Epis.
 Require Import UniMath.CategoryTheory.EpiFacts.
 
@@ -55,8 +55,8 @@ Definition signature_on_objects (a : signature_data) : ∏ R, LModule R C
 
 Coercion signature_on_objects : signature_data >-> Funclass.
 
-Definition signature_on_morphisms  (F : signature_data) {R S : MONAD} 
-  : ∏ (f: Monad_Mor R S), LModule_Mor _ (F R) (pb_LModule f (F S)) 
+Definition signature_on_morphisms  (F : signature_data) {R S : MONAD}
+  : ∏ (f: Monad_Mor R S), LModule_Mor _ (F R) (pb_LModule f (F S))
   := pr2 F R S.
 
 Notation "# F" := (signature_on_morphisms F) (at level 3) : signature_scope.
@@ -73,8 +73,8 @@ Definition signature_idax  (F : signature_data) :=
 
 Definition signature_compax  (F : signature_data) :=
   ∏ (R S T : MONAD) (f : PRE_MONAD ⟦R, S⟧) (g : PRE_MONAD ⟦S, T⟧),
-  (#F  (f · g))%ar 
-  = 
+  (#F  (f · g))%ar
+  =
   (((# F f)%ar :(F R : bmod_disp C C R) -->[f] F S) ;; (#F g)%ar)%mor_disp.
 
 Definition is_signature  (F : signature_data) : UU := signature_idax F × signature_compax F.
@@ -96,7 +96,7 @@ Coercion signature_data_from_signature : signature >-> signature_data.
 Notation Θ := tautological_LModule.
 
 Definition tautological_signature_on_objects : ∏ (R : Monad C), LModule R C := Θ.
-Definition tautological_signature_on_morphisms : 
+Definition tautological_signature_on_morphisms :
   ∏ (R S : Monad C) (f : Monad_Mor R S), LModule_Mor _ (Θ R) (pb_LModule f (Θ S)) :=
   @monad_mor_to_lmodule C.
 
@@ -127,20 +127,20 @@ Definition signature_id (F : signature) :
   := pr1 (pr2 F).
 (* ((# F (identity (C:= PRE_MONAD) R): LModule_Mor _ _ _ ))%ar x  = identity  _ *)
 
-Definition signature_comp (F : signature) {R S T : MONAD} 
-           (f : PRE_MONAD ⟦R,S⟧) (g : PRE_MONAD⟦S,T⟧) 
-  : (#F  (f · g))%ar 
-    = 
-    ((# F f : (F R : bmod_disp C C R) -->[f] F S) %ar ;; (#F g)%ar)%mor_disp 
+Definition signature_comp (F : signature) {R S T : MONAD}
+           (f : PRE_MONAD ⟦R,S⟧) (g : PRE_MONAD⟦S,T⟧)
+  : (#F  (f · g))%ar
+    =
+    ((# F f : (F R : bmod_disp C C R) -->[f] F S) %ar ;; (#F g)%ar)%mor_disp
   := pr2 (pr2 F) _ _ _ _ _ .
 
 (* Demander la version pointwise plutôt ? *)
 Definition is_signature_Mor (F F' : signature_data)
-           (t : ∏ R : MONAD, LModule_Mor R (F R)  (F' R)) 
+           (t : ∏ R : MONAD, LModule_Mor R (F R)  (F' R))
   :=
     ∏ (R S : MONAD)(f : Monad_Mor R S),
     (((# F)%ar f :   nat_trans _ _) : [_,_]⟦_,_⟧) ·
-                                                  (t S : nat_trans _ _) 
+                                                  (t S : nat_trans _ _)
     =
     ((t R : nat_trans _ _) : [_,_]⟦_,_⟧) · ((#F')%ar f : nat_trans _ _).
 
@@ -156,7 +156,7 @@ Proof.
 Qed.
 
 Definition signature_Mor  (F F' : signature_data) : UU := ∑ X, is_signature_Mor F F' X.
-                            
+
 Local Notation "F ⟹ G" := (signature_Mor F G) (at level 39) : signature_scope.
 
 Lemma isaset_signature_Mor (F F' : signature) : isaset (signature_Mor F F').
@@ -171,18 +171,18 @@ Definition signature_Mor_data
  {F F' : signature_data}(a : signature_Mor F F') := pr1 a.
 Coercion signature_Mor_data : signature_Mor >-> Funclass.
 
-Definition signature_Mor_ax {F F' : signature} (a : signature_Mor F F') 
+Definition signature_Mor_ax {F F' : signature} (a : signature_Mor F F')
   : ∏ {R S : MONAD}(f : Monad_Mor R S),
     (((# F)%ar f :   nat_trans _ _) : [_,_]⟦_,_⟧) ·
-                                                  (a S : nat_trans _ _) 
+                                                  (a S : nat_trans _ _)
     =
     ((a R : nat_trans _ _) : [_,_]⟦_,_⟧) · ((#F')%ar f : nat_trans _ _)
   := pr2 a.
 
-Lemma signature_Mor_ax_pw {F F' : signature} (a : signature_Mor F F') 
+Lemma signature_Mor_ax_pw {F F' : signature} (a : signature_Mor F F')
   : ∏ {R S : Monad C}(f : Monad_Mor R S) x,
     (((# F)%ar f :   nat_trans _ _) x) ·
-                                       ((a S : nat_trans _ _) x) 
+                                       ((a S : nat_trans _ _) x)
     =
     ((a R : nat_trans _ _)  x) · (((#F')%ar f : nat_trans _ _) x).
 Proof.
@@ -203,7 +203,7 @@ Proof.
   apply (total2_paths_f H'), proofirrelevance, isaprop_is_signature_Mor.
 Qed.
 
-Lemma is_signature_Mor_comp {F G H : signature} (a : signature_Mor F G) (b : signature_Mor G H) 
+Lemma is_signature_Mor_comp {F G H : signature} (a : signature_Mor F G) (b : signature_Mor G H)
   : is_signature_Mor F H (fun R  => (a R : category_LModule _ _ ⟦_,_⟧ ) · b R).
 Proof.
   intros ? ? ?.
@@ -235,7 +235,7 @@ Definition signature_Mor_id (F : signature_data) : signature_Mor F F :=
     tpair _ _ (is_signature_Mor_id F).
 
 Definition signature_Mor_comp {F G H : signature} (a : signature_Mor F G) (b : signature_Mor G H)
-  : signature_Mor F H 
+  : signature_Mor F H
   := tpair _ _ (is_signature_Mor_comp a b).
 
 Definition signature_precategory_data : precategory_data.
@@ -253,7 +253,7 @@ Proof.
   apply make_is_precategory_one_assoc; simpl; intros.
   - unfold identity.
     simpl.
-    apply signature_Mor_eq. 
+    apply signature_Mor_eq.
     intro x; simpl.
     apply (id_left (C:=category_LModule _ _)).
   - apply signature_Mor_eq.
@@ -330,13 +330,13 @@ That's how the large category of models is built.
 
 
 Section LargeCatRep.
-  
+
 Context {C : category}.
-  
+
 Local Notation MONAD := (Monad C).
 Local Notation PRE_MONAD := (category_Monad C).
 Local Notation BMOD := (bmod_disp C C).
-  
+
 
 (* Signatures are display functors over the identity *)
 Local Notation PRECAT_SIGNATURE  := (@signature_category C).
@@ -365,11 +365,11 @@ Coercion Monad_from_rep_ar (ar : SIGNATURE) (X : model ar) : MONAD := pr1 X.
 Definition model_τ {ar : signature} (X : model ar) := pr2 X.
 
 Definition model_mor_law {a b : signature} (M : model a) (N : model b)
-           (f : signature_Mor a b) (g : Monad_Mor M N) 
+           (f : signature_Mor a b) (g : Monad_Mor M N)
   := ∏ c : C, model_τ M c · g c = ((#a g)%ar:nat_trans _ _) c · f N c · model_τ N c .
 
 Lemma isaprop_model_mor_law {a b : SIGNATURE} (M : model a) (N : model b)
-      (f : signature_Mor a b) (g : Monad_Mor M N) 
+      (f : signature_Mor a b) (g : Monad_Mor M N)
   : isaprop (model_mor_law M N f g).
 Proof.
   intros.
@@ -397,7 +397,7 @@ Coercion monad_morphism_from_model_mor_mor {a b : SIGNATURE} {M : model a} {N :
 
 Definition model_mor_ax {a b : SIGNATURE} {M : model a} {N : model b}
            {f} (h:model_mor_mor a b M N f) :
-  ∏ c, model_τ M c · h c = (#a h)%ar c · f N c · model_τ N c 
+  ∏ c, model_τ M c · h c = (#a h)%ar c · f N c · model_τ N c
   := pr2 h.
 
 Definition rep_disp_ob_mor : disp_cat_ob_mor PRECAT_SIGNATURE :=
@@ -411,7 +411,7 @@ Proof.
   etrans.
     { apply cancel_postcomposition, id_right. }
   etrans.
-    { apply cancel_postcomposition, (signature_id a (pr1 RM) c). } 
+    { apply cancel_postcomposition, (signature_id a (pr1 RM) c). }
   etrans; [  apply id_left |].
   apply pathsinv0.
   apply id_right.
@@ -448,10 +448,10 @@ Lemma model_mor_mor_equiv (a b : SIGNATURE) (R:rep_disp_ob_mor a)
   (∏ c, pr1 u c = pr1 v c) -> u = v.
 Proof.
   intros.
-  use (invmap (subtypeInjectivity _ _ _ _  )). 
+  use (invmap (subtypeInjectivity _ _ _ _  )).
   - intro g.
     apply isaprop_model_mor_law.
-  - use (invmap (Monad_Mor_equiv _ _)).  
+  - use (invmap (Monad_Mor_equiv _ _)).
      +  apply nat_trans_eq.
         apply homset_property.
         assumption.
@@ -468,19 +468,19 @@ Lemma rep_comp_law  (a b c : SIGNATURE) (f : signature_Mor a b) (g : signature_M
                            ( monad_morphism_from_model_mor_mor  β))).
 Proof.
   intro x.
-  cbn.    
+  cbn.
   rewrite assoc.
   etrans.
   { apply cancel_postcomposition.
     use model_mor_ax. }
-    
+
   etrans.
   { rewrite <- assoc.
     apply cancel_precomposition.
     use model_mor_ax. }
-  
+
   (* Cf diagramme à ce point *)
-  
+
   symmetry.
   repeat rewrite assoc.
   apply cancel_postcomposition.
@@ -503,11 +503,11 @@ Proof.
 Qed.
 
 Definition rep_comp (a b c : SIGNATURE) f g
-           (RMa : rep_disp_ob_mor a) 
-           (RMb : rep_disp_ob_mor b)    
+           (RMa : rep_disp_ob_mor a)
+           (RMb : rep_disp_ob_mor b)
            (RMc : rep_disp_ob_mor c)
-           (mab : RMa -->[ f ] RMb) 
-           (mbc:RMb -->[g]  RMc) 
+           (mab : RMa -->[ f ] RMb)
+           (mbc:RMb -->[g]  RMc)
   : RMa -->[f·g] RMc.
 Proof.
   intros.
@@ -599,7 +599,7 @@ Proof.
     + apply hh.
     + apply rep_mor_law_pb.
 Defined.
-    
+
 Definition pb_rep_to_cartesian {a a'} (f : signature_category ⟦ a, a' ⟧)
            (R : model a') : is_cartesian ((pb_rep_to f R) :
                                              (pb_rep f R : rep_disp a) -->[_] R).
@@ -633,7 +633,7 @@ Proof.
   - apply pb_rep_to.
   - apply pb_rep_to_cartesian.
 Defined.
-     
+
 End LargeCatRep.
 
 Arguments rep_disp _ : clear implicits.
@@ -660,7 +660,7 @@ Lemma transport_disp_mor {C} {d:disp_cat C} {x y : C} {f g : C ⟦ x, y ⟧}
   (*
 Lemma rep_ar_mor_mor_equiv_inv {a b : SIGNATURE} {R:rep_disp_ob_mor a}
       {S:rep_disp_ob_mor b} {f:signature_Mor  a b}
-      (u v: R -->[ f] S) 
+      (u v: R -->[ f] S)
   : u = v -> (∏ c, pr1 (pr1 u) c = pr1 (pr1 v) c).
 Proof.
   intros.
@@ -669,7 +669,7 @@ Qed.
    *)
 
   (*
- Lemma transport_signature_mor' (x y : SIGNATURE) f g 
+ Lemma transport_signature_mor' (x y : SIGNATURE) f g
         (e : f = g)
         (ff : disp_nat_trans f x y)
         (R:MONAD)
diff --git a/Modules/Signatures/SignatureBinproducts.v b/Modules/Signatures/SignatureBinproducts.v
index e45b751..5a1bb28 100644
--- a/Modules/Signatures/SignatureBinproducts.v
+++ b/Modules/Signatures/SignatureBinproducts.v
@@ -17,8 +17,8 @@ Require Import UniMath.CategoryTheory.Monads.LModules.
 Require Import UniMath.CategoryTheory.DisplayedCats.Core.
 Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
 
-Require Import UniMath.CategoryTheory.limits.binproducts.
-Require Import UniMath.CategoryTheory.limits.graphs.colimits.
+Require Import UniMath.CategoryTheory.Limits.BinProducts.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
 
 Require Import Modules.Prelims.lib.
 Require Import Modules.Prelims.BinProductComplements.
@@ -110,11 +110,11 @@ Section Binprod.
         rewrite id_right.
         apply idpath.
   Qed.
-      
+
   Definition signature_binProd : Signature := _ ,, signature_binProd_is_signature.
 
-  Lemma signature_binProductPr1_laws : 
-    is_signature_Mor signature_binProd a 
+  Lemma signature_binProductPr1_laws :
+    is_signature_Mor signature_binProd a
                  (fun R => BinProductPr1  _  (cpLM R (a R) (b R)   )).
   Proof.
     intros R S f.
@@ -128,8 +128,8 @@ Section Binprod.
     use (BinProductOfArrowsPr1 _  CC).
   Qed.
 
-  Lemma signature_binProductPr2_laws : 
-    is_signature_Mor signature_binProd b 
+  Lemma signature_binProductPr2_laws :
+    is_signature_Mor signature_binProd b
                  (fun R => BinProductPr2  _  (cpLM R (a R) (b R)   )).
   Proof.
     intros R S f.
@@ -143,10 +143,10 @@ Section Binprod.
     use (BinProductOfArrowsPr2 _  CC).
   Qed.
 
-  Definition signature_binProductPr1 : 
+  Definition signature_binProductPr1 :
     signature_Mor  signature_binProd a := _ ,, signature_binProductPr1_laws .
 
-  Definition signature_binProductPr2 : 
+  Definition signature_binProductPr2 :
     signature_Mor  signature_binProd b := _ ,, signature_binProductPr2_laws .
 
   (* TODO : move to Signature *)
@@ -154,7 +154,7 @@ Section Binprod.
              (cb : signature_Mor c b)
     :
     is_signature_Mor
-      c signature_binProd 
+      c signature_binProd
       (fun R => BinProductArrow  _  (cpLM R (a R) (b R)) (ca R) (cb R))  .
   Proof.
     intros R S f.
@@ -188,7 +188,7 @@ Section Binprod.
   Qed.
 
   Definition signature_binProductArrow {c : Signature} (ca :  signature_Mor c a )
-             (cb : signature_Mor c b) : 
+             (cb : signature_Mor c b) :
     signature_Mor c signature_binProd  := _ ,, signature_binProductArrow_laws ca cb.
 
   Lemma signature_isBinProduct : isBinProduct signature_category   _ _ _
diff --git a/Modules/Signatures/SignatureCoproduct.v b/Modules/Signatures/SignatureCoproduct.v
index 710d520..1d8e029 100644
--- a/Modules/Signatures/SignatureCoproduct.v
+++ b/Modules/Signatures/SignatureCoproduct.v
@@ -1,7 +1,7 @@
 (**
 pullback of coproducts
  Coproducts of arities using LModule Coproducts (more
-conveninent than LModule.Colims) 
+conveninent than LModule.Colims)
  *)
 Require Import UniMath.Foundations.PartD.
 Require Import UniMath.Foundations.Propositions.
@@ -15,8 +15,8 @@ Require Import UniMath.CategoryTheory.Monads.LModules.
 Require Import UniMath.CategoryTheory.DisplayedCats.Core.
 Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
 
-Require Import UniMath.CategoryTheory.limits.coproducts.
-Require Import UniMath.CategoryTheory.limits.graphs.colimits.
+Require Import UniMath.CategoryTheory.Limits.Coproducts.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
 
 Require Import Modules.Prelims.lib.
 Require Import Modules.Prelims.CoproductsComplements.
@@ -95,10 +95,10 @@ Section Coprod.
       rewrite id_right.
       apply idpath.
   Qed.
-      
+
   Definition signature_coprod : Signature := _ ,, signature_coprod_is_signature.
 
-  Lemma signature_coproductIn_laws o : 
+  Lemma signature_coproductIn_laws o :
     is_signature_Mor (α o) signature_coprod
                  (fun R => CoproductIn  _ _  (cpLM R (fun o => α o R)) o  ).
   Proof.
@@ -114,7 +114,7 @@ Section Coprod.
     use (CoproductOfArrowsIn _ _ CC).
   Qed.
 
-  Definition signature_coproductIn o : 
+  Definition signature_coproductIn o :
     signature_Mor  (α o) signature_coprod := _ ,, signature_coproductIn_laws o.
 
   (* TODO : move to Signature *)
diff --git a/Modules/Signatures/SignatureDerivation.v b/Modules/Signatures/SignatureDerivation.v
index ea53cfa..5cdb0a7 100644
--- a/Modules/Signatures/SignatureDerivation.v
+++ b/Modules/Signatures/SignatureDerivation.v
@@ -15,9 +15,9 @@ Require Import UniMath.CategoryTheory.Monads.Derivative.
 Require Import UniMath.CategoryTheory.DisplayedCats.Core.
 Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
 
-Require Import UniMath.CategoryTheory.limits.coproducts.
-Require Import UniMath.CategoryTheory.limits.graphs.colimits.
-Require Import UniMath.CategoryTheory.limits.terminal.
+Require Import UniMath.CategoryTheory.Limits.Coproducts.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
 
 Require Import Modules.Prelims.lib.
 Require Import Modules.Prelims.LModulesCoproducts.
@@ -27,8 +27,8 @@ Require Import Modules.Signatures.Signature.
 Section DAr.
 
   Context {C : category}
-          (bcpC : limits.bincoproducts.BinCoproducts C)
-          (CT : limits.terminal.Terminal C).
+          (bcpC : Limits.BinCoproducts.BinCoproducts C)
+          (CT : Limits.Terminal.Terminal C).
 Local Notation "∂" := (LModule_deriv_functor (TerminalObject CT) bcpC
                                               _).
 
diff --git a/Modules/Signatures/SignaturesColims.v b/Modules/Signatures/SignaturesColims.v
index c177921..a3ae140 100644
--- a/Modules/Signatures/SignaturesColims.v
+++ b/Modules/Signatures/SignaturesColims.v
@@ -14,8 +14,8 @@ Require Import UniMath.MoreFoundations.Tactics.
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.FunctorCategory.
 Require Import UniMath.CategoryTheory.whiskering.
-Require Import UniMath.CategoryTheory.limits.graphs.limits.
-Require Import UniMath.CategoryTheory.limits.graphs.colimits.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Limits.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
 Require Import UniMath.CategoryTheory.Monads.Monads.
 Require Import UniMath.CategoryTheory.Monads.LModules.
 
@@ -26,11 +26,11 @@ Require Import Modules.Prelims.CoproductsComplements.
 Local Open Scope cat.
 
 (*
-Lemma compfNat 
-   {C : precategory} {g : graph} {d1 d2 d3 : diagram g C}  
-   
+Lemma compfNat
+   {C : precategory} {g : graph} {d1 d2 d3 : diagram g C}
+
    {f : ∏ u : vertex g, C ⟦ dob d1 u, dob d2 u ⟧}
-  (fNat : ∏ (u v : vertex g) (e : edge u v), dmor d1 e · f v = f u · dmor d2 e) 
+  (fNat : ∏ (u v : vertex g) (e : edge u v), dmor d1 e · f v = f u · dmor d2 e)
    {f2 : ∏ u : vertex g, C ⟦ dob d2 u, dob d3 u ⟧}
    (fNat2 : ∏ (u v : vertex g) (e : edge u v), dmor d2 e · f2 v = f2 u · dmor d3 e)
    (f3 := fun u => f u · f2 u)
@@ -47,12 +47,12 @@ Qed.
 *)
 (*
 Lemma compColimOfArrows
-   (C : precategory) (g : graph) (d1 d2 d3 : diagram g C) (CC1 : ColimCocone d1) 
+   (C : precategory) (g : graph) (d1 d2 d3 : diagram g C) (CC1 : ColimCocone d1)
    (CC2 : ColimCocone d2)(CC3 : ColimCocone d3)
    (f : ∏ u : vertex g, C ⟦ dob d1 u, dob d2 u ⟧)
-  (fNat : ∏ (u v : vertex g) (e : edge u v), dmor d1 e · f v = f u · dmor d2 e) 
+  (fNat : ∏ (u v : vertex g) (e : edge u v), dmor d1 e · f v = f u · dmor d2 e)
    (f2 : ∏ u : vertex g, C ⟦ dob d2 u, dob d3 u ⟧)
-  (fNat2 : ∏ (u v : vertex g) (e : edge u v), dmor d2 e · f2 v = f2 u · dmor d3 e) 
+  (fNat2 : ∏ (u v : vertex g) (e : edge u v), dmor d2 e · f2 v = f2 u · dmor d3 e)
   (x : C) (cc : cocone d2 x) :
   colimOfArrows CC1 CC2 f fNat · colimOfArrows CC2 CC3 f2 fNat2 =
   colimOfArrows CC1 CC3 (fun z => f z · f2 z) (compfNat  fNat fNat2).
@@ -70,7 +70,7 @@ Lemma compColimOfArrows
 
   reflexivity.
 .fNat · colimOfArrows CC2 CC3 f2 fNat2 .
-  colimOfArrows CC1 CC3 (fun 
+  colimOfArrows CC1 CC3 (fun
   colimArrow CC1 x
     (make_cocone (λ u : vertex g, f u · coconeIn cc u)
        (preCompWithColimOfArrows_subproof CC1 CC2 f fNat x cc)).
@@ -80,8 +80,8 @@ Lemma compColimOfArrows
 (* TODO déplacer ça dans Signature.v *)
 
 Section ColimsSig.
-  
-  Context 
+
+  Context
           {C : category}
           {g : graph} (colims_g : Colims_of_shape g C)
           (lims_g : Lims_of_shape g C).
@@ -197,7 +197,7 @@ Section ColimsSig.
       cbn.
       now rewrite id_right.
   Qed.
-  
+
   Lemma Sig_lim_is_signature : is_signature Sig_lim_signature_data.
   Proof.
     split.
@@ -263,8 +263,8 @@ Section ColimsSig.
 
 
 
-  Lemma Sig_coconeIn_laws v : 
-    is_signature_Mor 
+  Lemma Sig_coconeIn_laws v :
+    is_signature_Mor
                       (dob d v : signature  _)  Sig_colim
       (fun R => (coconeIn (colimCocone (coMod R (d' R))) v   )).
   Proof.
@@ -280,10 +280,10 @@ Section ColimsSig.
     cbn.
     apply (colimArrowCommutes cc2).
   Qed.
-  
-  Lemma Sig_coneOut_laws v : 
-    is_signature_Mor 
-                  Sig_lim    (dob d v : signature  _)  
+
+  Lemma Sig_coneOut_laws v :
+    is_signature_Mor
+                  Sig_lim    (dob d v : signature  _)
       (fun R => (coneOut (limCone (limMod R (d' R))) v   )).
   Proof.
     intros X Y f.
@@ -360,10 +360,10 @@ Section ColimsSig.
     cbn.
     apply signature_Mor_ax_pw.
   Qed.
-  
+
   Lemma Sig_limArrow_laws {M : signature C} (cc : cone d M) :
     is_signature_Mor
-      M  (  Sig_lim) 
+      M  (  Sig_lim)
       (fun R => limArrow  (limMod R (d' R)) (M R) (mapcone (FORGET R) d cc)  ).
   Proof.
     intros R S f.
@@ -425,7 +425,7 @@ Section ColimsSig.
       intro u.
       apply (  maponpaths (fun z => pr1 z R) (h u)).
   Defined.
-  
+
   Lemma Sig_isLimCone : isLimCone _ _ Sig_lim_cone.
     intros M cc.
     use unique_exists.
diff --git a/Modules/Signatures/quotientrep.v b/Modules/Signatures/quotientrep.v
index 19d3bbb..8abb79d 100644
--- a/Modules/Signatures/quotientrep.v
+++ b/Modules/Signatures/quotientrep.v
@@ -4,10 +4,10 @@ Require Import UniMath.Foundations.PartD.
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.FunctorCategory.
 Require Import UniMath.CategoryTheory.Monads.Monads.
-Require Import UniMath.CategoryTheory.Monads.LModules. 
+Require Import UniMath.CategoryTheory.Monads.LModules.
 Require Import UniMath.CategoryTheory.SetValuedFunctors.
 Require Import UniMath.CategoryTheory.HorizontalComposition.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 
 Require Import UniMath.Foundations.Sets.
 Require Import UniMath.CategoryTheory.Epis.
@@ -26,7 +26,7 @@ Local Notation "Z ∘ α" := (post_whisker α Z).
 
 Open Scope cat.
 
-    
+
 Set Automatic Introduction.
 
 Section QuotientMonad.
@@ -39,7 +39,7 @@ Context {R : Monad SET}
         (compat_μ_projR : compat_μ_projR_def congr_equivc).
 
 Let equivc {c:hSet} x y : hProp := eqrel_equivc c x y.
-  
+
 (* We define the quotient functor of R by these equivalence relations
 
 The following comment may be outdated
@@ -109,7 +109,7 @@ Context
         {h : LModule_Mor _ a (pb_LModule projR_monad b)}
         (* TODO : define the general type of compatability that is used everywhere to define
             a morphism out of an epimorphism (Cf quotient monad : compat_μ_def ..) *)
-        (compath : ∏ X (x y:(a X:hSet)), h X x = h X y -> 
+        (compath : ∏ X (x y:(a X:hSet)), h X x = h X y ->
                                          (τ X · projR_monad X) x = (τ X · projR_monad X) y)
         (* TODO : demander que ce soit pointwise epi plutôt *)
         (isEpih : isEpi (C:=[SET,SET]) (h:nat_trans _ _)).
@@ -123,7 +123,7 @@ Proof.
 Defined.
 
 Local Notation τ' := R'_model_τ.
-           
+
 Definition R'_model_τ_def : ∏ X, h X · τ' X = τ X · projR_monad X.
 Proof.
   apply (univ_surj_nt_ax_pw _
@@ -213,21 +213,21 @@ Lemma τ'_law_eq2 X : ((h∙∙projR_monad :[SET,SET]⟦_,_⟧)
 Proof.
   etrans.
   { apply cancel_postcomposition.
-    apply (LModule_Mor_σ R h). 
+    apply (LModule_Mor_σ R h).
   }
   repeat rewrite <- assoc.
   apply cancel_precomposition.
   apply R'_model_τ_def.
 Qed.
 
-Lemma R'_model_τ_module_laws 
-  : LModule_Mor_laws _ 
+Lemma R'_model_τ_module_laws
+  : LModule_Mor_laws _
                      (T:=b)
                      (T':= tautological_LModule R'_monad)
                      R'_model_τ.
 Proof.
   intro X.
-  
+
   (* En vrai, je n'ai pas besoin ici que ce soit un epi pointwise (me semble-t-il)*)
   assert (epi : isEpi (* (C:=functor_Precategory SET SET) *)
                   ((h ∙∙ projR) X)
@@ -242,9 +242,9 @@ Proof.
   etrans; [ apply τ'_law_eq1 |].
   apply pathsinv0.
   apply τ'_law_eq2.
-Qed.    
+Qed.
 
-Definition R'_model_τ_module : LModule_Mor _ b (tautological_LModule R'_monad) 
+Definition R'_model_τ_module : LModule_Mor _ b (tautological_LModule R'_monad)
   := _ ,, R'_model_τ_module_laws.
 
 (** Let S a monad, m : R -> S a monad morphism compatible with the equivalence relation
@@ -265,9 +265,9 @@ This induces a monad morphism u : R' -> S that makes the following diagram commu
 
 
 *)
-Context {S : Monad SET}  
+Context {S : Monad SET}
         {m : Monad_Mor R S}
-        (compatm : ∏ (X : SET) 
+        (compatm : ∏ (X : SET)
                      (x y : (R X : hSet)), projR X x = projR X y → m X x = m X y).
 
 Let u_monad := quotientmonad.u_monad R_epi compat_μ_projR _ compatm.
@@ -318,7 +318,7 @@ h ;; τ' ;; u =  τ ;; π ;; u (definition of τ')
 
 *)
 
-Context {c : LModule S SET} 
+Context {c : LModule S SET}
         {s : LModule_Mor _ c (Θ S)}
         {F : LModule_Mor _ b (pb_LModule u_monad c)}.
 
@@ -339,7 +339,7 @@ Proof.
   { rewrite assoc.
     apply cancel_postcomposition.
     apply R'_model_τ_def.
-  } 
+  }
   etrans.
   { rewrite <- assoc.
     apply cancel_precomposition.
diff --git a/Modules/SoftEquations/AdjunctionEquationRep.v b/Modules/SoftEquations/AdjunctionEquationRep.v
index a9c8715..9f88054 100644
--- a/Modules/SoftEquations/AdjunctionEquationRep.v
+++ b/Modules/SoftEquations/AdjunctionEquationRep.v
@@ -24,12 +24,12 @@ More generally, the forgetful functor from 2-models to 1-models has a left adjoi
 Require Import UniMath.Foundations.PartD.
 
 Require Import UniMath.CategoryTheory.Monads.Monads.
-Require Import UniMath.CategoryTheory.Monads.LModules. 
+Require Import UniMath.CategoryTheory.Monads.LModules.
 Require Import UniMath.CategoryTheory.SetValuedFunctors.
 Require Import UniMath.CategoryTheory.HorizontalComposition.
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.FunctorCategory.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 Require Import UniMath.CategoryTheory.Subcategory.Core.
 Require Import UniMath.CategoryTheory.Subcategory.Full.
 Require Import UniMath.SubstitutionSystems.BindingSigToMonad.
@@ -57,7 +57,7 @@ Require Import Modules.Signatures.BindingSig.
 Require Import Modules.SoftEquations.BindingSig.
 
 Require Import UniMath.CategoryTheory.Adjunctions.Core.
-Require Import UniMath.CategoryTheory.limits.initial.
+Require Import UniMath.CategoryTheory.Limits.Initial.
 
 
 Local Notation  "R →→ S" := (rep_fiber_mor R S) (at level 6).
@@ -199,12 +199,12 @@ Section QuotientRepInit.
 End QuotientRepInit.
 
 (** As a corrolary, the case of an algebraic signature *)
-Definition elementary_equations_on_alg_preserve_initiality 
+Definition elementary_equations_on_alg_preserve_initiality
           (S : BindingSig) (Sig := binding_to_one_sigHSET S)
 
            (O : UU) (eq : O → elementary_equation (Sig := Sig))
            (R := bindingSigHSET_Initial S : Initial (rep_fiber_category Sig))
-           (iniEpi :=  algebraic_model_Epi S : preserves_Epi (InitialObject R : model Sig)) 
+           (iniEpi :=  algebraic_model_Epi S : preserves_Epi (InitialObject R : model Sig))
            (epiSig := algSig_NatEpi S)
            (SR_epi := BindingSigAreEpiEpiSig S)
            (** A family of equations *)
@@ -216,7 +216,7 @@ Definition elementary_equations_on_alg_preserve_initiality
 
 
 (** A version using the axiom of choice *)
-Lemma soft_equations_preserve_initiality_choice 
+Lemma soft_equations_preserve_initiality_choice
   (ax_choice : AxiomOfChoice.AxiomOfChoice_surj) :
 
          ∏ (** The 1-signature *)
@@ -236,7 +236,7 @@ Qed.
 
 
 (** A version using the axiom of choice *)
-Lemma elementary_equations_preserve_initiality_choice 
+Lemma elementary_equations_preserve_initiality_choice
   (ax_choice : AxiomOfChoice.AxiomOfChoice_surj) :
 
          ∏ (** The 1-signature *)
@@ -254,8 +254,8 @@ Lemma elementary_equations_preserve_initiality_choice
          Initial (category_model_equations
                     (fun o =>
                        soft_equation_from_elementary_equation
-                         epiSig 
+                         epiSig
                          (eq o))
                  ).
   intros; use soft_equations_preserve_initiality_choice;  assumption.
-Qed.
\ No newline at end of file
+Qed.
diff --git a/Modules/SoftEquations/BindingSig.v b/Modules/SoftEquations/BindingSig.v
index a5048d1..12f2121 100644
--- a/Modules/SoftEquations/BindingSig.v
+++ b/Modules/SoftEquations/BindingSig.v
@@ -7,13 +7,13 @@
 Require Import UniMath.Foundations.PartD.
 
 Require Import UniMath.CategoryTheory.Monads.Monads.
-Require Import UniMath.CategoryTheory.Monads.LModules. 
+Require Import UniMath.CategoryTheory.Monads.LModules.
 Require Import UniMath.CategoryTheory.SetValuedFunctors.
 Require Import UniMath.CategoryTheory.HorizontalComposition.
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.FunctorCategory.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
-Require Import UniMath.CategoryTheory.limits.bincoproducts.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
+Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
 Require Import UniMath.CategoryTheory.catiso.
 
 Require Import UniMath.Foundations.Sets.
@@ -40,10 +40,10 @@ Require Import Modules.SoftEquations.quotientequation.
 Require Import Modules.Prelims.BinProductComplements.
 Require Import Modules.Prelims.CoproductsComplements.
 
-Require Import UniMath.CategoryTheory.limits.initial.
-Require Import UniMath.CategoryTheory.limits.binproducts.
-Require Import UniMath.CategoryTheory.limits.coproducts.
-Require Import UniMath.CategoryTheory.limits.terminal.
+Require Import UniMath.CategoryTheory.Limits.Initial.
+Require Import UniMath.CategoryTheory.Limits.BinProducts.
+Require Import UniMath.CategoryTheory.Limits.Coproducts.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
 
 Require Import Modules.SoftEquations.SignatureOverBinproducts.
 
diff --git a/Modules/SoftEquations/CatOfTwoSignatures.v b/Modules/SoftEquations/CatOfTwoSignatures.v
index d756fc4..9515c0d 100644
--- a/Modules/SoftEquations/CatOfTwoSignatures.v
+++ b/Modules/SoftEquations/CatOfTwoSignatures.v
@@ -16,16 +16,16 @@
 Require Import UniMath.Foundations.PartD.
 
 Require Import UniMath.CategoryTheory.Monads.Monads.
-Require Import UniMath.CategoryTheory.Monads.LModules. 
+Require Import UniMath.CategoryTheory.Monads.LModules.
 Require Import UniMath.CategoryTheory.SetValuedFunctors.
 Require Import UniMath.CategoryTheory.HorizontalComposition.
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.FunctorCategory.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 Require Import UniMath.Foundations.Sets.
 Require Import UniMath.CategoryTheory.Epis.
 Require Import UniMath.CategoryTheory.EpiFacts.
-Require Import UniMath.CategoryTheory.limits.graphs.coequalizers.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Coequalizers.
 
 Require Import Modules.Prelims.lib.
 Require Import Modules.Prelims.FaithfulFibrationEqualizer.
@@ -50,9 +50,9 @@ Require Import Modules.Prelims.BinCoproductComplements.
 Require Import Modules.Signatures.SignaturesColims.
 Require Import Modules.Signatures.SignatureCoproduct.
 
-Require Import UniMath.CategoryTheory.limits.coproducts.
-Require Import UniMath.CategoryTheory.limits.bincoproducts.
-Require Import UniMath.CategoryTheory.limits.pushouts.
+Require Import UniMath.CategoryTheory.Limits.Coproducts.
+Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
+Require Import UniMath.CategoryTheory.Limits.Pushouts.
 Require Import UniMath.CategoryTheory.Adjunctions.Core.
 
 Section TwoSig.
@@ -104,7 +104,7 @@ Proof.
   apply (model_equations_eq R o).
 Qed.
 
-Lemma two_signature_comp_Mor 
+Lemma two_signature_comp_Mor
   (x y z : signature_category) (f : signature_category ⟦ x, y ⟧) (g : signature_category ⟦ y, z ⟧)
   (xx : two_signature_disp_ob_mor x) (yy : two_signature_disp_ob_mor y) (zz : two_signature_disp_ob_mor z) :
   xx -->[ f] yy → yy -->[ g] zz → xx -->[ f · g] zz.
@@ -164,7 +164,7 @@ Definition TwoSignature_eqs (S : TwoSignature) : TwoSignature_index S -> equatio
 
 (** If thebase category has coequalizers, then the total two-sig category also *)
 Lemma TwoSignature_Coequalizers
-      (coeq : colimits.Colims_of_shape Coequalizer_graph  C)
+      (coeq : Colimits.Colims_of_shape Coequalizer_graph  C)
   : Coequalizers TwoSig_category.
 Proof.
   red.
@@ -195,8 +195,8 @@ Defined.
 Definition two_signature_coproduct_in
   {O : UU}
   (c : Coproducts O C)
-  (sigs : O → TwoSig_category) 
-  (i : O) : 
+  (sigs : O → TwoSig_category)
+  (i : O) :
   TwoSig_category ⟦ sigs i, two_signature_coproduct c sigs ⟧.
 Proof.
   use tpair.
@@ -206,7 +206,7 @@ Proof.
     apply (model_equations_eq R (i ,, o)).
 Defined.
 
-Lemma two_signature_is_coproduct 
+Lemma two_signature_is_coproduct
   {O : UU}
   (c : Coproducts O C)
   (sigs : O → TwoSig_category)  :
@@ -260,9 +260,9 @@ Proof.
   - apply two_signature_is_coproduct.
 Defined.
 
-Lemma TwoSignature_Pushouts 
+Lemma TwoSignature_Pushouts
       (b : BinCoproducts C)
-    (coeq : colimits.Colims_of_shape Coequalizer_graph  C)
+    (coeq : Colimits.Colims_of_shape Coequalizer_graph  C)
   : Pushouts  TwoSig_category.
 Proof.
   apply pushouts_from_coeq_bincoprod; revgoals.
@@ -291,7 +291,7 @@ Qed.
 
 (** A 1-signature S induces a 2-signature consisting of no equation *)
 Definition OneSig_to_TwoSig (S : signature C) : TwoSignature := (S ,, ∅ ,, empty_rect _).
-    
+
 (** This induces a left adjoint to the forgetful functor *)
 Lemma universal_OneSig_to_TwoSig (S : signature C) :
   is_universal_arrow_to (pr1_category two_signature_disp) S (OneSig_to_TwoSig S) (identity _).
@@ -336,7 +336,7 @@ Defined.
 Local Notation MONAD := (Monad C).
 Local Notation PRE_MONAD := (category_Monad C).
 (* Local Notation BMOD := (bmod_disp C C). *)
-  
+
 
 (* Signatures are display functors over the identity *)
 Local Notation PRECAT_SIGNATURE  := (@signature_precategory C).
@@ -489,7 +489,7 @@ Proof.
     (** reflexivity thanks to primitive projections *)
     apply idpath.
 Defined.
-      
+
 
 Definition TwoMod_OneMod_is_right_adjoint : is_right_adjoint TwoMod_OneMod_functor :=
   right_adjoint_left_from_partial (X := MOD1) _ _ _ universal_OneMod_TwoMod.
@@ -546,10 +546,10 @@ Proof.
       apply idpath.
   Defined.
 
-Definition catiso_modelcat_eq (S : TwoSignature) : 
+Definition catiso_modelcat_eq (S : TwoSignature) :
   catiso (two_model_disp [{S}]) (category_model_equations (TwoSignature_eqs S)) :=
    (make_functor _ (fib_to_dir_is_functor S) ,, (λ x y : (FIBER_CAT S), weqproperty (FSmor x y)),, idisweq _).
-     
+
 End TwoSig.
 
 
diff --git a/Modules/SoftEquations/Equation.v b/Modules/SoftEquations/Equation.v
index 3586ad1..d9a29af 100644
--- a/Modules/SoftEquations/Equation.v
+++ b/Modules/SoftEquations/Equation.v
@@ -16,7 +16,7 @@
 Require Import UniMath.Foundations.PartD.
 Require Import UniMath.Foundations.Propositions.
 Require Import UniMath.Foundations.Sets.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 Require Import UniMath.CategoryTheory.Monads.LModules.
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.FunctorCategory.
@@ -72,7 +72,7 @@ Section Equation.
     homset_property (category_LModule  _ _ ) _ _ _ _.
 
   Definition satisfies_equation_hp (e : equation) (R : REP) : hProp  :=
-    make_hProp _ (satisfies_equation_isaprop e R). 
+    make_hProp _ (satisfies_equation_isaprop e R).
 
   (** The proposition that a 1-model satisfies a family of equations: it must satisfy
       each of them *)
@@ -120,9 +120,9 @@ Definition po_equation
                     po_signature_over_mor f (halfeq1 e)  ,,
                     po_signature_over_mor f (halfeq2 e).
 
-Definition po_satisfies_equation  
+Definition po_satisfies_equation
            {C : category} {S1 S2 : signature C} (f : signature_Mor S1 S2)
-           (e : equation S1) 
+           (e : equation S1)
            (R : model _)
            (hR : satisfies_equation (po_equation f e) R) :
   satisfies_equation e (pb_rep f R) := hR.
diff --git a/Modules/SoftEquations/Examples/LCBetaEta.v b/Modules/SoftEquations/Examples/LCBetaEta.v
index a8dde6a..d446313 100644
--- a/Modules/SoftEquations/Examples/LCBetaEta.v
+++ b/Modules/SoftEquations/Examples/LCBetaEta.v
@@ -51,15 +51,15 @@ Some results:
 Require Import UniMath.Foundations.PartD.
 
 Require Import UniMath.CategoryTheory.Monads.Monads.
-Require Import UniMath.CategoryTheory.Monads.LModules. 
+Require Import UniMath.CategoryTheory.Monads.LModules.
 Require Import UniMath.CategoryTheory.SetValuedFunctors.
 Require Import UniMath.CategoryTheory.HorizontalComposition.
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.FunctorCategory.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 Require Import UniMath.CategoryTheory.Subcategory.Core.
 Require Import UniMath.CategoryTheory.Subcategory.Full.
-Require Import UniMath.CategoryTheory.limits.bincoproducts.
+Require Import UniMath.CategoryTheory.Limits.BinCoproducts.
 Require Import UniMath.CategoryTheory.catiso.
 
 Require Import UniMath.Foundations.Sets.
@@ -93,10 +93,10 @@ Require Import Modules.SoftEquations.quotientequation.
 Require Import Modules.Prelims.BinProductComplements.
 Require Import Modules.Prelims.CoproductsComplements.
 
-Require Import UniMath.CategoryTheory.limits.initial.
-Require Import UniMath.CategoryTheory.limits.binproducts.
-Require Import UniMath.CategoryTheory.limits.coproducts.
-Require Import UniMath.CategoryTheory.limits.terminal.
+Require Import UniMath.CategoryTheory.Limits.Initial.
+Require Import UniMath.CategoryTheory.Limits.BinProducts.
+Require Import UniMath.CategoryTheory.Limits.Coproducts.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
 Require Import Modules.SoftEquations.SignatureOverBinproducts.
 Require Import Modules.SoftEquations.BindingSig.
 
@@ -104,8 +104,8 @@ Require Import Modules.SoftEquations.BindingSig.
 
 Local Notation θ := (tautological_signature).
 Local Notation τ := (tautological_LModule).
-Local Notation BPO := (limits.binproducts.BinProductObject _ ).
-Local Notation CPO := (limits.coproducts.CoproductObject _ _ ).
+Local Notation BPO := (Limits.BinProducts.BinProductObject _ ).
+Local Notation CPO := (Limits.Coproducts.CoproductObject _ _ ).
 Local Notation ι := (sig_over_from_sig _).
 
 
@@ -124,7 +124,7 @@ Local Infix "××" :=  (signature_BinProduct (cpC := bpC)  ) (at level 20).
 
 
 (** The LC algebraic signature is to Θ' + Θ × Θ
-The binding signature [LamSig] is defined in UniMath as [1], [0,0] 
+The binding signature [LamSig] is defined in UniMath as [1], [0,0]
  *)
 Definition LamOneSig := binding_to_one_sig bpC bcpC cpC TC LamSig.
 
@@ -139,13 +139,13 @@ Lemma source_app_iso :
       (arity_to_one_sig bpC bcpC TC (BindingSigMap LamSig appIdx))
       (BPO (θ ×× θ)).
 Proof.
-  eapply iso_comp; [ use binprod_sigs_har_iso|use BinProduct_pw_iso]; cbn ; apply tauto_sigs_har_iso. 
+  eapply iso_comp; [ use binprod_sigs_har_iso|use BinProduct_pw_iso]; cbn ; apply tauto_sigs_har_iso.
 Defined.
 
 (** The next lemmas show that the arity of abs is isomorphic to θ' *)
 Definition arity_abs := arity_to_one_sig bpC bcpC TC (BindingSigMap LamSig absIdx).
 
-Lemma arity_abs_mod_eq_mult R c : 
+Lemma arity_abs_mod_eq_mult R c :
   (ModulesFromSignatures.lift_lm_mult (Arity_to_Signature bpC bcpC TC (BindingSigMap LamSig absIdx)) R (τ R) :
   nat_trans _ _) c =
   (nat_trans_comp (whiskering.post_whisker (Derivative.deriv_dist TC bcpC R) (θ R))
@@ -158,7 +158,7 @@ Qed.
 
 Lemma arity_abs_eq (R S : Monad C) (f : Monad_Mor R S) (c : C) :
   (signature_deriv_on_morphisms bcpC TC θ R S f) c =
-  ((lift_lmodule_mor (Arity_to_Signature bpC bcpC TC (BindingSigMap LamSig absIdx)) R (monad_mor_to_lmodule f) c) · 
+  ((lift_lmodule_mor (Arity_to_Signature bpC bcpC TC (BindingSigMap LamSig absIdx)) R (monad_mor_to_lmodule f) c) ·
 
    (lift_pb_LModule (Arity_to_Signature bpC bcpC TC (BindingSigMap LamSig absIdx)) f) c).
 Proof.
@@ -179,7 +179,7 @@ Proof.
 Defined.
 
 
-    
+
 
 (**
 The first beta half-equation:
@@ -189,7 +189,7 @@ The first beta half-equation:
 θ' × θ -------> θ × θ ---> θ
 >>>
 *)
-Lemma abs_app_halfeq : signature_over_Mor (binding_to_one_sig bpC bcpC cpC TC LamSig) 
+Lemma abs_app_halfeq : signature_over_Mor (binding_to_one_sig bpC bcpC cpC TC LamSig)
                                           (ι (BPO ((∂ θ) ×× θ)))
                                           (ι θ).
 Proof.
@@ -200,7 +200,7 @@ Proof.
       apply (inv_from_iso (C := signature_category)).
       apply source_app_iso.
     + eapply compose;[|apply  signature_over_BinProducts_commutes_sig].
-      eapply (compose );[apply inv_from_iso, signature_over_BinProducts_commutes_sig|]. 
+      eapply (compose );[apply inv_from_iso, signature_over_BinProducts_commutes_sig|].
       apply BinProductOfArrows.
       * eapply compose; [apply sig_sig_over_mor, (inv_from_iso (C := signature_category)), source_abs_iso|].
         apply bindingSig_op_to_sig_mor.
@@ -214,7 +214,7 @@ The first eta half-equation:
 θ  -----> θ' -----> θ
 >>>
 *)
-Definition in_abs_halfeq : signature_over_Mor (binding_to_one_sig bpC bcpC cpC TC LamSig) 
+Definition in_abs_halfeq : signature_over_Mor (binding_to_one_sig bpC bcpC cpC TC LamSig)
                                           (ι θ)
                                           (ι θ).
 Proof.
@@ -229,9 +229,9 @@ Defined.
 End BindingSigOp.
 
 
-Local Notation BP := (BinProductsHSET : limits.binproducts.BinProducts SET).
-Local Notation BCP := (BinCoproductsHSET : limits.bincoproducts.BinCoproducts SET).
-Local Notation T := (TerminalHSET : limits.terminal.Terminal SET).
+Local Notation BP := (BinProductsHSET : Limits.BinProducts.BinProducts SET).
+Local Notation BCP := (BinCoproductsHSET : Limits.BinCoproducts.BinCoproducts SET).
+Local Notation T := (TerminalHSET : Limits.Terminal.Terminal SET).
 Local Notation CP := (CoproductsHSET).
 Local Notation "∂" := (signature_deriv BCP T).
 
@@ -312,9 +312,9 @@ Definition LCBetaEta : Initial
   (category_model_equations
                     (fun o =>
                        soft_equation_from_elementary_equation
-                         LamOneSigHSET_epiSig 
+                         LamOneSigHSET_epiSig
                          (beta_eta_equations o))
-                 ). 
+                 ).
 Proof.
   use  elementary_equations_on_alg_preserve_initiality.
 Defined.
diff --git a/Modules/SoftEquations/Modularity.v b/Modules/SoftEquations/Modularity.v
index 7dc4ca2..0befb84 100644
--- a/Modules/SoftEquations/Modularity.v
+++ b/Modules/SoftEquations/Modularity.v
@@ -4,7 +4,7 @@
 Suppose we have the following pushout diagram in the category of 2-signatures:
 <<<
                 f1
-       a0 ------------>  a1 
+       a0 ------------>  a1
        |                 |
        |                 |
    f2  |                 | g2
@@ -12,8 +12,8 @@ Suppose we have the following pushout diagram in the category of 2-signatures:
        |                 |
        |                 |
        V                 V
-       a2 ------------>  a' 
-                 g1 
+       a2 ------------>  a'
+                 g1
 >>>
 
 such that a0, a1, a2 and a' are effective with initial models
@@ -21,7 +21,7 @@ R0, R1, R2 and R'. Then, above this pushout there is a pushout square in the
 large category of models:
 <<<
                 ff1
-       R0 ------------>  R1 
+       R0 ------------>  R1
        |                 |
        |                 |
   ff2  |                 | gg2
@@ -29,8 +29,8 @@ large category of models:
        |                 |
        |                 |
        V                 V
-       R2 ------------>  R' 
-                 gg1 
+       R2 ------------>  R'
+                 gg1
 >>>
 
 
@@ -43,8 +43,8 @@ Require Import UniMath.Foundations.Sets.
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.FunctorCategory.
 
-Require Import UniMath.CategoryTheory.limits.pushouts.
-Require Import UniMath.CategoryTheory.limits.initial.
+Require Import UniMath.CategoryTheory.Limits.Pushouts.
+Require Import UniMath.CategoryTheory.Limits.Initial.
 
 Require Import UniMath.CategoryTheory.DisplayedCats.Core.
 Require Import UniMath.CategoryTheory.DisplayedCats.Fiber.
@@ -70,10 +70,10 @@ Definition pushout_in_big_rep
 
            (** and syntaxes for each of the signatures *)
            {R0 : two_model_disp a0} {R1 : two_model_disp a1} {R2 : two_model_disp a2} {R' : two_model_disp a'}
-           (repr_R0 : isInitial  (fiber_category _ _) R0)  
+           (repr_R0 : isInitial  (fiber_category _ _) R0)
            (repr_R1 : isInitial  (fiber_category _ _) R1)
            (repr_R2 : isInitial  (fiber_category _ _) R2)
-           (repr_R' : isInitial  (fiber_category _ _) R') 
+           (repr_R' : isInitial  (fiber_category _ _) R')
            (** Then the initial morphisms induce a pushout in the total category *)
   :  isPushout (TT (ι f1))
                (TT (ι f2))
diff --git a/Modules/SoftEquations/SignatureOver.v b/Modules/SoftEquations/SignatureOver.v
index 0fee0a2..5f73291 100644
--- a/Modules/SoftEquations/SignatureOver.v
+++ b/Modules/SoftEquations/SignatureOver.v
@@ -22,7 +22,7 @@ Require Import UniMath.Foundations.Sets.
 
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.FunctorCategory.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 Require Import UniMath.CategoryTheory.Epis.
 Require Import UniMath.CategoryTheory.EpiFacts.
 
@@ -84,14 +84,14 @@ Definition signature_over_on_objects (a : signature_over_data) : ∏ (R : REP),
 
 Coercion signature_over_on_objects : signature_over_data >-> Funclass.
 
-Definition signature_over_on_morphisms  (F : signature_over_data) {R S : REP} 
-  : ∏ (f:  R →→ S), LModule_Mor _ (F R) (pb_LModule f (F S)) 
+Definition signature_over_on_morphisms  (F : signature_over_data) {R S : REP}
+  : ∏ (f:  R →→ S), LModule_Mor _ (F R) (pb_LModule f (F S))
   := pr2 F R S.
 
 (** Notation for the map 1-model morphism -> module morphism *)
 Notation "# F" := (signature_over_on_morphisms F) (at level 3) : signature_over_scope.
 
-Definition signature_over_on_morphisms_cancel_pw (F : signature_over_data) {R S : REP} 
+Definition signature_over_on_morphisms_cancel_pw (F : signature_over_data) {R S : REP}
            {u v : R →→ S}  (e : u = v) x : (# F u)%sigo x = (#F v)%sigo x.
   induction e.
   apply idpath.
@@ -106,8 +106,8 @@ Definition signature_over_idax  (F : signature_over_data) :=
 (** Statment that the raw data preserves composition *)
 Definition signature_over_compax  (F : signature_over_data) :=
   ∏ R S T  (f : R →→ S) (g : S →→ T) ,
-    (#F  (f ;; g))%sigo 
-      = 
+    (#F  (f ;; g))%sigo
+      =
       (((# F f)%sigo :(F R : bmod_disp C C (R : Monad _)) -->[(f : Monad_Mor  _ _)] F S) ;; (#F g)%sigo)%mor_disp.
 
 (** Raw data yields a Sig-module if it satisfies the previous functoriality conditions *)
@@ -140,7 +140,7 @@ Defined.
 Local Notation OSig := sig_over_data_from_sig.
 
 (** Functoriality conditions for a Sig-module induced by a signatre *)
-Lemma is_sig_over_from_sig (sig : signature C) : is_signature_over (OSig sig). 
+Lemma is_sig_over_from_sig (sig : signature C) : is_signature_over (OSig sig).
   split.
   - use signature_id.
   - red.
@@ -162,11 +162,11 @@ Definition signature_over_id (F : signature_over) :
   := pr1 (pr2 F).
 
 (** A Sig-module preserves composition *)
-Definition signature_over_comp (F : signature_over) {R S T : REP} 
+Definition signature_over_comp (F : signature_over) {R S T : REP}
            (f : rep_fiber_mor R S) (g : rep_fiber_mor S T)
-  : 
-    (#F  (f ;; g))%sigo 
-      = 
+  :
+    (#F  (f ;; g))%sigo
+      =
       (((# F f)%sigo :(F R : bmod_disp C C (R : Monad _)) -->[(f : Monad_Mor  _ _)] F S) ;; (#F g)%sigo)%mor_disp
   := pr2 (pr2 F) _ _ _ _ _ .
 
@@ -192,11 +192,11 @@ t_R |               | t_S
 >>>
 *)
 Definition is_signature_over_Mor (F F' : signature_over_data)
-           (t : ∏ R : REP, LModule_Mor R (F R)  (F' R)) 
+           (t : ∏ R : REP, LModule_Mor R (F R)  (F' R))
   :=
     ∏ (R S : REP)(f : rep_fiber_mor R S),
     (((# F)%sigo f :   nat_trans _ _) : [_,_]⟦_,_⟧) ·
-                                                  (t S : nat_trans _ _) 
+                                                  (t S : nat_trans _ _)
     =
     ((t R : nat_trans _ _) : [_,_]⟦_,_⟧) · ((#F')%sigo f : nat_trans _ _).
 
@@ -215,7 +215,7 @@ Definition signature_over_Mor  (F F' : signature_over_data) : UU := ∑ X, is_si
 Definition mkSignature_over_Mor {F F' : signature_over_data} X
            (hX : is_signature_over_Mor F F' X) : signature_over_Mor F F' :=
   X ,, hX.
-                            
+
 (** Notation for Sig-module morphisms *)
 Local Notation "F ⟹ G" := (signature_over_Mor F G) (at level 39) : signature_over_scope.
 
@@ -236,16 +236,16 @@ Coercion signature_over_Mor_data : signature_over_Mor >-> Funclass.
 Definition signature_over_Mor_ax {F F' : signature_over} (a : (F ⟹ F')%sigo)
   : ∏ {R S : REP}(f : rep_fiber_mor R S),
     (((# F)%sigo f :   nat_trans _ _) : [_,_]⟦_,_⟧) ·
-                                                  (a S : nat_trans _ _) 
+                                                  (a S : nat_trans _ _)
     =
     ((a R : nat_trans _ _) : [_,_]⟦_,_⟧) · ((#F')%sigo f : nat_trans _ _)
   := pr2 a.
 
 (** A Sig-module morphism is natural (pointwise version of the naturality diagram) *)
-Lemma signature_over_Mor_ax_pw {F F' : signature_over} (a : (F ⟹ F')%sigo) 
+Lemma signature_over_Mor_ax_pw {F F' : signature_over} (a : (F ⟹ F')%sigo)
   : ∏ {R S : REP}(f : rep_fiber_mor R S) x,
     (((# F)%sigo f :   nat_trans _ _) x) ·
-                                       ((a S : nat_trans _ _) x) 
+                                       ((a S : nat_trans _ _) x)
     =
     ((a R : nat_trans _ _)  x) · (((#F')%sigo f : nat_trans _ _) x).
 Proof.
@@ -285,7 +285,7 @@ Definition signature_over_Mor_id (F : signature_over_data) : signature_over_Mor
     tpair _ _ (is_signature_over_Mor_id F).
 
 (** Composition of two Sig-module morphisms yields a Sig-module morphism *)
-Lemma is_signature_over_Mor_comp {F G H : signature_over} (a : signature_over_Mor F G) (b : signature_over_Mor G H) 
+Lemma is_signature_over_Mor_comp {F G H : signature_over} (a : signature_over_Mor F G) (b : signature_over_Mor G H)
   : is_signature_over_Mor F H (fun R  => (a R : category_LModule _ _ ⟦_,_⟧ ) · b R).
 Proof.
   intros ? ? ?.
@@ -303,7 +303,7 @@ Proof.
 Qed.
 (** Composition of Sig-module morphisms *)
 Definition signature_over_Mor_comp {F G H : signature_over} (a : signature_over_Mor F G) (b : signature_over_Mor G H)
-  : signature_over_Mor F H 
+  : signature_over_Mor F H
   := tpair _ _ (is_signature_over_Mor_comp a b).
 
 (** Intermediate data to build the category of Sig-modules *)
@@ -325,7 +325,7 @@ Proof.
   apply make_is_precategory_one_assoc; simpl; intros.
   - unfold identity.
     simpl.
-    apply signature_over_Mor_eq. 
+    apply signature_over_Mor_eq.
     intro x; simpl.
     apply (id_left (C:=category_LModule _ _)).
   - apply signature_over_Mor_eq.
@@ -337,7 +337,7 @@ Proof.
 Qed.
 
 (** The precategory of Sig-modules *)
-Definition signature_over_precategory : precategory := 
+Definition signature_over_precategory : precategory :=
   tpair (fun C => is_precategory C)
         (signature_over_precategory_data)
         (is_precategory_signature_over_precategory_data).
@@ -412,7 +412,7 @@ Section PushoutOverSig.
       apply ((# SS1 (pb_rep_mor f g ))%sigo).
   Defined.
 
-  Lemma  po_is_signature_over 
+  Lemma  po_is_signature_over
         {C} {S1 S2 : signature C} (f : signature_Mor S1 S2) (SS1 : signature_over S1)
   : is_signature_over _ (po_signature_over_data f SS1).
   Proof.
@@ -435,14 +435,14 @@ Section PushoutOverSig.
       apply idpath.
   Defined.
 
-  Definition  po_signature_over 
+  Definition  po_signature_over
          {C} {S1 S2 : signature C} (f : signature_Mor S1 S2) (SS1 : signature_over S1) :
     signature_over S2 := _ ,, po_is_signature_over f SS1.
 
   Definition  po_signature_over_mor
               {C} {S1 S2 : signature C} (f : signature_Mor S1 S2) {SS1 SS1' : signature_over S1}
               (ff1 : signature_over_Mor _ SS1 SS1')
-    :  signature_over_Mor _ 
+    :  signature_over_Mor _
                              (po_signature_over f SS1)(po_signature_over f SS1')
      :=
      mkSignature_over_Mor _ (F := po_signature_over f SS1)
diff --git a/Modules/SoftEquations/SignatureOverAsFiber.v b/Modules/SoftEquations/SignatureOverAsFiber.v
index 01bae3f..d1d2339 100644
--- a/Modules/SoftEquations/SignatureOverAsFiber.v
+++ b/Modules/SoftEquations/SignatureOverAsFiber.v
@@ -8,7 +8,7 @@ Mathematically, a soft Σ-module is a functor from the category
 of models of Σ to the total category of modules, preserving the underlying monad.
 The source category is the fiber over Σ of the displayed category of representations.
 Morphisms are displayed morphism over the identity signature morphism. Hence composition
-does not work well, because the composition of two morphisms  x ->[id] y and y ->[id] z 
+does not work well, because the composition of two morphisms  x ->[id] y and y ->[id] z
 yield a morphism x ->[id ; id] z
 
 Inspired by Signature.v
@@ -23,7 +23,7 @@ Require Import UniMath.Foundations.Sets.
 
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.FunctorCategory.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 
 Require Import UniMath.CategoryTheory.Epis.
 Require Import UniMath.CategoryTheory.EpiFacts.
@@ -79,8 +79,8 @@ Definition signature_over_on_objects (a : signature_over_data) : ∏ (R : REP),
 
 Coercion signature_over_on_objects : signature_over_data >-> Funclass.
 
-Definition signature_over_on_morphisms  (F : signature_over_data) {R S : REP} 
-  : ∏ (f:  R →→ S), LModule_Mor _ (F R) (pb_LModule f (F S)) 
+Definition signature_over_on_morphisms  (F : signature_over_data) {R S : REP}
+  : ∏ (f:  R →→ S), LModule_Mor _ (F R) (pb_LModule f (F S))
   := pr2 F R S.
 
 Notation "# F" := (signature_over_on_morphisms F) (at level 3) : signature_over_scope.
@@ -95,8 +95,8 @@ Definition signature_over_idax  (F : signature_over_data) :=
     than in module because types would be incompatible because of the transport *)
 Definition signature_over_compax  (F : signature_over_data) :=
   ∏ R S T  (f : R →→ S) (g : S →→ T) ,
-  (#F  (f ;; g) :  nat_trans _ _)%sigo 
-  = 
+  (#F  (f ;; g) :  nat_trans _ _)%sigo
+  =
   (((# F f)%sigo :(F R : bmod_disp C C (R : Monad _)) -->[(f : Monad_Mor  _ _)] F S) ;; (#F g)%sigo :
      LModule_Mor _ _ _
   )%mor_disp.
@@ -120,7 +120,7 @@ Coercion signature_over_data_from_signature_over : signature_over >-> signature_
 Notation Θ := tautological_LModule.
 
 Definition tautological_signature_over_on_objects : ∏ (R : REP), LModule R C := Θ.
-Definition tautological_signature_over_on_morphisms : 
+Definition tautological_signature_over_on_morphisms :
   ∏ (R S : REP) (f : R →→ S), LModule_Mor _ (Θ R) (pb_LModule f (Θ S)) :=
   @monad_mor_to_lmodule C.
 
@@ -154,11 +154,11 @@ Definition signature_over_id (F : signature_over) :
   ((# F (rep_id _ R)))%sigo x  = identity  _
   := pr1 (pr2 F).
 
-Definition signature_over_comp (F : signature_over) {R S T : REP} 
+Definition signature_over_comp (F : signature_over) {R S T : REP}
            (f : R →→ S) (g : S →→  T)
            :
-  (#F  (f ;; g) :  nat_trans _ _)%sigo 
-  = 
+  (#F  (f ;; g) :  nat_trans _ _)%sigo
+  =
   (((# F f)%sigo :(F R : bmod_disp C C (R : Monad _)) -->[(f : Monad_Mor  _ _)] F S) ;; (#F g)%sigo :
      LModule_Mor _ _ _
   )%mor_disp
diff --git a/Modules/SoftEquations/SignatureOverBinproducts.v b/Modules/SoftEquations/SignatureOverBinproducts.v
index 1d60ab5..b903f13 100644
--- a/Modules/SoftEquations/SignatureOverBinproducts.v
+++ b/Modules/SoftEquations/SignatureOverBinproducts.v
@@ -21,8 +21,8 @@ Require Import UniMath.CategoryTheory.Monads.LModules.
 Require Import UniMath.CategoryTheory.DisplayedCats.Core.
 Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
 
-Require Import UniMath.CategoryTheory.limits.binproducts.
-Require Import UniMath.CategoryTheory.limits.graphs.colimits.
+Require Import UniMath.CategoryTheory.Limits.BinProducts.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
 
 Require Import Modules.Prelims.lib.
 
@@ -119,11 +119,11 @@ Section Binprod.
         rewrite id_right.
         apply idpath.
   Qed.
-      
+
   Definition signature_over_binProd : signature_over Sig := _ ,, signature_over_binProd_is_signature_over.
 
-  Lemma signature_over_binProductPr1_laws : 
-    is_signature_over_Mor _ signature_over_binProd a 
+  Lemma signature_over_binProductPr1_laws :
+    is_signature_over_Mor _ signature_over_binProd a
                  (fun R => BinProductPr1  _  (cpLM R (a R) (b R)   )).
   Proof.
     intros R S f.
@@ -137,8 +137,8 @@ Section Binprod.
     use (BinProductOfArrowsPr1 _  CC).
   Qed.
 
-  Lemma signature_over_binProductPr2_laws : 
-    is_signature_over_Mor _ signature_over_binProd b 
+  Lemma signature_over_binProductPr2_laws :
+    is_signature_over_Mor _ signature_over_binProd b
                  (fun R => BinProductPr2  _  (cpLM R (a R) (b R)   )).
   Proof.
     intros R S f.
@@ -152,10 +152,10 @@ Section Binprod.
     use (BinProductOfArrowsPr2 _  CC).
   Qed.
 
-  Definition signature_over_binProductPr1 : 
+  Definition signature_over_binProductPr1 :
     signature_over_Mor  _ signature_over_binProd a := _ ,, signature_over_binProductPr1_laws .
 
-  Definition signature_over_binProductPr2 : 
+  Definition signature_over_binProductPr2 :
     signature_over_Mor  _ signature_over_binProd b := _ ,, signature_over_binProductPr2_laws .
 
   (* TODO : move to Signature_Over *)
@@ -163,7 +163,7 @@ Section Binprod.
              (cb : signature_over_Mor _ c b)
     :
     is_signature_over_Mor
-      _ c signature_over_binProd 
+      _ c signature_over_binProd
       (fun R => BinProductArrow  _  (cpLM R (a R) (b R)) (ca R) (cb R))  .
   Proof.
     intros R S f.
@@ -197,7 +197,7 @@ Section Binprod.
   Qed.
 
   Definition signature_over_binProductArrow {c : signature_over _} (ca :  signature_over_Mor _ c a )
-             (cb : signature_over_Mor _ c b) : 
+             (cb : signature_over_Mor _ c b) :
     signature_over_Mor _ c signature_over_binProd  := _ ,, signature_over_binProductArrow_laws ca cb.
 
   Lemma signature_over_isBinProduct : isBinProduct (signature_over_category _)  _ _ _
@@ -303,14 +303,14 @@ Definition signature_over_BinProducts
             : BinProducts (signature_over_category (C := C) Sig) :=
    signature_over_BinProduct (cpC := cpC) Sig.
 
-Definition signature_over_BinProducts_commutes_sig 
+Definition signature_over_BinProducts_commutes_sig
            {C : category}
            (cpC : BinProducts C) (Sig : signature C)
            (a b : signature C) :
   (* iso (C := signature_over_category Sig) *)
-   iso (C := signature_over_category Sig) 
+   iso (C := signature_over_category Sig)
       (BPO (signature_over_BinProducts cpC _ (ι a) (ι b))) (ι (BPO (signature_BinProducts cpC a b))).
-      
+
 Proof.
   use signature_over_S1_S2_iso.
 Defined.
diff --git a/Modules/SoftEquations/SignatureOverDerivation.v b/Modules/SoftEquations/SignatureOverDerivation.v
index 944e75b..4949377 100644
--- a/Modules/SoftEquations/SignatureOverDerivation.v
+++ b/Modules/SoftEquations/SignatureOverDerivation.v
@@ -15,9 +15,9 @@ Require Import UniMath.CategoryTheory.Monads.Derivative.
 Require Import UniMath.CategoryTheory.DisplayedCats.Core.
 Require Import UniMath.CategoryTheory.DisplayedCats.Constructions.
 
-Require Import UniMath.CategoryTheory.limits.coproducts.
-Require Import UniMath.CategoryTheory.limits.graphs.colimits.
-Require Import UniMath.CategoryTheory.limits.terminal.
+Require Import UniMath.CategoryTheory.Limits.Coproducts.
+Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits.
+Require Import UniMath.CategoryTheory.Limits.Terminal.
 
 Require Import Modules.Prelims.lib.
 
@@ -31,8 +31,8 @@ Require Import Modules.SoftEquations.SignatureOver.
 Section DAr.
 
   Context {C : category}
-          (bcpC : limits.bincoproducts.BinCoproducts C)
-          (CT : limits.terminal.Terminal C).
+          (bcpC : Limits.BinCoproducts.BinCoproducts C)
+          (CT : Limits.Terminal.Terminal C).
 Local Notation "∂" := (LModule_deriv_functor (TerminalObject CT) bcpC
                                              _).
 
diff --git a/Modules/SoftEquations/Summary.v b/Modules/SoftEquations/Summary.v
index 0be9fdb..827e02e 100644
--- a/Modules/SoftEquations/Summary.v
+++ b/Modules/SoftEquations/Summary.v
@@ -7,13 +7,13 @@ Tip: The Coq command [About ident] prints where the ident was defined
 Require Import UniMath.Foundations.PartD.
 
 Require Import UniMath.CategoryTheory.Monads.Monads.
-Require Import UniMath.CategoryTheory.Monads.LModules. 
+Require Import UniMath.CategoryTheory.Monads.LModules.
 Require Import UniMath.CategoryTheory.Monads.Derivative.
 Require Import UniMath.CategoryTheory.SetValuedFunctors.
 Require Import UniMath.CategoryTheory.HorizontalComposition.
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.FunctorCategory.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 
 Require Import UniMath.Foundations.Sets.
 Require Import UniMath.CategoryTheory.Epis.
@@ -35,7 +35,7 @@ Require Import Modules.SoftEquations.Equation.
 Require Import Modules.SoftEquations.quotientrepslice.
 Require Import Modules.SoftEquations.quotientequation.
 
-Require Import UniMath.CategoryTheory.limits.initial.
+Require Import UniMath.CategoryTheory.Limits.Initial.
 Require Import Modules.SoftEquations.AdjunctionEquationRep.
 
 Require Import UniMath.CategoryTheory.DisplayedCats.Core.
@@ -55,7 +55,7 @@ Local Notation MODULE R := (LModule R SET).
 (**
 The command:
 
-Check (x ::= y) 
+Check (x ::= y)
 
 succeeds if and only if [x] is convertible to [y]
 
@@ -232,9 +232,9 @@ Check (∏ (S : SIGNATURE)
                    isEpi (C := [SET, SET]) (# F f : nat_trans _ _)%sigo
        ).
 
-(** Definition of a soft-over signature (SoftEquations/quotientequation.v) 
+(** Definition of a soft-over signature (SoftEquations/quotientequation.v)
 
-It is a signature Σ such that for any model R, and any family of model morphisms 
+It is a signature Σ such that for any model R, and any family of model morphisms
 (f_j : R --> d_j), the following diagram can be completed in the category
 of natural transformations:
 
@@ -268,7 +268,7 @@ Check (∏ (S : SIGNATURE)
             X (x y : (F R X : hSet))
             (pi := projR_rep S isEpi_sig R_epi SR_epi d f),
           (∏ j, (# F (f j))%sigo X x  = (# F (f j))%sigo X y )
-          -> (# F pi X x)%sigo = 
+          -> (# F pi X x)%sigo =
             (# F pi X y)%sigo  )
        ).
 
@@ -320,14 +320,14 @@ Check (∏ (S : SIGNATURE)
          (** but not that *)
          epiSig
          (e : elementary_equation),
-       (soft_equation_from_elementary_equation epiSig  e  : soft_equation _ 
+       (soft_equation_from_elementary_equation epiSig  e  : soft_equation _
        ) ::=
-         mk_soft_equation epiSig 
+         mk_soft_equation epiSig
                           (half_elem_eqs e)  (source_elem_epiSig e)
                           (isSoft_finite_deriv_tauto epiSig  (target_elem_eq e))).
 
 
-(** 
+(**
 Definition of the category of 2-models of a 1-signature with a family of equation.
 
 It is the full subcategory of 1-models satisfying all the equations
@@ -366,7 +366,7 @@ Check (∏ (S : SIGNATURE)
                          (satisfies_all_equations_hp e)).
 
 
-(** *********************** 
+(** ***********************
 
 Our main result : if a 1-signature Σ generates a syntax, then the 2-signature over Σ
 consisting of any family of soft equations over Σ also generates a syntax
@@ -374,7 +374,7 @@ consisting of any family of soft equations over Σ also generates a syntax
 
 *)
 Check (@soft_equations_preserve_initiality :
-         ∏ 
+         ∏
            (Sig : SIGNATURE)
            (** S is an epi-signature *)
            (epiSig : sig_preservesNatEpiMonad Sig)
@@ -385,7 +385,7 @@ Check (@soft_equations_preserve_initiality :
            (** this is implied by the axiom of choice *)
          preserves_Epi (InitialObject R : model Sig) ->
          preserves_Epi (Sig (InitialObject R : model Sig)) ->
-         
+
         (** .. then the category of 2-models has an initial object *)
          Initial (category_model_equations eq)).
 
@@ -393,7 +393,7 @@ Check (@soft_equations_preserve_initiality :
 
 (** As a corrolary, the case of a family of elementary equations *)
 Check (@elementary_equations_preserve_initiality :
-         ∏ 
+         ∏
            (Sig : SIGNATURE)
            (** (1) The 1-signature must be an epi-signature
             *)
@@ -429,7 +429,7 @@ any model preserves epis, , we can prove that
 the forgetful functor from 2-models (of a fixed 2-signature)
    to 1-models has a left adjoint *)
 Check (@ModEq_Mod_is_right_adjoint :
-         ∏ 
+         ∏
            (Sig : SIGNATURE)
            (** (1) S is an epi-signature *)
            (epiSig : sig_preservesNatEpiMonad Sig)
@@ -446,7 +446,7 @@ Check (@ModEq_Mod_is_right_adjoint :
 Note that an epimorphic monad morphism may not be epimorphic as a natural transformation.
 
 A natural transformation is epimorphic if and only if it is pointwise epimorphic.
-Thus, Hypotheses (2) and (3) are implied by the axiom of choice (because 
+Thus, Hypotheses (2) and (3) are implied by the axiom of choice (because
 any epimorphism has a section). Hypothesis (1) does not seem to be implied
 by the axiom of choice. Note that even with the axiom of choice, there are some
 epimorphic natural transformations which don't have a retract
@@ -465,13 +465,13 @@ completion of the following diagram (so that the canonical projection π is a mo
          π π |           | π
              v           v
             R' R'        R'
-                  
+
 >>
 where R' is the quotient monad. This definition requires that π π = R' π ∘ π R = π R' ∘ R π
 is an epimorphism, and this is implied by R π being an epi. Hence the requirement that R preserves epis
 (since π is indeed an epi, as a canonical projection)
 
-- to show that Σ_R' preserves epi in when showing that 
+- to show that Σ_R' preserves epi in when showing that
     the Σ-action of the quotient monad is a module morphism (see diagram (Act) below)
 
 
@@ -483,15 +483,15 @@ is an epimorphism, and this is implied by R π being an epi. Hence the requireme
 <<
             Σ_π
      Σ_R -----------> Σ_R'
-     |                 
-     |                 
-  τ_R|                 
-     |                 
-     V                 
+     |
+     |
+  τ_R|
+     |
+     V
      R ------------->  R'
            π
 >>
-where R' is the quotient monad. This definition requires that Σ π 
+where R' is the quotient monad. This definition requires that Σ π
 is an epimorphism, hence the requirement that Σ sends epimorphic natural transformations
 to epimorphisms (π is indeed an epimorphic natural transformation, as a canonical projection)
 
@@ -502,7 +502,7 @@ to epimorphisms (π is indeed an epimorphic natural transformation, as a canonic
   case of the monad R .
   Indeed, I need to show that the following diagram commutes:
 <<
-                          
+
      Σ_R' R' -----------> Σ_R'
         |                 |
         |                 |
diff --git a/Modules/SoftEquations/quotientequation.v b/Modules/SoftEquations/quotientequation.v
index 959152a..c2c7f6b 100644
--- a/Modules/SoftEquations/quotientequation.v
+++ b/Modules/SoftEquations/quotientequation.v
@@ -21,12 +21,12 @@ equations, then it is also the case for R'.
 Require Import UniMath.Foundations.PartD.
 
 Require Import UniMath.CategoryTheory.Monads.Monads.
-Require Import UniMath.CategoryTheory.Monads.LModules. 
+Require Import UniMath.CategoryTheory.Monads.LModules.
 Require Import UniMath.CategoryTheory.SetValuedFunctors.
 Require Import UniMath.CategoryTheory.HorizontalComposition.
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.FunctorCategory.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 
 Require Import UniMath.Foundations.Sets.
 Require Import UniMath.CategoryTheory.Epis.
@@ -64,7 +64,7 @@ Context (epiSig : sig_preservesNatEpiMonad Sig).
 
 (** Definition of a soft Sig-module
 
-It is a soft module Σ such that for any model R, and any family of model morphisms 
+It is a soft module Σ such that for any model R, and any family of model morphisms
 (f_j : R --> d_j), the following triangle can be completed in the category
 of natural transformations (from Σ(S) to Σ(d_j)):
 
@@ -89,7 +89,7 @@ where π : R -> S is the canonical projection (S is R quotiented by the family (
       (J : UU)(d : J -> (model Sig))(f : ∏ j, R →→ (d j))
       X (x y : (OSig R X : hSet)) (pi := projR_rep Sig epiSig  R_epi SigR_epi d f),
     (∏ j, (# OSig (f j))%sigo X x  = (# OSig (f j))%sigo X y )
-      -> (# OSig pi X x)%sigo = 
+      -> (# OSig pi X x)%sigo =
         (# OSig pi X y)%sigo  .
 
   Local Notation REP := (model Sig).
@@ -172,7 +172,7 @@ where π : R -> S is the canonical projection (S is R quotiented by the family (
   Context (R_epi : preserves_Epi R).
   Context (SigR_epi : preserves_Epi (Sig R)).
 
-  Context {J : UU} (d : J -> REP) 
+  Context {J : UU} (d : J -> REP)
             (ff : ∏ (j : J), R →→ (d j)).
 
   (** R' is the 1-model R quotiented by the following relation on R(X):
@@ -224,8 +224,8 @@ where π : R -> S is the canonical projection (S is R quotiented by the family (
   (** R' can be thus given the structure of a 2-model *)
   Definition R'_model_equations {O : UU} (e : O -> soft_equation)
     (deq : ∏ j, satisfies_all_equations_hp e (d j))
-    : model_equations e 
-    := R' ,, R'_satisfies_all_equations e deq. 
+    : model_equations e
+    := R' ,, R'_satisfies_all_equations e deq.
 
 
   (** ** Definition of elementary equations
@@ -235,11 +235,11 @@ where π : R -> S is the canonical projection (S is R quotiented by the family (
 
   (** An elementary equation
 
-The source is an epi-Sig-module and the target a finite derivative of the tautological signature 
+The source is an epi-Sig-module and the target a finite derivative of the tautological signature
 
    *)
   Definition elementary_equation : UU :=
-    ∑ (S1 : signature_over Sig)(n : nat), isEpi_overSig S1 × half_equation S1 (θ ^(n)) × half_equation S1 (θ ^(n)). 
+    ∑ (S1 : signature_over Sig)(n : nat), isEpi_overSig S1 × half_equation S1 (θ ^(n)) × half_equation S1 (θ ^(n)).
 
   (** The Sig-module source of a soft equation *)
   Definition source_elem_eq (e : elementary_equation) : signature_over Sig :=
@@ -251,12 +251,12 @@ The source is an epi-Sig-module and the target a finite derivative of the tautol
   Local Notation σ' := source_elem_eq.
   Local Notation τ' := target_elem_eq.
 
-  Definition source_elem_epiSig (e : elementary_equation) : isEpi_overSig (σ' e) := 
+  Definition source_elem_epiSig (e : elementary_equation) : isEpi_overSig (σ' e) :=
     pr1 (pr2 (pr2 e)).
 
   Definition half_elem_eqs (e : elementary_equation) :
     half_equation (σ' e) (θ ^(τ' e)) ×
-    half_equation (σ' e) (θ ^(τ' e)) 
+    half_equation (σ' e) (θ ^(τ' e))
     :=
     pr2 (pr2 (pr2 e)).
 
@@ -273,7 +273,7 @@ The source is an epi-Sig-module and the target a finite derivative of the tautol
 
 End QuotientRep.
 
-Definition soft_equation_choice (choice : AxiomOfChoice.AxiomOfChoice_surj) (S : signature SET) 
+Definition soft_equation_choice (choice : AxiomOfChoice.AxiomOfChoice_surj) (S : signature SET)
             (** S preserves epimorphisms of monads *)
            (isEpi_sig : sig_preservesNatEpiMonad S)
          : UU :=
diff --git a/Modules/SoftEquations/quotientrepslice.v b/Modules/SoftEquations/quotientrepslice.v
index f3fc4ae..ae45544 100644
--- a/Modules/SoftEquations/quotientrepslice.v
+++ b/Modules/SoftEquations/quotientrepslice.v
@@ -22,13 +22,13 @@ complicate its use.
 Require Import UniMath.Foundations.PartD.
 
 Require Import UniMath.CategoryTheory.Monads.Monads.
-Require Import UniMath.CategoryTheory.Monads.LModules. 
+Require Import UniMath.CategoryTheory.Monads.LModules.
 Require Import UniMath.CategoryTheory.SetValuedFunctors.
 Require Import UniMath.CategoryTheory.HorizontalComposition.
 
 Require Import UniMath.CategoryTheory.Core.Prelude.
 Require Import UniMath.CategoryTheory.FunctorCategory.
-Require Import UniMath.CategoryTheory.categories.HSET.All.
+Require Import UniMath.CategoryTheory.Categories.HSET.All.
 
 Require Import UniMath.Foundations.Sets.
 Require Import UniMath.CategoryTheory.Epis.
@@ -49,7 +49,7 @@ Open Scope cat.
 
 (** TODO : move this section in Prelims/..
 and use thees results to shorten quotienrep (or don't do that because we don't care about
-this old presentable stuff 
+this old presentable stuff
  *)
 Section univ_mod.
   Context {C  : category}{R : Monad C}.
@@ -95,7 +95,7 @@ completion of the diagram with an arrow from N to O
    *)
   Definition univ_surj_lmod_nt_epi epip : LModule_Mor R N O := _ ,, univ_surj_lmod_laws epip.
 
-      
+
 End univ_mod.
 
 (** Now we do the same when N and O are modules over another monad S
@@ -126,7 +126,7 @@ But here, we want a S-module morphism. Hence, we need an additional hypothesis,
    m*O
 *)
 
-  Lemma univ_surj_pb_lmod_laws 
+  Lemma univ_surj_pb_lmod_laws
         (epip : isEpi (C := [C, SET]) (p : nat_trans M N)) :
           LModule_Mor_laws S (univ_surj_nt p f compat epip).
   Proof.
@@ -148,10 +148,10 @@ But here, we want a S-module morphism. Hence, we need an additional hypothesis,
    *)
   Definition univ_surj_pb_lmod_nt_epi epip : LModule_Mor S N O := _ ,, univ_surj_pb_lmod_laws epip.
 
-      
+
 End univ_pb_mod.
 
-    
+
 Local Notation  "R →→ S" := (rep_fiber_mor R S) (at level 6).
 
 Section QuotientRep.
@@ -191,7 +191,7 @@ Proof.
     apply isEpi_projR.
 Qed.
 
-  
+
 
 Local Notation π := projR.
 Local Notation Θ := tautological_LModule.
@@ -230,7 +230,7 @@ Qed.
      V                 V
      R ----------->    R'
            π
-          
+
 >>
  *)
 Definition R'_action : LModule_Mor R' (Sig R') (Θ R').
@@ -320,7 +320,7 @@ Proof.
   etrans; [apply rep_fiber_mor_ax|].
   rewrite assoc.
   apply cancel_postcomposition.
-  
+
   rewrite (u_monad_def R_epi  d ff).
   rewrite signature_comp.
   reflexivity.