diff --git a/theories/Basics/Settings.v b/theories/Basics/Settings.v
index 46d7594ebd..738f277c3a 100644
--- a/theories/Basics/Settings.v
+++ b/theories/Basics/Settings.v
@@ -42,7 +42,10 @@ Global Set Printing Primitive Projection Parameters.
 (** ** Pattern Matching *)
 
 (** This flag removes parameters from constructors in patterns that appear in a match statement. *)
-Global Set Asymmetric Patterns. #[warning="-unknown-option"] Global Set Asymmetric Patterns No Implicits.
+Global Set Asymmetric Patterns.
+(** The warning clause here can be removed once our minimum Rocq version is 9.3. *)
+#[warning="-unknown-option"]
+Global Set Asymmetric Patterns No Implicits.
 
 (** ** Unification *)
 
diff --git a/theories/Categories/Adjoint/Composition/AssociativityLaw.v b/theories/Categories/Adjoint/Composition/AssociativityLaw.v
index ffaa80735c..e1a47779b7 100644
--- a/theories/Categories/Adjoint/Composition/AssociativityLaw.v
+++ b/theories/Categories/Adjoint/Composition/AssociativityLaw.v
@@ -4,10 +4,8 @@ Require Import Adjoint.Composition.Core Adjoint.Core.
 Require Adjoint.Composition.LawsTactic.
 Require Import Types.Sigma Types.Prod.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope adjunction_scope.
 Local Open Scope morphism_scope.
diff --git a/theories/Categories/Adjoint/Composition/Core.v b/theories/Categories/Adjoint/Composition/Core.v
index 294cfacb51..4859456c73 100644
--- a/theories/Categories/Adjoint/Composition/Core.v
+++ b/theories/Categories/Adjoint/Composition/Core.v
@@ -7,10 +7,8 @@ Require Import Adjoint.UnitCounit Adjoint.Core.
 Require Import HoTT.Tactics.
 Require Import Basics.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope natural_transformation_scope.
 
diff --git a/theories/Categories/Adjoint/Composition/IdentityLaws.v b/theories/Categories/Adjoint/Composition/IdentityLaws.v
index e7fb2f7510..5d98530e99 100644
--- a/theories/Categories/Adjoint/Composition/IdentityLaws.v
+++ b/theories/Categories/Adjoint/Composition/IdentityLaws.v
@@ -4,10 +4,8 @@ Require Import Adjoint.Composition.Core Adjoint.Core Adjoint.Identity.
 Require Adjoint.Composition.LawsTactic.
 Require Import Types.Sigma Types.Prod.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope adjunction_scope.
 Local Open Scope morphism_scope.
diff --git a/theories/Categories/Adjoint/Composition/LawsTactic.v b/theories/Categories/Adjoint/Composition/LawsTactic.v
index 5d224b1268..bac9e14e30 100644
--- a/theories/Categories/Adjoint/Composition/LawsTactic.v
+++ b/theories/Categories/Adjoint/Composition/LawsTactic.v
@@ -4,10 +4,8 @@ Require Import Functor.Composition.Laws.
 Require Import Adjoint.UnitCounit Adjoint.Paths.
 Require Import PathGroupoids HoTT.Tactics Types.Prod Types.Forall.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Ltac law_t :=
   rewrite !transport_path_prod'; simpl;
diff --git a/theories/Categories/Adjoint/Dual.v b/theories/Categories/Adjoint/Dual.v
index 3b992de31a..3d0c575d64 100644
--- a/theories/Categories/Adjoint/Dual.v
+++ b/theories/Categories/Adjoint/Dual.v
@@ -3,10 +3,8 @@ Require Import Category.Core Functor.Core.
 Require Import Functor.Dual NaturalTransformation.Dual.
 Require Import Adjoint.UnitCounit Adjoint.Core.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope category_scope.
 
diff --git a/theories/Categories/Adjoint/Functorial/Core.v b/theories/Categories/Adjoint/Functorial/Core.v
index 6cf90862ca..a2e0f69b7f 100644
--- a/theories/Categories/Adjoint/Functorial/Core.v
+++ b/theories/Categories/Adjoint/Functorial/Core.v
@@ -7,10 +7,8 @@ Require Import Adjoint.Core.
 Require Import Adjoint.Functorial.Parts Adjoint.Functorial.Laws.
 Require Import HoTT.Types.Prod.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope natural_transformation_scope.
 Local Open Scope morphism_scope.
diff --git a/theories/Categories/Adjoint/Functorial/Laws.v b/theories/Categories/Adjoint/Functorial/Laws.v
index dd841d46bb..c32bc91ec4 100644
--- a/theories/Categories/Adjoint/Functorial/Laws.v
+++ b/theories/Categories/Adjoint/Functorial/Laws.v
@@ -10,10 +10,8 @@ Require Import Adjoint.Functorial.Parts.
 Require Import HoTT.Tactics.
 Require Import Basics.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope natural_transformation_scope.
 Local Open Scope morphism_scope.
diff --git a/theories/Categories/Adjoint/Functorial/Parts.v b/theories/Categories/Adjoint/Functorial/Parts.v
index badd5f8087..39e9913c30 100644
--- a/theories/Categories/Adjoint/Functorial/Parts.v
+++ b/theories/Categories/Adjoint/Functorial/Parts.v
@@ -5,10 +5,8 @@ Require Import NaturalTransformation.Composition.Core NaturalTransformation.Comp
 Require Import Functor.Dual NaturalTransformation.Dual.
 Require Import Adjoint.Core Adjoint.UnitCounit Adjoint.Dual.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope natural_transformation_scope.
 Local Open Scope morphism_scope.
diff --git a/theories/Categories/Adjoint/Hom.v b/theories/Categories/Adjoint/Hom.v
index 940460aeee..92668efe62 100644
--- a/theories/Categories/Adjoint/Hom.v
+++ b/theories/Categories/Adjoint/Hom.v
@@ -8,11 +8,8 @@ Require Import Functor.Composition.Core.
 Require Import FunctorCategory.Morphisms.
 Require Import Functor.Identity.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
-
 
 Local Open Scope morphism_scope.
 Local Open Scope category_scope.
diff --git a/theories/Categories/Adjoint/HomCoercions.v b/theories/Categories/Adjoint/HomCoercions.v
index 5a07618a31..86094e98aa 100644
--- a/theories/Categories/Adjoint/HomCoercions.v
+++ b/theories/Categories/Adjoint/HomCoercions.v
@@ -8,10 +8,8 @@ Require Import Functor.Identity.
 Require Import SetCategory.Morphisms.
 Require Import Basics.Trunc Types.Sigma HoTT.Tactics Equivalences.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope path_scope.
 Local Open Scope morphism_scope.
diff --git a/theories/Categories/Adjoint/Identity.v b/theories/Categories/Adjoint/Identity.v
index 37c4ec8113..ff6e79fc27 100644
--- a/theories/Categories/Adjoint/Identity.v
+++ b/theories/Categories/Adjoint/Identity.v
@@ -3,10 +3,8 @@ Require Import Category.Core.
 Require Import Functor.Identity NaturalTransformation.Identity.
 Require Import Adjoint.UnitCounit Adjoint.Core.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Section identity.
   (** There is an identity adjunction.  It does the obvious thing. *)
diff --git a/theories/Categories/Adjoint/Paths.v b/theories/Categories/Adjoint/Paths.v
index 2a7f6893dc..8c10dbe943 100644
--- a/theories/Categories/Adjoint/Paths.v
+++ b/theories/Categories/Adjoint/Paths.v
@@ -5,10 +5,8 @@ Require Import Adjoint.UnitCounit Adjoint.Core NaturalTransformation.Paths.
 Require Import Types Trunc.
 Require Import Basics.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope morphism_scope.
 Local Open Scope natural_transformation_scope.
@@ -20,8 +18,6 @@ Section path_adjunction.
   Variable F : Functor C D.
   Variable G : Functor D C.
 
-
-
   Notation adjunction_sig :=
     { eta : NaturalTransformation 1 (G o F)
     | { eps : NaturalTransformation (F o G) 1
diff --git a/theories/Categories/Adjoint/Pointwise.v b/theories/Categories/Adjoint/Pointwise.v
index bee9d590c5..59a08fe37a 100644
--- a/theories/Categories/Adjoint/Pointwise.v
+++ b/theories/Categories/Adjoint/Pointwise.v
@@ -12,10 +12,8 @@ Import NaturalTransformation.Identity.NaturalTransformationIdentityNotations.
 Require Import NaturalTransformation.Paths Functor.Paths.
 Require Import Basics.PathGroupoids HoTT.Tactics Types.Arrow.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope morphism_scope.
 Local Open Scope functor_scope.
diff --git a/theories/Categories/Adjoint/UnitCounit.v b/theories/Categories/Adjoint/UnitCounit.v
index d1677a2f11..d1ddd85b52 100644
--- a/theories/Categories/Adjoint/UnitCounit.v
+++ b/theories/Categories/Adjoint/UnitCounit.v
@@ -3,10 +3,8 @@ Require Import Category.Core Functor.Core NaturalTransformation.Core.
 Require Import Category.Dual Functor.Dual NaturalTransformation.Dual.
 Require Import Functor.Composition.Core Functor.Identity.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope category_scope.
 Local Open Scope morphism_scope.
diff --git a/theories/Categories/Adjoint/UnitCounitCoercions.v b/theories/Categories/Adjoint/UnitCounitCoercions.v
index 08711be2cd..a8dfaccd73 100644
--- a/theories/Categories/Adjoint/UnitCounitCoercions.v
+++ b/theories/Categories/Adjoint/UnitCounitCoercions.v
@@ -5,10 +5,8 @@ Require Import Functor.Composition.Core Functor.Identity.
 Require Import HoTT.Tactics Basics.Trunc Types.Sigma.
 Require Import Basics.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope natural_transformation_scope.
 Local Open Scope category_scope.
diff --git a/theories/Categories/Adjoint/UniversalMorphisms/Core.v b/theories/Categories/Adjoint/UniversalMorphisms/Core.v
index e4ef3b2c71..77c23d94ca 100644
--- a/theories/Categories/Adjoint/UniversalMorphisms/Core.v
+++ b/theories/Categories/Adjoint/UniversalMorphisms/Core.v
@@ -9,10 +9,8 @@ Import Comma.Core.
 Local Set Warnings "notation-overridden".
 Require Import UniversalProperties Comma.Dual InitialTerminalCategory.Core InitialTerminalCategory.Functors.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope morphism_scope.
 
diff --git a/theories/Categories/Cat/Core.v b/theories/Categories/Cat/Core.v
index a3ad64f3aa..68cae3defb 100644
--- a/theories/Categories/Cat/Core.v
+++ b/theories/Categories/Cat/Core.v
@@ -2,10 +2,8 @@
 Require Import Category.Objects InitialTerminalCategory.Core InitialTerminalCategory.Functors Functor.Core Category.Strict Functor.Paths.
 Require Import Functor.Identity Functor.Composition.Core Functor.Composition.Laws.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope functor_scope.
 
diff --git a/theories/Categories/Cat/Morphisms.v b/theories/Categories/Cat/Morphisms.v
index 7765a03a37..a5a5343481 100644
--- a/theories/Categories/Cat/Morphisms.v
+++ b/theories/Categories/Cat/Morphisms.v
@@ -2,10 +2,8 @@
 Require Import Category.Core Functor.Core FunctorCategory.Core NaturalTransformation.Core.
 Require Import Category.Morphisms.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope category_scope.
 Local Open Scope morphism_scope.
diff --git a/theories/Categories/Category/Core.v b/theories/Categories/Category/Core.v
index 3e8ce50db3..5208c1e74c 100644
--- a/theories/Categories/Category/Core.v
+++ b/theories/Categories/Category/Core.v
@@ -1,10 +1,8 @@
 (** * Definition of a [PreCategory] *)
 Require Export Overture Basics.Notations.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Declare Scope morphism_scope.
 Declare Scope category_scope.
diff --git a/theories/Categories/Category/Dual.v b/theories/Categories/Category/Dual.v
index 5e3192c588..911babc959 100644
--- a/theories/Categories/Category/Dual.v
+++ b/theories/Categories/Category/Dual.v
@@ -1,11 +1,8 @@
 (** * Opposite Category *)
 Require Import Category.Core Category.Objects.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
-
 
 Local Open Scope morphism_scope.
 Local Open Scope category_scope.
diff --git a/theories/Categories/Category/Morphisms.v b/theories/Categories/Category/Morphisms.v
index 3251a95c15..5ca1b69bdc 100644
--- a/theories/Categories/Category/Morphisms.v
+++ b/theories/Categories/Category/Morphisms.v
@@ -2,10 +2,8 @@
 Require Import Category.Core Functor.Core.
 Require Import HoTT.Tactics Basics.Trunc Basics.Tactics Basics.Equivalences Types.Sigma.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope category_scope.
 Local Open Scope morphism_scope.
diff --git a/theories/Categories/Category/Objects.v b/theories/Categories/Category/Objects.v
index 2ef90cd787..0b611f9dd5 100644
--- a/theories/Categories/Category/Objects.v
+++ b/theories/Categories/Category/Objects.v
@@ -2,10 +2,8 @@
 Require Import Basics.Contractible.
 Require Import Category.Core Category.Morphisms.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope category_scope.
 Local Open Scope morphism_scope.
diff --git a/theories/Categories/Category/Paths.v b/theories/Categories/Category/Paths.v
index a67240c07e..86525f164a 100644
--- a/theories/Categories/Category/Paths.v
+++ b/theories/Categories/Category/Paths.v
@@ -4,18 +4,14 @@ Require Import HoTT.Basics.Equivalences HoTT.Basics.PathGroupoids HoTT.Basics.Tr
 Require Import HoTT.Types.Sigma HoTT.Types.Arrow HoTT.Types.Forall.
 Require Import HoTT.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope morphism_scope.
 Local Open Scope category_scope.
 
 Section path_category.
   Local Open Scope path_scope.
-
-
   (** We add a prime ([']) as an arbitrary convention to denote that
       we are talking about equality of functions (less convenient for
       use) rather than pointwise equality of functions (more
diff --git a/theories/Categories/Category/Pi.v b/theories/Categories/Category/Pi.v
index 865f58dabb..027e914b6f 100644
--- a/theories/Categories/Category/Pi.v
+++ b/theories/Categories/Category/Pi.v
@@ -2,10 +2,8 @@
 Require Import Category.Strict.
 Require Import Basics.Trunc.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope category_scope.
 Local Open Scope morphism_scope.
diff --git a/theories/Categories/Category/Prod.v b/theories/Categories/Category/Prod.v
index 683a89d959..5b84d521d1 100644
--- a/theories/Categories/Category/Prod.v
+++ b/theories/Categories/Category/Prod.v
@@ -3,10 +3,8 @@ Require Import Basics.Tactics.
 Require Import Category.Strict.
 Require Import Types.Prod.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope category_scope.
 Local Open Scope morphism_scope.
diff --git a/theories/Categories/Category/Sigma/Core.v b/theories/Categories/Category/Sigma/Core.v
index ca68f449af..2cb89cc648 100644
--- a/theories/Categories/Category/Sigma/Core.v
+++ b/theories/Categories/Category/Sigma/Core.v
@@ -2,10 +2,8 @@
 Require Import Category.Core Functor.Core.
 Require Import Basics.Trunc Types.Sigma.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Notation sig_type := sig.
 
diff --git a/theories/Categories/Category/Sigma/OnMorphisms.v b/theories/Categories/Category/Sigma/OnMorphisms.v
index c68204e378..f9638214f0 100644
--- a/theories/Categories/Category/Sigma/OnMorphisms.v
+++ b/theories/Categories/Category/Sigma/OnMorphisms.v
@@ -6,10 +6,8 @@ Require Import Functor.Paths.
 Import Functor.Identity.FunctorIdentityNotations.
 Import Functor.Composition.Core.FunctorCompositionCoreNotations.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Notation sig_type := Overture.sig.
 Local Notation pr1_type := Overture.pr1.
diff --git a/theories/Categories/Category/Sigma/OnObjects.v b/theories/Categories/Category/Sigma/OnObjects.v
index 88887409a6..b3f7191bc1 100644
--- a/theories/Categories/Category/Sigma/OnObjects.v
+++ b/theories/Categories/Category/Sigma/OnObjects.v
@@ -6,10 +6,8 @@ Require Import Functor.Paths.
 Import Functor.Identity.FunctorIdentityNotations.
 Import Functor.Composition.Core.FunctorCompositionCoreNotations.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Notation sig_type := Overture.sig.
 Local Notation pr1_type := Overture.pr1.
diff --git a/theories/Categories/Category/Sigma/Univalent.v b/theories/Categories/Category/Sigma/Univalent.v
index 27d472176f..077d03dcac 100644
--- a/theories/Categories/Category/Sigma/Univalent.v
+++ b/theories/Categories/Category/Sigma/Univalent.v
@@ -4,10 +4,8 @@ Require Import Category.Univalent.
 Require Import Category.Sigma.Core Category.Sigma.OnObjects Category.Sigma.OnMorphisms.
 Require Import HoTT.Types HoTT.Basics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Notation pr1_type := Overture.pr1 (only parsing).
 
diff --git a/theories/Categories/Category/Strict.v b/theories/Categories/Category/Strict.v
index 5df37fe405..76205a4044 100644
--- a/theories/Categories/Category/Strict.v
+++ b/theories/Categories/Category/Strict.v
@@ -1,10 +1,8 @@
 (** * Definition of a strict category *)
 Require Export Category.Core.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope morphism_scope.
 
diff --git a/theories/Categories/Category/Sum.v b/theories/Categories/Category/Sum.v
index f5e01b8b2b..3bb1d620a4 100644
--- a/theories/Categories/Category/Sum.v
+++ b/theories/Categories/Category/Sum.v
@@ -1,10 +1,8 @@
 (** * The coproduct of categories *)
 Require Export Category.Core.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 (** ** Definition of [+] for categories *)
 Section internals.
diff --git a/theories/Categories/Category/Univalent.v b/theories/Categories/Category/Univalent.v
index c1bd4c88b8..84116b0748 100644
--- a/theories/Categories/Category/Univalent.v
+++ b/theories/Categories/Category/Univalent.v
@@ -2,10 +2,8 @@
 Require Import Category.Core Category.Morphisms.
 Require Import HoTT.Basics HoTT.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope morphism_scope.
 
diff --git a/theories/Categories/CategoryOfGroupoids.v b/theories/Categories/CategoryOfGroupoids.v
index f019a1eb14..1a3aa630af 100644
--- a/theories/Categories/CategoryOfGroupoids.v
+++ b/theories/Categories/CategoryOfGroupoids.v
@@ -4,10 +4,8 @@ Require Import Cat.Core.
 Require Import GroupoidCategory.Core.
 Require Import Functor.Paths.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope functor_scope.
 
diff --git a/theories/Categories/CategoryOfSections/Core.v b/theories/Categories/CategoryOfSections/Core.v
index 98bf9cea10..5ae7eea3d7 100644
--- a/theories/Categories/CategoryOfSections/Core.v
+++ b/theories/Categories/CategoryOfSections/Core.v
@@ -6,12 +6,8 @@ Require Import NaturalTransformation.Paths NaturalTransformation.Composition.Cor
 Require Import Functor.Paths.
 Require Import HoTT.Basics HoTT.Types.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
-
-
 Local Open Scope functor_scope.
 
 Section FunctorSectionCategory.
diff --git a/theories/Categories/ChainCategory.v b/theories/Categories/ChainCategory.v
index 85af68c94c..9b32c0ef7f 100644
--- a/theories/Categories/ChainCategory.v
+++ b/theories/Categories/ChainCategory.v
@@ -4,10 +4,8 @@ Require Import Category.Sigma.Univalent.
 Require Import Category.Morphisms Category.Univalent Category.Strict.
 Require Import HoTT.Basics HoTT.Types HoTT.Spaces.Nat.Core.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope nat_scope.
 
@@ -64,8 +62,6 @@ Module Utf8.
   Notation "[ ∞ ]" := omega : category_scope.
   Notation "[ 'ω' ]" := omega : category_scope.
 End Utf8.
-
-
 Module Export Strict.
   Definition isstrict_omega : IsStrictCategory omega.
   Proof.
diff --git a/theories/Categories/Comma/Core.v b/theories/Categories/Comma/Core.v
index 48d37629c8..b82247eb59 100644
--- a/theories/Categories/Comma/Core.v
+++ b/theories/Categories/Comma/Core.v
@@ -6,12 +6,8 @@ Require Functor.Identity.
 Require Import Category.Strict.
 Import Functor.Identity.FunctorIdentityNotations.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
-
-
 Local Open Scope morphism_scope.
 Local Open Scope category_scope.
 
@@ -161,8 +157,6 @@ Module Import CommaCategory.
       apply contr_inhabited_hprop; try reflexivity.
       typeclasses eauto.
     Qed.
-
-
     Lemma issig_morphism abf a'b'f'
     : (morphism_sig_T abf a'b'f')
         <~> morphism abf a'b'f'.
@@ -285,8 +279,6 @@ Qed.
       hnf in *.
       destruct i, i'.
       simpl in *.
-
-
     #[export] Instance comma_category_IsCategory `{IsCategory A, IsCategory B}
     : IsCategory comma_category.
     Proof.
diff --git a/theories/Categories/Comma/Dual.v b/theories/Categories/Comma/Dual.v
index e3b4a05e9d..7ea313e7e5 100644
--- a/theories/Categories/Comma/Dual.v
+++ b/theories/Categories/Comma/Dual.v
@@ -7,10 +7,8 @@ Local Set Warnings "-notation-overridden". (* work around bug #5567, https://coq
 Import Comma.Core.
 Local Set Warnings "notation-overridden".
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope path_scope.
 Local Open Scope morphism_scope.
diff --git a/theories/Categories/Comma/Functorial.v b/theories/Categories/Comma/Functorial.v
index 4463fcf748..90e4ed2ed5 100644
--- a/theories/Categories/Comma/Functorial.v
+++ b/theories/Categories/Comma/Functorial.v
@@ -11,12 +11,8 @@ Local Set Warnings "notation-overridden".
 Import Functor.Identity.FunctorIdentityNotations NaturalTransformation.Identity.NaturalTransformationIdentityNotations.
 Require Import HoTT.Tactics PathGroupoids Types.Forall.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
-
-
 Local Open Scope morphism_scope.
 Local Open Scope category_scope.
 
diff --git a/theories/Categories/Comma/InducedFunctors.v b/theories/Categories/Comma/InducedFunctors.v
index bf0fab941b..862d71b779 100644
--- a/theories/Categories/Comma/InducedFunctors.v
+++ b/theories/Categories/Comma/InducedFunctors.v
@@ -12,10 +12,8 @@ Local Set Warnings "notation-overridden".
 Require Import HoTT.Tactics.
 Require Import Basics.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope functor_scope.
 Local Open Scope category_scope.
diff --git a/theories/Categories/Comma/Projection.v b/theories/Categories/Comma/Projection.v
index 0a682aa381..2727c90913 100644
--- a/theories/Categories/Comma/Projection.v
+++ b/theories/Categories/Comma/Projection.v
@@ -9,10 +9,8 @@ Local Set Warnings "-notation-overridden". (* work around bug #5567, https://coq
 Import Comma.Core.
 Local Set Warnings "notation-overridden". (* work around bug #5567, https://coq.inria.fr/bugs/show_bug.cgi?id=5567, notation-overridden,parsing should not trigger for only printing notations *)
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope functor_scope.
 Local Open Scope category_scope.
diff --git a/theories/Categories/Comma/ProjectionFunctors.v b/theories/Categories/Comma/ProjectionFunctors.v
index 6702d7f67a..4e640bf386 100644
--- a/theories/Categories/Comma/ProjectionFunctors.v
+++ b/theories/Categories/Comma/ProjectionFunctors.v
@@ -15,10 +15,8 @@ Require Import Comma.InducedFunctors Comma.Projection.
 Require ProductLaws ExponentialLaws.Law1.Functors ExponentialLaws.Law4.Functors.
 Require Import Types.Forall PathGroupoids HoTT.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope category_scope.
 
diff --git a/theories/Categories/DependentProduct.v b/theories/Categories/DependentProduct.v
index 438aad41dd..95b6d6e2b6 100644
--- a/theories/Categories/DependentProduct.v
+++ b/theories/Categories/DependentProduct.v
@@ -4,10 +4,8 @@ Require Import Cat.Core.
 Require Grothendieck.ToCat.
 Require Import CategoryOfSections.Core.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope functor_scope.
 
diff --git a/theories/Categories/DiscreteCategory.v b/theories/Categories/DiscreteCategory.v
index 60e2c94af7..2d7648124f 100644
--- a/theories/Categories/DiscreteCategory.v
+++ b/theories/Categories/DiscreteCategory.v
@@ -1,10 +1,8 @@
 (** * Discrete category *)
 Require Import HoTT.Basics GroupoidCategory.Core.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 (** A discrete category is a groupoid which is a 0-type *)
 Module Export Core.
diff --git a/theories/Categories/DualFunctor.v b/theories/Categories/DualFunctor.v
index d5a36d990b..9f39a3dadd 100644
--- a/theories/Categories/DualFunctor.v
+++ b/theories/Categories/DualFunctor.v
@@ -5,10 +5,8 @@ Require Import Functor.Composition.Core Functor.Identity.
 Require Import Cat.Core Functor.Paths.
 Require Import Basics.Trunc Types.Sigma HoTT.Tactics Types.Forall.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope category_scope.
 
diff --git a/theories/Categories/ExponentialLaws.v b/theories/Categories/ExponentialLaws.v
index f9bfe1ca98..1fd1f51d79 100644
--- a/theories/Categories/ExponentialLaws.v
+++ b/theories/Categories/ExponentialLaws.v
@@ -21,7 +21,5 @@ Require ExponentialLaws.Law3.
 (** ** Currying *)
 (** *** [(yⁿ)ᵐ ≅ yⁿᵐ] *)
 Require ExponentialLaws.Law4.
-
-
 Require ExponentialLaws.Tactics.
 Include ExponentialLaws.Tactics.
diff --git a/theories/Categories/ExponentialLaws/Law0.v b/theories/Categories/ExponentialLaws/Law0.v
index e6704a81a8..e853ebbd1e 100644
--- a/theories/Categories/ExponentialLaws/Law0.v
+++ b/theories/Categories/ExponentialLaws/Law0.v
@@ -3,10 +3,8 @@ Require Import Category.Core Functor.Core FunctorCategory.Core Functor.Identity.
 Require Import InitialTerminalCategory.Core InitialTerminalCategory.Functors InitialTerminalCategory.NaturalTransformations.
 Require Import HoTT.Basics HoTT.Types.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope functor_scope.
 
@@ -16,8 +14,6 @@ Local Open Scope functor_scope.
       - [0ˣ ≅ 0] if [x ≠ 0]
       - [0⁰ ≅ 1]
  *)
-
-
 (** ** x⁰ ≅ 1 *)
 Section law0.
   Context `{Funext}.
diff --git a/theories/Categories/ExponentialLaws/Law1/Functors.v b/theories/Categories/ExponentialLaws/Law1/Functors.v
index 4cf798facb..bf1184bec5 100644
--- a/theories/Categories/ExponentialLaws/Law1/Functors.v
+++ b/theories/Categories/ExponentialLaws/Law1/Functors.v
@@ -3,10 +3,8 @@ Require Import Category.Core Functor.Core FunctorCategory.Core Functor.Identity
 Require Import InitialTerminalCategory.Core InitialTerminalCategory.Functors InitialTerminalCategory.NaturalTransformations.
 Require Import HoTT.Basics HoTT.Types.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope functor_scope.
 
diff --git a/theories/Categories/ExponentialLaws/Law1/Law.v b/theories/Categories/ExponentialLaws/Law1/Law.v
index 8ce178f169..94589b5031 100644
--- a/theories/Categories/ExponentialLaws/Law1/Law.v
+++ b/theories/Categories/ExponentialLaws/Law1/Law.v
@@ -4,10 +4,8 @@ Require Import InitialTerminalCategory.Core.
 Require Import Basics.Trunc ExponentialLaws.Tactics.
 Require Import Basics.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope functor_scope.
 
diff --git a/theories/Categories/ExponentialLaws/Law2/Functors.v b/theories/Categories/ExponentialLaws/Law2/Functors.v
index 5d10cc5859..725f124a75 100644
--- a/theories/Categories/ExponentialLaws/Law2/Functors.v
+++ b/theories/Categories/ExponentialLaws/Law2/Functors.v
@@ -1,10 +1,8 @@
 (** * Exponential functors between products and sums in exponents *)
 Require Import Functor.Core FunctorCategory.Core Functor.Identity NaturalTransformation.Core Category.Sum Category.Prod Functor.Sum Functor.Prod.Core NaturalTransformation.Sum Functor.Pointwise.Core NaturalTransformation.Paths.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope functor_scope.
 
diff --git a/theories/Categories/ExponentialLaws/Law2/Law.v b/theories/Categories/ExponentialLaws/Law2/Law.v
index 169938590e..60f40bd5d0 100644
--- a/theories/Categories/ExponentialLaws/Law2/Law.v
+++ b/theories/Categories/ExponentialLaws/Law2/Law.v
@@ -6,10 +6,8 @@ Require Import Functor.Identity Functor.Composition.Core.
 Require Import Types.Prod ExponentialLaws.Tactics.
 Require Import ExponentialLaws.Law2.Functors.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope functor_scope.
 
@@ -18,8 +16,6 @@ Section Law2.
   Context `{Funext}.
   Variables D C1 C2 : PreCategory.
 
-
-
   Lemma helper1 (c : Functor C1 D * Functor C2 D)
   : ((1 o (Basics.Overture.fst c + Basics.Overture.snd c) o inl C1 C2)%functor,
      (1 o (Basics.Overture.fst c + Basics.Overture.snd c) o inr C1 C2)%functor)%core = c.
diff --git a/theories/Categories/ExponentialLaws/Law3/Functors.v b/theories/Categories/ExponentialLaws/Law3/Functors.v
index 2fc051b639..678154247f 100644
--- a/theories/Categories/ExponentialLaws/Law3/Functors.v
+++ b/theories/Categories/ExponentialLaws/Law3/Functors.v
@@ -3,10 +3,8 @@ Require Import Category.Core Functor.Core FunctorCategory.Core Category.Prod.
 Require Import Functor.Prod Functor.Composition.Core NaturalTransformation.Composition.Laws NaturalTransformation.Composition.Core.
 Require Import Types.Prod.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope natural_transformation_scope.
 Local Open Scope functor_scope.
diff --git a/theories/Categories/ExponentialLaws/Law3/Law.v b/theories/Categories/ExponentialLaws/Law3/Law.v
index 7eac2c714c..0e3436d658 100644
--- a/theories/Categories/ExponentialLaws/Law3/Law.v
+++ b/theories/Categories/ExponentialLaws/Law3/Law.v
@@ -6,10 +6,8 @@ Require Import Functor.Identity Functor.Composition.Core.
 Require Import ExponentialLaws.Law3.Functors.
 Require Import Types.Prod ExponentialLaws.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope functor_scope.
 
diff --git a/theories/Categories/ExponentialLaws/Law4/Functors.v b/theories/Categories/ExponentialLaws/Law4/Functors.v
index ca7fe03569..7d3ba4c2da 100644
--- a/theories/Categories/ExponentialLaws/Law4/Functors.v
+++ b/theories/Categories/ExponentialLaws/Law4/Functors.v
@@ -2,10 +2,8 @@
 Require Import Category.Core Category.Prod FunctorCategory.Core Functor.Core NaturalTransformation.Core NaturalTransformation.Paths.
 Require Import Basics.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope functor_scope.
 
diff --git a/theories/Categories/ExponentialLaws/Law4/Law.v b/theories/Categories/ExponentialLaws/Law4/Law.v
index b957d2d2de..1de1276301 100644
--- a/theories/Categories/ExponentialLaws/Law4/Law.v
+++ b/theories/Categories/ExponentialLaws/Law4/Law.v
@@ -5,10 +5,8 @@ Require Import Functor.Identity Functor.Composition.Core.
 Require Import ExponentialLaws.Law4.Functors.
 Require Import ExponentialLaws.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope functor_scope.
 
diff --git a/theories/Categories/Functor/Attributes.v b/theories/Categories/Functor/Attributes.v
index 209c054ee4..252de24b95 100644
--- a/theories/Categories/Functor/Attributes.v
+++ b/theories/Categories/Functor/Attributes.v
@@ -2,10 +2,8 @@
 Require Import Category.Core Functor.Core HomFunctor Category.Morphisms Category.Dual Functor.Dual Category.Prod Functor.Prod NaturalTransformation.Core SetCategory.Core Functor.Composition.Core.
 Require Import Basics.Trunc Types.Universe HIT.iso HoTT.Truncations.Core.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope category_scope.
 
diff --git a/theories/Categories/Functor/Composition/Core.v b/theories/Categories/Functor/Composition/Core.v
index ef8848e973..5ddf67461a 100644
--- a/theories/Categories/Functor/Composition/Core.v
+++ b/theories/Categories/Functor/Composition/Core.v
@@ -1,10 +1,8 @@
 (** * Composition of functors *)
 Require Import Category.Core Functor.Core.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope morphism_scope.
 
diff --git a/theories/Categories/Functor/Composition/Functorial/Attributes.v b/theories/Categories/Functor/Composition/Functorial/Attributes.v
index be9802e05d..975930dd3f 100644
--- a/theories/Categories/Functor/Composition/Functorial/Attributes.v
+++ b/theories/Categories/Functor/Composition/Functorial/Attributes.v
@@ -9,10 +9,8 @@ Require Import Category.Morphisms.
 Require Import NaturalTransformation.Paths.
 Require Import HoTT.Truncations.Core.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope category_scope.
 Local Open Scope natural_transformation_scope.
diff --git a/theories/Categories/Functor/Composition/Functorial/Core.v b/theories/Categories/Functor/Composition/Functorial/Core.v
index 1dceced2fe..2faa0ac47c 100644
--- a/theories/Categories/Functor/Composition/Functorial/Core.v
+++ b/theories/Categories/Functor/Composition/Functorial/Core.v
@@ -5,10 +5,8 @@ Require Import Category.Prod FunctorCategory.Core NaturalTransformation.Composit
 Require Import NaturalTransformation.Paths.
 Require ProductLaws.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 (** Construction of the functor [_∘_ : (C → D) × (D → E) → (C → E)] and its curried variant *)
 Section functorial_composition.
diff --git a/theories/Categories/Functor/Composition/Laws.v b/theories/Categories/Functor/Composition/Laws.v
index 90231b5924..65654dd21c 100644
--- a/theories/Categories/Functor/Composition/Laws.v
+++ b/theories/Categories/Functor/Composition/Laws.v
@@ -3,10 +3,8 @@ Require Import Category.Core Functor.Core Functor.Composition.Core Functor.Ident
 Require Import Functor.Paths.
 Require Import Basics.PathGroupoids Basics.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope morphism_scope.
 
diff --git a/theories/Categories/Functor/Core.v b/theories/Categories/Functor/Core.v
index ac90a126dd..badb155635 100644
--- a/theories/Categories/Functor/Core.v
+++ b/theories/Categories/Functor/Core.v
@@ -1,10 +1,8 @@
 (** * Definition of a functor *)
 Require Import Category.Core.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Declare Scope functor_scope.
 Delimit Scope functor_scope with functor.
diff --git a/theories/Categories/Functor/Dual.v b/theories/Categories/Functor/Dual.v
index f7f73df5a0..c60fd3161b 100644
--- a/theories/Categories/Functor/Dual.v
+++ b/theories/Categories/Functor/Dual.v
@@ -3,10 +3,8 @@ Require Category.Dual.
 Import Category.Dual.CategoryDualNotations.
 Require Import Category.Core Functor.Core.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope category_scope.
 
diff --git a/theories/Categories/Functor/Identity.v b/theories/Categories/Functor/Identity.v
index f823512ade..1df8d43252 100644
--- a/theories/Categories/Functor/Identity.v
+++ b/theories/Categories/Functor/Identity.v
@@ -1,10 +1,8 @@
 (** * Identity functor *)
 Require Import Category.Core Functor.Core.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Section identity.
   (** There is an identity functor.  It does the obvious thing. *)
diff --git a/theories/Categories/Functor/Paths.v b/theories/Categories/Functor/Paths.v
index 18503710d5..4290553e9a 100644
--- a/theories/Categories/Functor/Paths.v
+++ b/theories/Categories/Functor/Paths.v
@@ -2,10 +2,8 @@
 Require Import Category.Core Functor.Core.
 Require Import HoTT.Basics HoTT.Types HoTT.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope path_scope.
 Local Open Scope morphism_scope.
@@ -16,8 +14,6 @@ Section path_functor.
 
   Variables C D : PreCategory.
 
-
-
   Local Notation functor_sig_T :=
     { OO : C -> D
     | { MO : forall s d, morphism C s d -> morphism D (OO s) (OO d)
diff --git a/theories/Categories/Functor/Pointwise/Core.v b/theories/Categories/Functor/Pointwise/Core.v
index 2d94a02a6c..05f71e0bb4 100644
--- a/theories/Categories/Functor/Pointwise/Core.v
+++ b/theories/Categories/Functor/Pointwise/Core.v
@@ -1,10 +1,8 @@
 (** * Functors between functor categories constructed pointwise *)
 Require Import Category.Core Functor.Core FunctorCategory.Core NaturalTransformation.Paths Functor.Composition.Core NaturalTransformation.Composition.Core.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope natural_transformation_scope.
 Local Open Scope morphism_scope.
diff --git a/theories/Categories/Functor/Pointwise/Properties.v b/theories/Categories/Functor/Pointwise/Properties.v
index 64407740b8..05c04a7821 100644
--- a/theories/Categories/Functor/Pointwise/Properties.v
+++ b/theories/Categories/Functor/Pointwise/Properties.v
@@ -3,10 +3,8 @@ Require Import Category.Core Functor.Core Functor.Pointwise.Core NaturalTransfor
 Require Import PathGroupoids Types.Forall HoTT.Tactics.
 Require Import Basics.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope category_scope.
 Local Open Scope functor_scope.
diff --git a/theories/Categories/Functor/Prod/Core.v b/theories/Categories/Functor/Prod/Core.v
index bb3e703d5e..64f382ff1d 100644
--- a/theories/Categories/Functor/Prod/Core.v
+++ b/theories/Categories/Functor/Prod/Core.v
@@ -2,10 +2,8 @@
 Require Import Category.Core Functor.Core Category.Prod Functor.Composition.Core.
 Require Import Types.Prod.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Notation fst_type := fst.
 Local Notation snd_type := snd.
diff --git a/theories/Categories/Functor/Prod/Functorial.v b/theories/Categories/Functor/Prod/Functorial.v
index 26a898e5f9..0d4c73c072 100644
--- a/theories/Categories/Functor/Prod/Functorial.v
+++ b/theories/Categories/Functor/Prod/Functorial.v
@@ -2,10 +2,8 @@
 Require Import Category.Core Functor.Core Functor.Prod.Core FunctorCategory.Core Category.Prod NaturalTransformation.Prod NaturalTransformation.Composition.Core.
 Require Import NaturalTransformation.Paths.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope natural_transformation_scope.
 
diff --git a/theories/Categories/Functor/Prod/Universal.v b/theories/Categories/Functor/Prod/Universal.v
index df1ad2d92e..37cc4dc20a 100644
--- a/theories/Categories/Functor/Prod/Universal.v
+++ b/theories/Categories/Functor/Prod/Universal.v
@@ -4,10 +4,8 @@ Require Import Functor.Paths.
 Require Import Types.Prod HoTT.Tactics Types.Forall Types.Sigma.
 Require Import Basics.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Notation fst_type := Basics.Overture.fst.
 Local Notation snd_type := Basics.Overture.snd.
diff --git a/theories/Categories/Functor/Sum.v b/theories/Categories/Functor/Sum.v
index 7f90d0905b..70bad0f7fa 100644
--- a/theories/Categories/Functor/Sum.v
+++ b/theories/Categories/Functor/Sum.v
@@ -3,10 +3,8 @@ Require Import Category.Sum Functor.Core Functor.Composition.Core Functor.Identi
 Require Import Functor.Paths HoTT.Tactics Types.Forall.
 Require Import Basics.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 (** We save [inl] and [inr] so we can use them to refer to the functors, too.  Outside of the [Categories/] directory, they should always be referred to as [Functor.inl] and [Functor.inr], after a [Require Functor].  Outside of this file, but in the [Categories/] directory, if you do not want to depend on all of [Functor] (for e.g., speed reasons), they should be referred to as [Functor.Sum.inl] and [Functor.Sum.inr] after a [Require Functor.Sum]. *)
 Local Notation type_inl := inl.
diff --git a/theories/Categories/FunctorCategory/Core.v b/theories/Categories/FunctorCategory/Core.v
index 15896afa5d..f26b4cc767 100644
--- a/theories/Categories/FunctorCategory/Core.v
+++ b/theories/Categories/FunctorCategory/Core.v
@@ -3,10 +3,8 @@ Require Import Category.Strict Functor.Core NaturalTransformation.Core Functor.P
 (** These must come last, so that [identity], [compose], etc., refer to natural transformations. *)
 Require Import NaturalTransformation.Composition.Core NaturalTransformation.Identity NaturalTransformation.Composition.Laws NaturalTransformation.Paths. 
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 (** ** Definition of [C → D] *)
 Section functor_category.
diff --git a/theories/Categories/FunctorCategory/Dual.v b/theories/Categories/FunctorCategory/Dual.v
index 10e6623164..98061d02ae 100644
--- a/theories/Categories/FunctorCategory/Dual.v
+++ b/theories/Categories/FunctorCategory/Dual.v
@@ -6,10 +6,8 @@ Require Import FunctorCategory.Core.
 Require Import Functor.Paths.
 Require Import HoTT.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope functor_scope.
 
diff --git a/theories/Categories/FunctorCategory/Functorial.v b/theories/Categories/FunctorCategory/Functorial.v
index 51f6103137..fe673194ca 100644
--- a/theories/Categories/FunctorCategory/Functorial.v
+++ b/theories/Categories/FunctorCategory/Functorial.v
@@ -1,10 +1,8 @@
 (** * Functoriality of functor category construction *)
 Require Import Category.Core Functor.Core FunctorCategory.Core Functor.Pointwise.Core Functor.Pointwise.Properties Category.Dual Category.Prod Cat.Core ExponentialLaws.Law4.Functors.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope category_scope.
 Local Open Scope type_scope.
diff --git a/theories/Categories/FunctorCategory/Morphisms.v b/theories/Categories/FunctorCategory/Morphisms.v
index 396dfee5e2..263c19d377 100644
--- a/theories/Categories/FunctorCategory/Morphisms.v
+++ b/theories/Categories/FunctorCategory/Morphisms.v
@@ -2,10 +2,8 @@
 Require Import Category.Core Functor.Core NaturalTransformation.Paths FunctorCategory.Core Category.Morphisms NaturalTransformation.Core.
 Require Import Basics.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope path_scope.
 Local Open Scope category_scope.
diff --git a/theories/Categories/FundamentalPreGroupoidCategory.v b/theories/Categories/FundamentalPreGroupoidCategory.v
index c2cbfa69c6..d9614a7c67 100644
--- a/theories/Categories/FundamentalPreGroupoidCategory.v
+++ b/theories/Categories/FundamentalPreGroupoidCategory.v
@@ -3,10 +3,8 @@ Require Import Category.Core.
 Require Import HoTT.Truncations.Core.
 Require Import HoTT.Basics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope path_scope.
 
diff --git a/theories/Categories/Grothendieck/PseudofunctorToCat.v b/theories/Categories/Grothendieck/PseudofunctorToCat.v
index 973cc74307..8a7d77a93f 100644
--- a/theories/Categories/Grothendieck/PseudofunctorToCat.v
+++ b/theories/Categories/Grothendieck/PseudofunctorToCat.v
@@ -8,10 +8,8 @@ Require Import Functor.Identity.
 Require Import FunctorCategory.Core.
 From HoTT Require Import Basics Types Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope morphism_scope.
 
diff --git a/theories/Categories/Grothendieck/ToCat.v b/theories/Categories/Grothendieck/ToCat.v
index 839a13ed1f..1ee6a88fe4 100644
--- a/theories/Categories/Grothendieck/ToCat.v
+++ b/theories/Categories/Grothendieck/ToCat.v
@@ -4,10 +4,8 @@ Require Import Pseudofunctor.FromFunctor.
 Require Import Cat.Core.
 Require Import Grothendieck.PseudofunctorToCat.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope morphism_scope.
 
diff --git a/theories/Categories/Grothendieck/ToSet/Core.v b/theories/Categories/Grothendieck/ToSet/Core.v
index 2182f73f99..cd7d4044ce 100644
--- a/theories/Categories/Grothendieck/ToSet/Core.v
+++ b/theories/Categories/Grothendieck/ToSet/Core.v
@@ -4,10 +4,8 @@ Require Import SetCategory.Core.
 Require Import Basics.Trunc Types.Sigma.
 Require Import Basics.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope morphism_scope.
 
diff --git a/theories/Categories/Grothendieck/ToSet/Morphisms.v b/theories/Categories/Grothendieck/ToSet/Morphisms.v
index 384a2ebbfc..027e297cff 100644
--- a/theories/Categories/Grothendieck/ToSet/Morphisms.v
+++ b/theories/Categories/Grothendieck/ToSet/Morphisms.v
@@ -5,10 +5,8 @@ Require Import SetCategory.Core.
 Require Import Grothendieck.ToSet.Core.
 Require Import HoTT.Basics HoTT.Types.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope morphism_scope.
 
diff --git a/theories/Categories/Grothendieck/ToSet/Univalent.v b/theories/Categories/Grothendieck/ToSet/Univalent.v
index 315a6a9003..5a7031ae03 100644
--- a/theories/Categories/Grothendieck/ToSet/Univalent.v
+++ b/theories/Categories/Grothendieck/ToSet/Univalent.v
@@ -7,10 +7,8 @@ Require Import Grothendieck.ToSet.Core Grothendieck.ToSet.Morphisms.
 Require Import HoTT.Basics.Equivalences HoTT.Basics.Trunc.
 Require Import HoTT.Types.Universe HoTT.Types.Sigma.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope morphism_scope.
 
diff --git a/theories/Categories/GroupoidCategory/Core.v b/theories/Categories/GroupoidCategory/Core.v
index d9311baf79..1ab2b50e6e 100644
--- a/theories/Categories/GroupoidCategory/Core.v
+++ b/theories/Categories/GroupoidCategory/Core.v
@@ -2,12 +2,8 @@
 Require Import Category.Morphisms Category.Strict.
 Require Import Trunc PathGroupoids Basics.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
-
-
 Local Open Scope category_scope.
 
 (** A groupoid is a precategory where every morphism is an isomorphism.  Since 1-types are 1-groupoids, we can construct the category corresponding to the 1-groupoid of a 1-type. *)
diff --git a/theories/Categories/GroupoidCategory/Dual.v b/theories/Categories/GroupoidCategory/Dual.v
index 12e1594e9c..76d0e39486 100644
--- a/theories/Categories/GroupoidCategory/Dual.v
+++ b/theories/Categories/GroupoidCategory/Dual.v
@@ -3,10 +3,8 @@ Require Import Category.Core GroupoidCategory.Core Category.Paths Category.Dual.
 Require Import HoTT.Types.
 Require Import Basics.Trunc Basics.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope category_scope.
 
diff --git a/theories/Categories/GroupoidCategory/Morphisms.v b/theories/Categories/GroupoidCategory/Morphisms.v
index 2ac8962053..a8ceffbe88 100644
--- a/theories/Categories/GroupoidCategory/Morphisms.v
+++ b/theories/Categories/GroupoidCategory/Morphisms.v
@@ -2,12 +2,8 @@
 Require Import Category.Core Category.Morphisms Category.Univalent GroupoidCategory.Core.
 Require Import Trunc Equivalences HoTT.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
-
-
 Local Open Scope category_scope.
 
 Section groupoid_category.
diff --git a/theories/Categories/HomFunctor.v b/theories/Categories/HomFunctor.v
index 18f75e0b9e..3ade20a1ac 100644
--- a/theories/Categories/HomFunctor.v
+++ b/theories/Categories/HomFunctor.v
@@ -4,10 +4,8 @@ Require Functor.Prod.Core.
 Import Category.Prod.CategoryProdNotations Functor.Prod.Core.FunctorProdCoreNotations.
 Require Import Basics.Trunc.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope morphism_scope.
 
diff --git a/theories/Categories/HomotopyPreCategory.v b/theories/Categories/HomotopyPreCategory.v
index c125dc3f66..b7903abf7d 100644
--- a/theories/Categories/HomotopyPreCategory.v
+++ b/theories/Categories/HomotopyPreCategory.v
@@ -2,10 +2,8 @@
 Require Import Category.Core.
 Require Import HoTT.Basics HoTT.Truncations.Core.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope path_scope.
 
diff --git a/theories/Categories/IndiscreteCategory.v b/theories/Categories/IndiscreteCategory.v
index 6181418894..fd2ba2810f 100644
--- a/theories/Categories/IndiscreteCategory.v
+++ b/theories/Categories/IndiscreteCategory.v
@@ -2,10 +2,8 @@
 Require Import Functor.Core Category.Strict Category.Univalent Category.Morphisms.
 Require Import Types.Unit Trunc HoTT.Tactics Equivalences.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 (** ** Definition of an indiscrete category *)
 Module Export Core.
diff --git a/theories/Categories/InitialTerminalCategory.v b/theories/Categories/InitialTerminalCategory.v
index bde1589ad2..eb39a9419e 100644
--- a/theories/Categories/InitialTerminalCategory.v
+++ b/theories/Categories/InitialTerminalCategory.v
@@ -10,6 +10,4 @@ Require InitialTerminalCategory.Functors.
 Require InitialTerminalCategory.NaturalTransformations.
 (** ** Pseudofunctors from initial and terminal categories *)
 Require InitialTerminalCategory.Pseudofunctors.
-
-
 Require Export InitialTerminalCategory.Notations.
diff --git a/theories/Categories/InitialTerminalCategory/Core.v b/theories/Categories/InitialTerminalCategory/Core.v
index 11ca76691e..8ad8cbdd94 100644
--- a/theories/Categories/InitialTerminalCategory/Core.v
+++ b/theories/Categories/InitialTerminalCategory/Core.v
@@ -3,10 +3,8 @@ Require Import HoTT.Basics HoTT.Types.
 Require Import Category.Core.
 Require Import NatCategory.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 Local Unset Primitive Projections. (* suppress a warning about [IsTerminalCategory] *)
 
 Notation initial_category := (nat_category 0) (only parsing).
diff --git a/theories/Categories/InitialTerminalCategory/Functors.v b/theories/Categories/InitialTerminalCategory/Functors.v
index bafaeae0bc..ea93a52a76 100644
--- a/theories/Categories/InitialTerminalCategory/Functors.v
+++ b/theories/Categories/InitialTerminalCategory/Functors.v
@@ -4,10 +4,8 @@ Require Import InitialTerminalCategory.Core.
 Require Import NatCategory.
 Require Import HoTT.Basics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Section functors.
   Variable C : PreCategory.
diff --git a/theories/Categories/InitialTerminalCategory/NaturalTransformations.v b/theories/Categories/InitialTerminalCategory/NaturalTransformations.v
index f10cbaace7..73ec8f77ea 100644
--- a/theories/Categories/InitialTerminalCategory/NaturalTransformations.v
+++ b/theories/Categories/InitialTerminalCategory/NaturalTransformations.v
@@ -3,10 +3,8 @@ Require Import Category.Core Functor.Core NaturalTransformation.Core NaturalTran
 Require Import InitialTerminalCategory.Core InitialTerminalCategory.Functors.
 Require Import Contractible.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Section NaturalTransformations.
   Variable C : PreCategory.
diff --git a/theories/Categories/InitialTerminalCategory/Pseudofunctors.v b/theories/Categories/InitialTerminalCategory/Pseudofunctors.v
index 6b49f56418..be8959085a 100644
--- a/theories/Categories/InitialTerminalCategory/Pseudofunctors.v
+++ b/theories/Categories/InitialTerminalCategory/Pseudofunctors.v
@@ -8,10 +8,8 @@ Require Import NaturalTransformation.Paths.
 Require Import NatCategory.
 Require Import PathGroupoids.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Section pseudofunctors.
   (** ** Constant functor from any terminal category *)
diff --git a/theories/Categories/KanExtensions/Core.v b/theories/Categories/KanExtensions/Core.v
index 8873096815..143bee70f1 100644
--- a/theories/Categories/KanExtensions/Core.v
+++ b/theories/Categories/KanExtensions/Core.v
@@ -4,10 +4,8 @@ Require Import FunctorCategory.Core.
 Require Import Functor.Composition.Functorial.Core.
 Require Import UniversalProperties.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope category_scope.
 
@@ -126,8 +124,6 @@ Section kan_extensions.
       p* h : C --> C' --> D
 >>
    *)
-
-
   (** *** Pullback-along functor *)
   Context `{Funext}.
   Variables C C' D : PreCategory.
diff --git a/theories/Categories/KanExtensions/Functors.v b/theories/Categories/KanExtensions/Functors.v
index 996045f6e6..f9d87d08de 100644
--- a/theories/Categories/KanExtensions/Functors.v
+++ b/theories/Categories/KanExtensions/Functors.v
@@ -5,10 +5,8 @@ Require Import Adjoint.UniversalMorphisms.Core.
 Require Import FunctorCategory.Core.
 Require Import Adjoint.Core.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Section kan_extension_functors.
   Context `{Funext}.
@@ -29,8 +27,6 @@ Section kan_extension_functors.
     : left_kan_extension_functor -| pullback_along D p
       := adjunction__of__initial_morphism has_left_kan_extensions.
   End lan.
-
-
   (** ** Right Kan extension functor *)
   Section ran.
     Context `(has_right_kan_extensions
diff --git a/theories/Categories/LaxComma/Core.v b/theories/Categories/LaxComma/Core.v
index 1c5ffbe660..1dd269f3e3 100644
--- a/theories/Categories/LaxComma/Core.v
+++ b/theories/Categories/LaxComma/Core.v
@@ -13,12 +13,8 @@ Import Functor.Identity.FunctorIdentityNotations.
 Import Pseudofunctor.Identity.PseudofunctorIdentityNotations.
 Import LaxComma.CoreLaws.LaxCommaCategory.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
-
-
 Local Open Scope morphism_scope.
 Local Open Scope category_scope.
 
@@ -94,8 +90,6 @@ Instance isstrict_oplax_comma_category `{fs : Funext} A B S T HA HB H
       hnf in *.
       destruct i, i'.
       simpl in *.
-
-
     #[export] Instance comma_category_IsCategory `{IsCategory A, IsCategory B}
     : IsCategory comma_category.
     Proof.
diff --git a/theories/Categories/LaxComma/CoreLaws.v b/theories/Categories/LaxComma/CoreLaws.v
index 9acd60b351..665fc40451 100644
--- a/theories/Categories/LaxComma/CoreLaws.v
+++ b/theories/Categories/LaxComma/CoreLaws.v
@@ -11,12 +11,8 @@ Require Import HoTT.Tactics.
 
 Import Functor.Identity.FunctorIdentityNotations.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
-
-
 Local Open Scope morphism_scope.
 Local Open Scope category_scope.
 
diff --git a/theories/Categories/LaxComma/CoreParts.v b/theories/Categories/LaxComma/CoreParts.v
index 399d1d93cf..26805ac993 100644
--- a/theories/Categories/LaxComma/CoreParts.v
+++ b/theories/Categories/LaxComma/CoreParts.v
@@ -9,12 +9,8 @@ Require Import Basics.Tactics.
 
 Import Functor.Identity.FunctorIdentityNotations.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
-
-
 Local Open Scope morphism_scope.
 Local Open Scope category_scope.
 Local Open Scope type_scope.
diff --git a/theories/Categories/Limits/Core.v b/theories/Categories/Limits/Core.v
index a0defc270e..bfe5ef0349 100644
--- a/theories/Categories/Limits/Core.v
+++ b/theories/Categories/Limits/Core.v
@@ -8,12 +8,8 @@ Local Set Warnings "-notation-overridden". (* work around bug #5567, https://coq
 Import Comma.Core.
 Local Set Warnings "notation-overridden".
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
-
-
 Local Open Scope functor_scope.
 Local Open Scope category_scope.
 
diff --git a/theories/Categories/Limits/Functors.v b/theories/Categories/Limits/Functors.v
index 736b2dfcdc..55f6a891ed 100644
--- a/theories/Categories/Limits/Functors.v
+++ b/theories/Categories/Limits/Functors.v
@@ -6,10 +6,8 @@ Require Import FunctorCategory.Core.
 Require Import Adjoint.Core.
 Require Import NatCategory.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 (** (co)limits assemble into functors *)
 
diff --git a/theories/Categories/Monoidal/MonoidalCategory.v b/theories/Categories/Monoidal/MonoidalCategory.v
index 3dd7cc345b..999daf1e0a 100644
--- a/theories/Categories/Monoidal/MonoidalCategory.v
+++ b/theories/Categories/Monoidal/MonoidalCategory.v
@@ -6,10 +6,8 @@ Require Import NaturalTransformation.Core.
 Require Import FunctorCategory.Core FunctorCategory.Morphisms.
 Require Import ProductLaws.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Section MonoidalStructure.
   Context `{Funext}.
diff --git a/theories/Categories/NatCategory.v b/theories/Categories/NatCategory.v
index fcb9c47dac..69bae24bc0 100644
--- a/theories/Categories/NatCategory.v
+++ b/theories/Categories/NatCategory.v
@@ -3,10 +3,8 @@ Require Import Category.Core DiscreteCategory IndiscreteCategory.
 Require Import Types.Unit Trunc Types.Sum Types.Empty.
 Require Import Basics.Nat.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 Local Open Scope nat_scope.
 
 Module Export Core.
diff --git a/theories/Categories/NaturalTransformation/Composition/Core.v b/theories/Categories/NaturalTransformation/Composition/Core.v
index b5b867f027..286630ad51 100644
--- a/theories/Categories/NaturalTransformation/Composition/Core.v
+++ b/theories/Categories/NaturalTransformation/Composition/Core.v
@@ -1,10 +1,8 @@
 (** * Composition of natural transformations *)
 Require Import Category.Core Functor.Core Functor.Composition.Core NaturalTransformation.Core.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope path_scope.
 Local Open Scope morphism_scope.
diff --git a/theories/Categories/NaturalTransformation/Composition/Functorial.v b/theories/Categories/NaturalTransformation/Composition/Functorial.v
index b914bd3b6d..0656db04bc 100644
--- a/theories/Categories/NaturalTransformation/Composition/Functorial.v
+++ b/theories/Categories/NaturalTransformation/Composition/Functorial.v
@@ -2,10 +2,8 @@
 Require Import Category.Core Functor.Core.
 Require Import FunctorCategory.Core Functor.Composition.Core NaturalTransformation.Composition.Core NaturalTransformation.Composition.Laws.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope functor_scope.
 
diff --git a/theories/Categories/NaturalTransformation/Composition/Laws.v b/theories/Categories/NaturalTransformation/Composition/Laws.v
index 152fb81c0e..50e90b6acc 100644
--- a/theories/Categories/NaturalTransformation/Composition/Laws.v
+++ b/theories/Categories/NaturalTransformation/Composition/Laws.v
@@ -1,10 +1,8 @@
 (** * Laws about composition of functors *)
 Require Import Category.Core Functor.Core Functor.Identity Functor.Composition.Core NaturalTransformation.Core NaturalTransformation.Identity NaturalTransformation.Composition.Core NaturalTransformation.Paths.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope morphism_scope.
 Local Open Scope natural_transformation_scope.
diff --git a/theories/Categories/NaturalTransformation/Core.v b/theories/Categories/NaturalTransformation/Core.v
index 5a03a059ba..9d3ab90699 100644
--- a/theories/Categories/NaturalTransformation/Core.v
+++ b/theories/Categories/NaturalTransformation/Core.v
@@ -1,10 +1,8 @@
 (** * Definition of natural transformation *)
 Require Import Category.Core Functor.Core.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Declare Scope natural_transformation_scope.
 Delimit Scope natural_transformation_scope with natural_transformation.
diff --git a/theories/Categories/NaturalTransformation/Dual.v b/theories/Categories/NaturalTransformation/Dual.v
index f88ae049fb..7639d04918 100644
--- a/theories/Categories/NaturalTransformation/Dual.v
+++ b/theories/Categories/NaturalTransformation/Dual.v
@@ -3,10 +3,8 @@ Require Category.Dual Functor.Dual.
 Import Category.Dual.CategoryDualNotations Functor.Dual.FunctorDualNotations.
 Require Import Category.Core Functor.Core NaturalTransformation.Core.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope category_scope.
 
diff --git a/theories/Categories/NaturalTransformation/Identity.v b/theories/Categories/NaturalTransformation/Identity.v
index 47725b2ae5..2b01041627 100644
--- a/theories/Categories/NaturalTransformation/Identity.v
+++ b/theories/Categories/NaturalTransformation/Identity.v
@@ -1,10 +1,8 @@
 (** * Identity natural transformation *)
 Require Import Category.Core Functor.Core NaturalTransformation.Core.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope morphism_scope.
 Local Open Scope path_scope.
diff --git a/theories/Categories/NaturalTransformation/Isomorphisms.v b/theories/Categories/NaturalTransformation/Isomorphisms.v
index 51bbb64cd5..eed48998dc 100644
--- a/theories/Categories/NaturalTransformation/Isomorphisms.v
+++ b/theories/Categories/NaturalTransformation/Isomorphisms.v
@@ -7,16 +7,12 @@ Require Import FunctorCategory.Core.
 Require Import NaturalTransformation.Paths.
 Require Import Basics.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope category_scope.
 Local Open Scope natural_transformation_scope.
 Local Open Scope morphism_scope.
-
-
 Local Ltac iso_whisker_t :=
   path_natural_transformation;
   try rewrite <- composition_of, <- identity_of;
diff --git a/theories/Categories/NaturalTransformation/Paths.v b/theories/Categories/NaturalTransformation/Paths.v
index 550d734ce5..5aeaeb4093 100644
--- a/theories/Categories/NaturalTransformation/Paths.v
+++ b/theories/Categories/NaturalTransformation/Paths.v
@@ -2,10 +2,8 @@
 Require Import Category.Core Functor.Core NaturalTransformation.Core.
 Require Import Equivalences HoTT.Types Trunc Basics.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope morphism_scope.
 Local Open Scope natural_transformation_scope.
@@ -16,8 +14,6 @@ Section path_natural_transformation.
   Variables C D : PreCategory.
   Variables F G : Functor C D.
 
-
-
   (** ** Equivalence between record and sigma versions of natural transformation *)
   Lemma equiv_sig_natural_transformation
   : { CO : forall x, morphism D (F x) (G x)
diff --git a/theories/Categories/NaturalTransformation/Pointwise.v b/theories/Categories/NaturalTransformation/Pointwise.v
index 8f6e583188..677b47bf98 100644
--- a/theories/Categories/NaturalTransformation/Pointwise.v
+++ b/theories/Categories/NaturalTransformation/Pointwise.v
@@ -3,10 +3,8 @@ Require Import Category.Core Functor.Core NaturalTransformation.Core.
 Require Import FunctorCategory.Core NaturalTransformation.Paths Functor.Composition.Core NaturalTransformation.Composition.Core.
 Require Import Functor.Pointwise.Core.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 (** Recall that a "pointwise" functor is a functor [Aᴮ → Cᴰ] induced
     by functors [D → B] and [A → C].  Given two functors [D → B] and a
diff --git a/theories/Categories/NaturalTransformation/Prod.v b/theories/Categories/NaturalTransformation/Prod.v
index 8da27e1367..a01e8805c3 100644
--- a/theories/Categories/NaturalTransformation/Prod.v
+++ b/theories/Categories/NaturalTransformation/Prod.v
@@ -2,10 +2,8 @@
 Require Import Category.Core Functor.Core Category.Prod Functor.Prod.Core NaturalTransformation.Core.
 Require Import Types.Prod.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 (** ** Product of natural transformations *)
 Section prod.
diff --git a/theories/Categories/NaturalTransformation/Sum.v b/theories/Categories/NaturalTransformation/Sum.v
index 10a77278de..d88feafb21 100644
--- a/theories/Categories/NaturalTransformation/Sum.v
+++ b/theories/Categories/NaturalTransformation/Sum.v
@@ -1,10 +1,8 @@
 (** * Coproduct of natural transformations *)
 Require Import Category.Sum Functor.Sum NaturalTransformation.Core.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Section sum.
   Definition sum
diff --git a/theories/Categories/ProductLaws.v b/theories/Categories/ProductLaws.v
index 6a62b0168b..03c30332ad 100644
--- a/theories/Categories/ProductLaws.v
+++ b/theories/Categories/ProductLaws.v
@@ -2,10 +2,8 @@
 Require Import HoTT.Basics HoTT.Types.
 Require Import Category.Core Functor.Core InitialTerminalCategory.Core InitialTerminalCategory.Functors Category.Prod Functor.Prod Functor.Composition.Core Functor.Identity Functor.Composition.Laws.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope category_scope.
 Local Open Scope functor_scope.
diff --git a/theories/Categories/Profunctor/Core.v b/theories/Categories/Profunctor/Core.v
index fd2c1f5cd5..46f569a544 100644
--- a/theories/Categories/Profunctor/Core.v
+++ b/theories/Categories/Profunctor/Core.v
@@ -1,10 +1,8 @@
 (** * Profunctors *)
 Require Import Category.Core Functor.Core Category.Prod Category.Dual SetCategory.Core.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Declare Scope profunctor_scope.
 Delimit Scope profunctor_scope with profunctor.
diff --git a/theories/Categories/Profunctor/Identity.v b/theories/Categories/Profunctor/Identity.v
index 8b5e4426b3..3261a7e324 100644
--- a/theories/Categories/Profunctor/Identity.v
+++ b/theories/Categories/Profunctor/Identity.v
@@ -1,10 +1,8 @@
 (** * Identity profunctor *)
 Require Import Category.Core Profunctor.Core HomFunctor.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope profunctor_scope.
 
diff --git a/theories/Categories/Profunctor/Representable.v b/theories/Categories/Profunctor/Representable.v
index 4d3145b0b4..db5c3994f9 100644
--- a/theories/Categories/Profunctor/Representable.v
+++ b/theories/Categories/Profunctor/Representable.v
@@ -1,10 +1,8 @@
 (** * Representable profunctors *)
 Require Import Category.Core Functor.Core Functor.Prod.Core Profunctor.Core Functor.Dual Profunctor.Identity Functor.Composition.Core Functor.Identity.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope functor_scope.
 Local Open Scope profunctor_scope.
diff --git a/theories/Categories/Pseudofunctor/Core.v b/theories/Categories/Pseudofunctor/Core.v
index 3fe4af3dea..e2eed64b52 100644
--- a/theories/Categories/Pseudofunctor/Core.v
+++ b/theories/Categories/Pseudofunctor/Core.v
@@ -5,10 +5,8 @@ Require Import Functor.Composition.Core Functor.Identity.
 Require Import NaturalTransformation.Composition.Core NaturalTransformation.Composition.Laws.
 Require Import FunctorCategory.Core.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope morphism_scope.
 
diff --git a/theories/Categories/Pseudofunctor/FromFunctor.v b/theories/Categories/Pseudofunctor/FromFunctor.v
index 65281cf542..5c403f698e 100644
--- a/theories/Categories/Pseudofunctor/FromFunctor.v
+++ b/theories/Categories/Pseudofunctor/FromFunctor.v
@@ -9,10 +9,8 @@ Require Import FunctorCategory.Morphisms NaturalTransformation.Isomorphisms.
 Require Import Category.Morphisms NaturalTransformation.Paths.
 Require Import Basics.PathGroupoids Basics.Trunc.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope path_scope.
 Local Open Scope morphism_scope.
diff --git a/theories/Categories/Pseudofunctor/Identity.v b/theories/Categories/Pseudofunctor/Identity.v
index 36c81072e0..2f0a15c832 100644
--- a/theories/Categories/Pseudofunctor/Identity.v
+++ b/theories/Categories/Pseudofunctor/Identity.v
@@ -14,10 +14,8 @@ Import FunctorCategory.Core.
 
 Require Import PathGroupoids.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope natural_transformation_scope.
 
diff --git a/theories/Categories/Pseudofunctor/RewriteLaws.v b/theories/Categories/Pseudofunctor/RewriteLaws.v
index 767cf2cd4b..888aec21c8 100644
--- a/theories/Categories/Pseudofunctor/RewriteLaws.v
+++ b/theories/Categories/Pseudofunctor/RewriteLaws.v
@@ -9,10 +9,8 @@ Require Import FunctorCategory.Core.
 Require Import Pseudofunctor.Core.
 Require Import HoTT.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope morphism_scope.
 
diff --git a/theories/Categories/PseudonaturalTransformation/Core.v b/theories/Categories/PseudonaturalTransformation/Core.v
index 4db9628e73..3058b3b396 100644
--- a/theories/Categories/PseudonaturalTransformation/Core.v
+++ b/theories/Categories/PseudonaturalTransformation/Core.v
@@ -6,10 +6,8 @@ Require Import Functor.Composition.Core.
 Require Import NaturalTransformation.Composition.Core NaturalTransformation.Composition.Laws.
 Require Import NaturalTransformation.Identity.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Declare Scope pseudonatural_transformation_scope.
 Delimit Scope pseudonatural_transformation_scope with pseudonatural_transformation.
@@ -64,8 +62,6 @@ Module PseudonaturalTransformationParts.
     Variable X : PreCategory.
 
     Variables F G : Pseudofunctor X.
-
-
     Definition A : PreCategory
       := (forall x : X, F x -> G x)%category.
     Definition B : PreCategory
diff --git a/theories/Categories/SemiSimplicialSets.v b/theories/Categories/SemiSimplicialSets.v
index 7e54de2095..70a940a09a 100644
--- a/theories/Categories/SemiSimplicialSets.v
+++ b/theories/Categories/SemiSimplicialSets.v
@@ -7,10 +7,8 @@ Require Import SetCategory.Core.
 Require Import SimplicialSets.
 Require Import Category.Sigma.OnMorphisms Category.Subcategory.Wide.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope category_scope.
 
diff --git a/theories/Categories/SetCategory/Core.v b/theories/Categories/SetCategory/Core.v
index cd2fb4838f..7a181be9c6 100644
--- a/theories/Categories/SetCategory/Core.v
+++ b/theories/Categories/SetCategory/Core.v
@@ -2,10 +2,8 @@
 Require Import Category.Strict.
 Require Import HoTT.Basics HoTT.Types TruncType.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Notation cat_of obj :=
   (@Build_PreCategory obj
diff --git a/theories/Categories/SetCategory/Functors/SetProp.v b/theories/Categories/SetCategory/Functors/SetProp.v
index 080bfe25c4..31e78cfac5 100644
--- a/theories/Categories/SetCategory/Functors/SetProp.v
+++ b/theories/Categories/SetCategory/Functors/SetProp.v
@@ -2,10 +2,8 @@
 Require Import Category.Core Functor.Core SetCategory.Core.
 Require Import Basics.Trunc.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Section set_coercions_definitions.
   Context `{Funext}.
diff --git a/theories/Categories/SetCategory/Morphisms.v b/theories/Categories/SetCategory/Morphisms.v
index 9007087bc5..edfd1570da 100644
--- a/theories/Categories/SetCategory/Morphisms.v
+++ b/theories/Categories/SetCategory/Morphisms.v
@@ -5,10 +5,8 @@ Require Import Category.Univalent.
 Require Import SetCategory.Core.
 Require Import HoTT.Basics HoTT.Types TruncType.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope path_scope.
 
diff --git a/theories/Categories/SimplicialSets.v b/theories/Categories/SimplicialSets.v
index 3a7dce5c22..c4b4ca9eee 100644
--- a/theories/Categories/SimplicialSets.v
+++ b/theories/Categories/SimplicialSets.v
@@ -6,10 +6,8 @@ Require Import ChainCategory FunctorCategory.Core.
 Require Import Category.Dual.
 Require Import Functor.Identity Functor.Composition.Core Functor.Composition.Laws.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope functor_scope.
 Local Open Scope category_scope.
diff --git a/theories/Categories/Structure/Core.v b/theories/Categories/Structure/Core.v
index 1d5d6ed904..b44e39daaa 100644
--- a/theories/Categories/Structure/Core.v
+++ b/theories/Categories/Structure/Core.v
@@ -2,10 +2,8 @@
 Require Import Category.Core.
 Require Import HoTT.Basics HoTT.Types HSet.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope category_scope.
 Local Open Scope morphism_scope.
@@ -119,8 +117,6 @@ Local Notation "a <=_{ x } b" := (is_structure_homomorphism _ x x (identity x) a
 Local Notation "a <= b" := (a <=_{ _ } b)%long_structure : structure_scope.
 
 (** By (iii) and (iv), this is a preorder with [P x] its type of objects. *)
-
-
 (** *** Being a structure homomorphism is a preorder *)
 #[export] Instance preorder_is_structure_homomorphism
        X (P : NotionOfStructure X) x
diff --git a/theories/Categories/Structure/IdentityPrinciple.v b/theories/Categories/Structure/IdentityPrinciple.v
index c6c2397c92..f3733ae49e 100644
--- a/theories/Categories/Structure/IdentityPrinciple.v
+++ b/theories/Categories/Structure/IdentityPrinciple.v
@@ -4,10 +4,8 @@ Require Import Structure.Core.
 Require Import Types.Sigma Trunc Equivalences.
 Require Import Basics.Iff Basics.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope path_scope.
 Local Open Scope category_scope.
diff --git a/theories/Categories/UniversalProperties.v b/theories/Categories/UniversalProperties.v
index 390852f495..c0eb603b15 100644
--- a/theories/Categories/UniversalProperties.v
+++ b/theories/Categories/UniversalProperties.v
@@ -10,10 +10,8 @@ Local Set Warnings "notation-overridden".
 Require Import Trunc Types.Sigma HoTT.Tactics.
 Require Import Basics.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope morphism_scope.
 
diff --git a/theories/Categories/Yoneda.v b/theories/Categories/Yoneda.v
index c7d76f9578..d63d3f97a2 100644
--- a/theories/Categories/Yoneda.v
+++ b/theories/Categories/Yoneda.v
@@ -12,10 +12,8 @@ Require Import FunctorCategory.Core.
 Require Import NaturalTransformation.Paths.
 Require Import HoTT.Tactics.
 
-Set Universe Polymorphism.
 Set Implicit Arguments.
 Generalizable All Variables.
-Set Asymmetric Patterns. #[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.
 
 Local Open Scope morphism_scope.
 Local Open Scope category_scope.
@@ -120,8 +118,6 @@ Section coyoneda_lemma.
                 _)
              (F a)
     := fun phi => phi a 1%morphism. *)
-
-
     Definition coyoneda_functor
     : Functor (A -> set_cat)
               (A -> set_cat)