Diff to put on top of tip (ede8193) of https://bitbucket.org/JasonGross/catdb for universe polymorphism / HoTT/coq

poylmorphic.diff

diff --git a/Adjoint.v b/Adjoint.v
index 2276dc5..bac19c8 100644
--- a/Adjoint.v
+++ b/Adjoint.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section Adjunction.
   Context `{C : @SpecializedCategory objC}.
   Context `{D : @SpecializedCategory objD}.
diff --git a/AdjointComposition.v b/AdjointComposition.v
index 4788008..b6a24b5 100644
--- a/AdjointComposition.v
+++ b/AdjointComposition.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section compose.
   Context `(C : SpecializedCategory objC).
   Context `(D : SpecializedCategory objD).
diff --git a/AdjointPointwise.v b/AdjointPointwise.v
index 7ed426a..28426ac 100644
--- a/AdjointPointwise.v
+++ b/AdjointPointwise.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section AdjointPointwise.
   Context `(C : @SpecializedCategory objC).
   Context `(D : @SpecializedCategory objD).
diff --git a/AdjointUnit.v b/AdjointUnit.v
index 11ac1f1..8866dea 100644
--- a/AdjointUnit.v
+++ b/AdjointUnit.v
@@ -3,6 +3,8 @@ Require Import Common.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 Section Adjunction.
   Variables C D : Category.
   Variable F : Functor C D.
diff --git a/AdjointUniversalMorphisms.v b/AdjointUniversalMorphisms.v
index b814b7c..3e9875a 100644
--- a/AdjointUniversalMorphisms.v
+++ b/AdjointUniversalMorphisms.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section AdjunctionUniversal.
   Context `{C : @SpecializedCategory objC}.
   Context `{D : @SpecializedCategory objD}.
diff --git a/BoolCategory.v b/BoolCategory.v
index cded94e..1562552 100644
--- a/BoolCategory.v
+++ b/BoolCategory.v
@@ -3,6 +3,8 @@ Require Import Bool.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 Section BoolCat.
   Let obj := bool.
   Let mor s d := if (implb s d) then unit else Empty_set.
diff --git a/CanonicalStructureSimplification.v b/CanonicalStructureSimplification.v
index 015511e..b9e41e7 100644
--- a/CanonicalStructureSimplification.v
+++ b/CanonicalStructureSimplification.v
@@ -4,6 +4,10 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Asymmetric Patterns.
+
+Set Universe Polymorphism.
+
 Section SimplifiedMorphism.
   Inductive ReifiedMorphism : forall objC (C : SpecializedCategory objC), C -> C -> Type :=
   | ReifiedIdentityMorphism : forall objC C x, @ReifiedMorphism objC C x x
diff --git a/Category.v b/Category.v
index a6f6332..f04de71 100644
--- a/Category.v
+++ b/Category.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Record Category := {
   CObject : Type;
 
diff --git a/CategoryEquality.v b/CategoryEquality.v
index 20db887..b13dd83 100644
--- a/CategoryEquality.v
+++ b/CategoryEquality.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Infix "==" := JMeq.
 
 Section Categories_Equal.
diff --git a/CategoryIsomorphisms.v b/CategoryIsomorphisms.v
index 9ce583e..c087d18 100644
--- a/CategoryIsomorphisms.v
+++ b/CategoryIsomorphisms.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section Category.
   Context `{C : @SpecializedCategory obj}.
 
diff --git a/CategorySchemaEquivalence.v b/CategorySchemaEquivalence.v
index fc61620..a68b60a 100644
--- a/CategorySchemaEquivalence.v
+++ b/CategorySchemaEquivalence.v
@@ -5,6 +5,8 @@ Require Import NaturalEquivalence ComputableCategory SNaturalEquivalence Computa
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 Section Schema_Category_Equivalence.
   Variable C : SmallCategory.
   Variable S : SmallSchema.
diff --git a/ChainCategory.v b/ChainCategory.v
index 720df29..c7ef51d 100644
--- a/ChainCategory.v
+++ b/ChainCategory.v
@@ -4,6 +4,8 @@ Require Import NatFacts Subcategory DefinitionSimplification.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 Section ChainCat.
   Definition OmegaCategory : @SpecializedCategory nat.
     refine (@Build_SpecializedCategory _
diff --git a/Coend.v b/Coend.v
index 9c32918..0aac5ec 100644
--- a/Coend.v
+++ b/Coend.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Ltac t := simpl in *; subst_body;
   repeat (let H := fresh in intro H; hnf in H); subst;
     simpl in *;
diff --git a/CoendFunctor.v b/CoendFunctor.v
index 8d971a2..0655065 100644
--- a/CoendFunctor.v
+++ b/CoendFunctor.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Open Scope type_scope.
 
 Section Coend.
diff --git a/CommaCategory.v b/CommaCategory.v
index 8fa6aa0..5b173e8 100644
--- a/CommaCategory.v
+++ b/CommaCategory.v
@@ -4,6 +4,8 @@ Require Import Common Notations InitialTerminalCategory SpecializedCommaCategory
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 Local Open Scope category_scope.
 
 Local Ltac fold_functor :=
diff --git a/CommaCategoryFunctorProperties.v b/CommaCategoryFunctorProperties.v
index 17ac971..effa1a6 100644
--- a/CommaCategoryFunctorProperties.v
+++ b/CommaCategoryFunctorProperties.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Open Scope category_scope.
 
 Local Ltac slice_t :=
diff --git a/CommaCategoryFunctors.v b/CommaCategoryFunctors.v
index 5d63a3a..275a5c6 100644
--- a/CommaCategoryFunctors.v
+++ b/CommaCategoryFunctors.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Notation "C / a" := (@SliceSpecializedCategoryOver _ C a) : category_scope.
 Local Notation "a \ C" := (@CosliceSpecializedCategoryOver _ C a) (at level 70) : category_scope.
 
diff --git a/Common.v b/Common.v
index 76eee20..42c54a8 100644
--- a/Common.v
+++ b/Common.v
@@ -2,6 +2,10 @@ Require Import JMeq ProofIrrelevance Eqdep_dec.
 
 Set Implicit Arguments.
 
+Set Asymmetric Patterns.
+
+Set Universe Polymorphism.
+
 Local Infix "==" := JMeq (at level 70).
 
 (* The standard library does not provide projections of [sigT2] or [sig2].
diff --git a/ComputableCategory.v b/ComputableCategory.v
index 55e2f8b..0a63c2b 100644
--- a/ComputableCategory.v
+++ b/ComputableCategory.v
@@ -3,6 +3,8 @@ Require Import Common.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 Section ComputableCategory.
   Variable I : Type.
   Variable Index2Object : I -> Type.
diff --git a/ComputableGraphCategory.v b/ComputableGraphCategory.v
index e14141b..165c44c 100644
--- a/ComputableGraphCategory.v
+++ b/ComputableGraphCategory.v
@@ -3,6 +3,8 @@ Require Import Common.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 Section ComputableGraphCategory.
   Variable I : Type.
   Variable Index2Vertex : I -> Type.
diff --git a/ComputableSchemaCategory.v b/ComputableSchemaCategory.v
index e663294..f0413e4 100644
--- a/ComputableSchemaCategory.v
+++ b/ComputableSchemaCategory.v
@@ -4,6 +4,8 @@ Require Import Common SmallTranslation EquivalenceClass.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 Section ComputableSchema.
   Variable O : Type.
   Variable Object2Sch : O -> SmallSchema.
diff --git a/Correspondences.v b/Correspondences.v
index 364fb93..1ff6fc3 100644
--- a/Correspondences.v
+++ b/Correspondences.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 (** Quoting Jacob Lurie in "Higher Topos Theory", section 2.3.1:
    Let [C] and [C'] be categories. A correspondence from [C] to [C']
    is a functor
diff --git a/DataMigrationFunctorExamples.v b/DataMigrationFunctorExamples.v
index 5de9921..63f6b28 100644
--- a/DataMigrationFunctorExamples.v
+++ b/DataMigrationFunctorExamples.v
@@ -7,6 +7,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Open Scope type_scope.
 
 Section helpers.
diff --git a/DataMigrationFunctors.v b/DataMigrationFunctors.v
index 7990063..cb8bfe5 100644
--- a/DataMigrationFunctors.v
+++ b/DataMigrationFunctors.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Infix "==" := JMeq.
 
 Local Open Scope category_scope.
diff --git a/DataMigrationFunctorsAdjoint.v b/DataMigrationFunctorsAdjoint.v
index 6e99811..ba9ffe1 100644
--- a/DataMigrationFunctorsAdjoint.v
+++ b/DataMigrationFunctorsAdjoint.v
@@ -4,6 +4,8 @@ Require Import Common Notations FunctorCategory LimitFunctors AdjointUnit Specia
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 Local Open Scope category_scope.
 (*
 Section coslice_initial.
diff --git a/DecidableComputableCategory.v b/DecidableComputableCategory.v
index 2e85239..92ff759 100644
--- a/DecidableComputableCategory.v
+++ b/DecidableComputableCategory.v
@@ -4,6 +4,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section ComputableCategory.
   Variable I : Type.
   Context `(Index2Cat : forall i : I, @SpecializedCategory (@Index2Object i)).
diff --git a/DecidableDiscreteCategory.v b/DecidableDiscreteCategory.v
index b7c2ec3..f1f8285 100644
--- a/DecidableDiscreteCategory.v
+++ b/DecidableDiscreteCategory.v
@@ -3,6 +3,8 @@ Require Import Common Notations.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 Local Hint Extern 2 (_ = _) => simpl in *; tauto.
 
 Section DCategoryDec.
diff --git a/DecidableDiscreteCategoryFunctors.v b/DecidableDiscreteCategoryFunctors.v
index 7af5afc..b4dcec3 100644
--- a/DecidableDiscreteCategoryFunctors.v
+++ b/DecidableDiscreteCategoryFunctors.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section eq_dec_prop.
   Lemma eq_dec_prop T (eq_dec : forall x y : T, {x = y} + {x <> y}) : forall x y : T, x = y \/ x <> y.
     intros x y; case (eq_dec x y); intuition.
diff --git a/DecidableSetCategory.v b/DecidableSetCategory.v
index 0237633..2c14cf0 100644
--- a/DecidableSetCategory.v
+++ b/DecidableSetCategory.v
@@ -2,6 +2,8 @@ Require Export SetCategory SigTCategory.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 (* There is a category [Set], where the objects are sets with decidable equality
    and the morphisms are set morphisms *)
 Section CSet.
diff --git a/DecidableSmallCat.v b/DecidableSmallCat.v
index 8f7ac62..628e220 100644
--- a/DecidableSmallCat.v
+++ b/DecidableSmallCat.v
@@ -4,6 +4,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section SmallCat.
   Let eq_dec_on_cat `(C : @SpecializedCategory objC) := forall x y : objC, {x = y} + {x <> y}.
 
diff --git a/DefinitionSimplification.v b/DefinitionSimplification.v
index 0c67c2c..10636e9 100644
--- a/DefinitionSimplification.v
+++ b/DefinitionSimplification.v
@@ -2,6 +2,8 @@ Require Import Common.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 (* Silly predicate that we can use to get Ltac to help us manipulate terms *)
 Definition focus A (_ : A) := True.
 
diff --git a/DiscreteCategory.v b/DiscreteCategory.v
index cf51dea..8e1b47f 100644
--- a/DiscreteCategory.v
+++ b/DiscreteCategory.v
@@ -3,6 +3,8 @@ Require Import Common.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 Section DCategory.
   Variable O : Type.
 
diff --git a/DiscreteCategoryFunctors.v b/DiscreteCategoryFunctors.v
index abe8e17..7d1116e 100644
--- a/DiscreteCategoryFunctors.v
+++ b/DiscreteCategoryFunctors.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section FunctorFromDiscrete.
   Variable O : Type.
   Context `(D : @SpecializedCategory objD).
diff --git a/DualFunctor.v b/DualFunctor.v
index 820ad5f..3b96c1e 100644
--- a/DualFunctor.v
+++ b/DualFunctor.v
@@ -2,6 +2,8 @@ Require Export Duals SmallCat.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 Section OppositeCategory.
   Definition SmallOppositeFunctor : SpecializedFunctor SmallCat SmallCat.
     refine (Build_SpecializedFunctor SmallCat SmallCat
diff --git a/Duals.v b/Duals.v
index 6bf983b..34a15ca 100644
--- a/Duals.v
+++ b/Duals.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Infix "==" := JMeq.
 
 Local Open Scope category_scope.
diff --git a/EnrichedCategory.v b/EnrichedCategory.v
index 40332e5..d81c9ae 100644
--- a/EnrichedCategory.v
+++ b/EnrichedCategory.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section EnrichedCategory.
   (** Quoting Wikipedia:
      Let [(M, ⊗, I, α, λ, ρ)] be a monoidal category.
diff --git a/Equalizer.v b/Equalizer.v
index 5bb4744..689d939 100644
--- a/Equalizer.v
+++ b/Equalizer.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section Equalizer.
   Context `(C : @SpecializedCategory objC).
   Variables A B : objC.
diff --git a/EqualizerFunctor.v b/EqualizerFunctor.v
index 1c9e39e..8be8deb 100644
--- a/EqualizerFunctor.v
+++ b/EqualizerFunctor.v
@@ -4,6 +4,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section Equalizer.
   Context `(C : @SpecializedCategory objC).
 
diff --git a/EquivalenceClass.v b/EquivalenceClass.v
index 54c99cc..be75d35 100644
--- a/EquivalenceClass.v
+++ b/EquivalenceClass.v
@@ -3,6 +3,8 @@ Require Import Common Notations.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 (**
    An equivalence class is a non-empty set of all values
    which are all equivalent to some particular value.
@@ -208,7 +210,9 @@ Section InClass_classOf.
   Qed.
 
   Let C_Equivalence : Equivalence equiv
-    := Build_Equivalence _ _ (ClassEquivalent_refl C) (ClassEquivalent_sym C) (ClassEquivalent_trans C).
+    := {| Equivalence_Reflexive := ClassEquivalent_refl C;
+          Equivalence_Symmetric := ClassEquivalent_sym C;
+          Equivalence_Transitive := ClassEquivalent_trans C |}.
 
   Definition InClass_classOf_eq' : forall v, InClass C v -> C = classOf C_Equivalence v
     := InClass_classOf_eq C_Equivalence.
diff --git a/EquivalenceRelationGenerator.v b/EquivalenceRelationGenerator.v
index cc0f296..b8ea043 100644
--- a/EquivalenceRelationGenerator.v
+++ b/EquivalenceRelationGenerator.v
@@ -3,6 +3,8 @@ Require Import Common.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 Section Gen.
   Variable A : Type.
   Variable equiv : relation A.
diff --git a/EquivalenceSet.v b/EquivalenceSet.v
index 7683a04..1fb17af 100644
--- a/EquivalenceSet.v
+++ b/EquivalenceSet.v
@@ -3,6 +3,8 @@ Require Import Common Notations.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 (**
    An equivalence class is a non-empty set of all values
    which are all equivalent to some particular value.
@@ -233,7 +235,9 @@ Section InSet_setOf.
   Qed.
 
   Let C_Equivalence : Equivalence equiv
-    := Build_Equivalence _ _ (SetEquivalent_refl C) (SetEquivalent_sym C) (SetEquivalent_trans C).
+    := {| Equivalence_Reflexive := SetEquivalent_refl C;
+          Equivalence_Symmetric := SetEquivalent_sym C;
+          Equivalence_Transitive := SetEquivalent_trans C |}.
 
   Definition InSet_setOf_eq' : forall v, InSet C v -> C = setOf C_Equivalence equiv_dec v
     := InSet_setOf_eq C_Equivalence.
diff --git a/Examples.v b/Examples.v
index ce45cbc..0c2d502 100644
--- a/Examples.v
+++ b/Examples.v
@@ -3,6 +3,9 @@ Require Import Schema Category Instance Translation.
 
 Set Implicit Arguments.
 
+Set Asymmetric Patterns.
+
+Set Universe Polymorphism.
 
 (** * The empty category *)
 
diff --git a/ExponentialLaws.v b/ExponentialLaws.v
index c2bc063..3f356de 100644
--- a/ExponentialLaws.v
+++ b/ExponentialLaws.v
@@ -8,6 +8,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Hint Immediate
       TerminalCategoryFunctorUnique InitialCategoryFunctorUnique
       InitialCategoryFunctor'Unique.
diff --git a/FEqualDep.v b/FEqualDep.v
index f9e7940..d94fe98 100644
--- a/FEqualDep.v
+++ b/FEqualDep.v
@@ -3,6 +3,10 @@ Require Import Common Notations.
 
 Set Implicit Arguments.
 
+Set Asymmetric Patterns.
+
+Set Universe Polymorphism.
+
 Local Infix "==" := JMeq.
 
 Section f_equal_dep.
diff --git a/Functor.v b/Functor.v
index c5b9fec..60917e3 100644
--- a/Functor.v
+++ b/Functor.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Infix "==" := JMeq.
 
 Section SpecializedFunctor.
diff --git a/FunctorAttributes.v b/FunctorAttributes.v
index 8ce069b..feee594 100644
--- a/FunctorAttributes.v
+++ b/FunctorAttributes.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Open Scope category_scope.
 
 Section FullFaithful.
diff --git a/FunctorCategory.v b/FunctorCategory.v
index a988cbd..9b37b14 100644
--- a/FunctorCategory.v
+++ b/FunctorCategory.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section FunctorCategory.
   Context `(C : @SpecializedCategory objC).
   Context `(D : @SpecializedCategory objD).
diff --git a/FunctorCategoryFunctorial.v b/FunctorCategoryFunctorial.v
index c3ccab0..8adf45b 100644
--- a/FunctorCategoryFunctorial.v
+++ b/FunctorCategoryFunctorial.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Open Scope category_scope.
 
 Section FunctorCategoryParts.
diff --git a/FunctorIsomorphisms.v b/FunctorIsomorphisms.v
index c15079c..a902e94 100644
--- a/FunctorIsomorphisms.v
+++ b/FunctorIsomorphisms.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Open Scope category_scope.
 
 Section FunctorIsomorphism.
diff --git a/FunctorProduct.v b/FunctorProduct.v
index 683bbe8..d66ed46 100644
--- a/FunctorProduct.v
+++ b/FunctorProduct.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section FunctorProduct.
   Context `(C : @SpecializedCategory objC).
   Context `(D : @SpecializedCategory objD).
diff --git a/FunctorialComposition.v b/FunctorialComposition.v
index 010243a..a38c032 100644
--- a/FunctorialComposition.v
+++ b/FunctorialComposition.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section FunctorialComposition.
   Context `(C : SpecializedCategory objC).
   Context `(D : SpecializedCategory objD).
diff --git a/GetArguments.v b/GetArguments.v
index f9e7a7a..396e9b0 100644
--- a/GetArguments.v
+++ b/GetArguments.v
@@ -3,6 +3,8 @@
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 (* Definitions generated by the python script
 def mk_get_arg(n, m, indent=0, prefix='Global '):
     if not isinstance(indent, str): indent = ''.join([' '] * indent)
diff --git a/Graph.v b/Graph.v
index 28025fa..f15dfff 100644
--- a/Graph.v
+++ b/Graph.v
@@ -4,6 +4,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section Graph.
   Record Graph (v : Type) := {
     Vertex :> _ := v;
diff --git a/GraphTranslation.v b/GraphTranslation.v
index 5766cba..91cc5fc 100644
--- a/GraphTranslation.v
+++ b/GraphTranslation.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Infix "==" := JMeq.
 
 Section Graphs.
diff --git a/Graphs.v b/Graphs.v
index 4b13019..39bac73 100644
--- a/Graphs.v
+++ b/Graphs.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section GraphObj.
   Context `(C : @SpecializedCategory objC).
 
diff --git a/Grothendieck.v b/Grothendieck.v
index de272b5..e245ce9 100644
--- a/Grothendieck.v
+++ b/Grothendieck.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section Grothendieck.
   (**
      Quoting Wikipedia:
diff --git a/GrothendieckCat.v b/GrothendieckCat.v
index 2a2a003..0c71310 100644
--- a/GrothendieckCat.v
+++ b/GrothendieckCat.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section Grothendieck.
   Context `(Index2Cat : forall i : Index, SpecializedCategory (Index2Object i)).
   Let Cat := @ComputableCategory _ Index2Object Index2Cat.
diff --git a/Group.v b/Group.v
index 27327e5..22eca1d 100644
--- a/Group.v
+++ b/Group.v
@@ -2,6 +2,8 @@ Require Import Notations.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 Delimit Scope group_elements_scope with group.
 Delimit Scope groups_scope with groups.
 
diff --git a/GroupCategory.v b/GroupCategory.v
index 7b4ee2d..227b122 100644
--- a/GroupCategory.v
+++ b/GroupCategory.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Ltac destruct_first_if_not_second a b :=
   (constr_eq a b; fail 1) || (let H := fresh in set (H := a : unit) in *; destruct H).
 
diff --git a/Groupoid.v b/Groupoid.v
index 3ec615a..af53692 100644
--- a/Groupoid.v
+++ b/Groupoid.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section GroupoidOf.
   Context `(C : @SpecializedCategory objC).
 
diff --git a/Hom.v b/Hom.v
index 19c6ce3..d27d79b 100644
--- a/Hom.v
+++ b/Hom.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Open Scope category_scope.
 
 (*
diff --git a/InducedLimitFunctors.v b/InducedLimitFunctors.v
index c8ea608..067e063 100644
--- a/InducedLimitFunctors.v
+++ b/InducedLimitFunctors.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section InducedFunctor.
   (* The components of the functor can be useful even if we don't have
      a category that we're coming from.  So prove them separately, so
diff --git a/InitialTerminalCategory.v b/InitialTerminalCategory.v
index 4144d52..bff6216 100644
--- a/InitialTerminalCategory.v
+++ b/InitialTerminalCategory.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section InitialTerminal.
    Definition InitialCategory : SmallSpecializedCategory _ := 0.
    Definition TerminalCategory : SmallSpecializedCategory _ := 1.
diff --git a/Instance.v b/Instance.v
index 6bc3c89..1d4f118 100644
--- a/Instance.v
+++ b/Instance.v
@@ -4,6 +4,8 @@ Require Import Common Translation SetSchema.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 Section Schema.
   Variable S : Schema.
 
diff --git a/LaxCommaCategory.v b/LaxCommaCategory.v
index 51b3903..14b84c7 100644
--- a/LaxCommaCategory.v
+++ b/LaxCommaCategory.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Open Scope category_scope.
 
 Local Ltac fold_functor :=
diff --git a/LimitFunctor2CategoryTheorems.v b/LimitFunctor2CategoryTheorems.v
index 9db7e60..c79197e 100644
--- a/LimitFunctor2CategoryTheorems.v
+++ b/LimitFunctor2CategoryTheorems.v
@@ -4,6 +4,8 @@ Require Import Common Notations FunctorCategory NaturalTransformation Hom Duals
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 Local Open Scope category_scope.
 
 (* This should be useful for proving that the data migration functors
diff --git a/LimitFunctorTheorems.v b/LimitFunctorTheorems.v
index 67ce0df..aae4baf 100644
--- a/LimitFunctorTheorems.v
+++ b/LimitFunctorTheorems.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section InducedMaps.
   (** Quoting David:
      Given a commutative triangle consisting of
diff --git a/LimitFunctors.v b/LimitFunctors.v
index a9a45bb..48ada47 100644
--- a/LimitFunctors.v
+++ b/LimitFunctors.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Open Scope category_scope.
 
 Section LimitFunctors.
diff --git a/Limits.v b/Limits.v
index 034252d..0e593a8 100644
--- a/Limits.v
+++ b/Limits.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Open Scope category_scope.
 
 Section DiagonalFunctor.
diff --git a/MetaEquivalence.v b/MetaEquivalence.v
index 0855a2b..e7bb698 100644
--- a/MetaEquivalence.v
+++ b/MetaEquivalence.v
@@ -5,6 +5,8 @@ Require Import Common.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 Section MetaEquivalence.
   Variable C D : Schema.
   Variable F G : Translation C D.
diff --git a/MetaTranslation.v b/MetaTranslation.v
index 8e325d1..c3a7386 100644
--- a/MetaTranslation.v
+++ b/MetaTranslation.v
@@ -4,6 +4,8 @@ Require Import Common.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 Section MetaTranslation.
   Variable C D : Schema.
   Variable F G : Translation C D.
diff --git a/MonoidalCategory.v b/MonoidalCategory.v
index 22123ac..0284e0f 100644
--- a/MonoidalCategory.v
+++ b/MonoidalCategory.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section PreMonoidalCategory.
   (* It's too hard to implement it all inside a record, so first we
      define everything, then we put it in a record *)
diff --git a/NatFacts.v b/NatFacts.v
index 26ec06e..f3a89cf 100644
--- a/NatFacts.v
+++ b/NatFacts.v
@@ -2,6 +2,8 @@ Require Import Omega.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 Section le_rel.
   Lemma le_refl n : n <= n. trivial. Qed.
 
diff --git a/NaturalEquivalence.v b/NaturalEquivalence.v
index fa28424..19ef5e7 100644
--- a/NaturalEquivalence.v
+++ b/NaturalEquivalence.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Ltac intro_object_of :=
   repeat match goal with
            | [ |- appcontext[ObjectOf ?G ?x] ] => unique_pose_with_body (ObjectOf G x)
diff --git a/NaturalNumbersObject.v b/NaturalNumbersObject.v
index 3404112..c6c387c 100644
--- a/NaturalNumbersObject.v
+++ b/NaturalNumbersObject.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section preobject.
   (** Quoting nCatLab (http://ncatlab.org/nlab/show/natural+numbers+object):
 
diff --git a/NaturalTransformation.v b/NaturalTransformation.v
index 1072bf9..06ba0e8 100644
--- a/NaturalTransformation.v
+++ b/NaturalTransformation.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Infix "==" := JMeq.
 
 Section SpecializedNaturalTransformation.
diff --git a/Paths.v b/Paths.v
index 28e603d..046c176 100644
--- a/Paths.v
+++ b/Paths.v
@@ -2,6 +2,10 @@ Require Import Common.
 
 Set Implicit Arguments.
 
+Set Asymmetric Patterns.
+
+Set Universe Polymorphism.
+
 Section path.
   Variable V : Type.
   Variable E : V -> V -> Type.
diff --git a/PathsCategory.v b/PathsCategory.v
index 047aed0..8317ce7 100644
--- a/PathsCategory.v
+++ b/PathsCategory.v
@@ -3,6 +3,8 @@ Require Import Common.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 Section PCategory.
   Variable V : Type.
   Variable E : V -> V -> Type.
diff --git a/PathsCategoryFunctors.v b/PathsCategoryFunctors.v
index 1d9cf3d..a5c4895 100644
--- a/PathsCategoryFunctors.v
+++ b/PathsCategoryFunctors.v
@@ -6,6 +6,10 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Asymmetric Patterns.
+
+Set Universe Polymorphism.
+
 Section FunctorFromPaths.
   Variable V : Type.
   Variable E : V -> V -> Type.
diff --git a/ProductCategory.v b/ProductCategory.v
index 812569b..ff5715e 100644
--- a/ProductCategory.v
+++ b/ProductCategory.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section ProductCategory.
   Context `(C : @SpecializedCategory objC).
   Context `(D : @SpecializedCategory objD).
diff --git a/ProductFunctors.v b/ProductFunctors.v
index 3127df3..e90796a 100644
--- a/ProductFunctors.v
+++ b/ProductFunctors.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section Products.
   Context `{C : @SpecializedCategory objC}.
   Variable I : Type.
diff --git a/ProductInducedFunctors.v b/ProductInducedFunctors.v
index f84eacc..816095b 100644
--- a/ProductInducedFunctors.v
+++ b/ProductInducedFunctors.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Ltac t :=
   intros; simpl; repeat (rewrite <- FCompositionOf || rewrite <- FIdentityOf);
   apply f_equal; expand; autorewrite with morphism;
diff --git a/ProductLaws.v b/ProductLaws.v
index 6eaf283..4ec5bcb 100644
--- a/ProductLaws.v
+++ b/ProductLaws.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Open Scope category_scope.
 
 Section swap.
diff --git a/ProductNaturalTransformation.v b/ProductNaturalTransformation.v
index d2fb45a..2f82905 100644
--- a/ProductNaturalTransformation.v
+++ b/ProductNaturalTransformation.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section ProductNaturalTransformation.
   Context `{A : @SpecializedCategory objA}.
   Context `{B : @SpecializedCategory objB}.
diff --git a/Products.v b/Products.v
index 011d5e9..1bc46f3 100644
--- a/Products.v
+++ b/Products.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section Products.
   Context `{C : @SpecializedCategory objC}.
   Variable I : Type.
diff --git a/Pullback.v b/Pullback.v
index 395aa21..96d8ccb 100644
--- a/Pullback.v
+++ b/Pullback.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section Pullback.
   (* Quoting nCatLab (http://ncatlab.org/nlab/show/pullback):
 
diff --git a/PullbackFunctor.v b/PullbackFunctor.v
index c0e67c4..262a4c4 100644
--- a/PullbackFunctor.v
+++ b/PullbackFunctor.v
@@ -4,6 +4,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section Equalizer.
   Context `(C : @SpecializedCategory objC).
 
diff --git a/Schema.v b/Schema.v
index f9215a5..f3846f8 100644
--- a/Schema.v
+++ b/Schema.v
@@ -4,6 +4,10 @@ Require Import Common Eqdep.
 
 Set Implicit Arguments.
 
+Set Asymmetric Patterns.
+
+Set Universe Polymorphism.
+
 Section path'.
   Variable V : Type.
   Variable E : V -> V -> Type.
diff --git a/SemiSimplicialSets.v b/SemiSimplicialSets.v
index 4200796..3c88732 100644
--- a/SemiSimplicialSets.v
+++ b/SemiSimplicialSets.v
@@ -5,6 +5,8 @@ Generalizable Variables objC.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 Local Notation "'Δ'" := SimplexCategory : category_scope.
 
 Section SemiSimplicialSets.
diff --git a/SetCategory.v b/SetCategory.v
index 3d22620..9c1c704 100644
--- a/SetCategory.v
+++ b/SetCategory.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Notation IndexedCatOf obj coerce := (@Build_SpecializedCategory obj
                                                                 (fun s d => coerce s -> coerce d)
                                                                 (fun _ => (fun x => x))
diff --git a/SetCategoryFacts.v b/SetCategoryFacts.v
index f279f5d..34066b1 100644
--- a/SetCategoryFacts.v
+++ b/SetCategoryFacts.v
@@ -4,6 +4,8 @@ Require Import Common NaturalNumbersObject.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 Notation IndexedTInitialOf obj coerce initial_obj :=
   ((fun o => exist _
                    (fun x : initial_obj%type => match x with end)
diff --git a/SetCategoryProductFunctor.v b/SetCategoryProductFunctor.v
index 65ed732..943f22d 100644
--- a/SetCategoryProductFunctor.v
+++ b/SetCategoryProductFunctor.v
@@ -4,6 +4,8 @@ Require Import Common Notations.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 Local Close Scope nat_scope.
 
 Section ProductFunctor.
diff --git a/SetColimits.v b/SetColimits.v
index c2c44ee..e323585 100644
--- a/SetColimits.v
+++ b/SetColimits.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Ltac colimit_morphism_t chooser_respectful :=
   simpl; intros; hnf;
   repeat (apply functional_extensionality_dep; intro);
diff --git a/SetLimits.v b/SetLimits.v
index c3d3f98..199fb49 100644
--- a/SetLimits.v
+++ b/SetLimits.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Ltac limit_t :=
   repeat (repeat intro; repeat split);
   simpl in *;
diff --git a/SigCategory.v b/SigCategory.v
index f827b85..0808f51 100644
--- a/SigCategory.v
+++ b/SigCategory.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Infix "==" := JMeq.
 
 Local Ltac faithful_t :=
diff --git a/SigSigTCategory.v b/SigSigTCategory.v
index 9fe869a..f5d9328 100644
--- a/SigSigTCategory.v
+++ b/SigSigTCategory.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Infix "==" := JMeq.
 
 Section sig_sigT_obj_mor.
diff --git a/SigTCategory.v b/SigTCategory.v
index 56da5a6..3453f98 100644
--- a/SigTCategory.v
+++ b/SigTCategory.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Infix "==" := JMeq.
 
 Local Ltac faithful_t :=
diff --git a/SigTInducedFunctors.v b/SigTInducedFunctors.v
index b3a6f18..e57bdd4 100644
--- a/SigTInducedFunctors.v
+++ b/SigTInducedFunctors.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section T2.
   (* use dummy variables so we don't have to specify the types of
      all these hypotheses *)
diff --git a/SigTSigCategory.v b/SigTSigCategory.v
index 5cca04e..7ddae19 100644
--- a/SigTSigCategory.v
+++ b/SigTSigCategory.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Infix "==" := JMeq.
 
 Section sigT_sig_obj_mor.
diff --git a/SigTSigInducedFunctors.v b/SigTSigInducedFunctors.v
index 6c4f13a..08164a6 100644
--- a/SigTSigInducedFunctors.v
+++ b/SigTSigInducedFunctors.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section T2.
   (* use dummy variables so we don't have to specify the types of
      all these hypotheses *)
diff --git a/SimplicialSets.v b/SimplicialSets.v
index b0ffe54..077d24a 100644
--- a/SimplicialSets.v
+++ b/SimplicialSets.v
@@ -5,6 +5,8 @@ Generalizable Variables objC.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 Section SimplicialSets.
   Definition SimplexCategory := @ComputableCategory nat _ (fun n => [n])%category.
   Local Notation "'Δ'" := SimplexCategory : category_scope.
diff --git a/SmallCat.v b/SmallCat.v
index 80bfffc..8f41a74 100644
--- a/SmallCat.v
+++ b/SmallCat.v
@@ -4,6 +4,8 @@ Require Import Common FEqualDep.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 Section SmallCat.
   Definition SmallCat := ComputableCategory _ SUnderlyingCategory.
   Definition LocallySmallCat := ComputableCategory _ LSUnderlyingCategory.
diff --git a/SmallSchema.v b/SmallSchema.v
index ab1ae30..4eb6e94 100644
--- a/SmallSchema.v
+++ b/SmallSchema.v
@@ -4,6 +4,8 @@ Require Import Common FEqualDep.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 Record SmallSchema := {
   SVertex :> Set;
   SEdge : SVertex -> SVertex -> Set;
diff --git a/SmallTranslation.v b/SmallTranslation.v
index d2b38b0..d46fee4 100644
--- a/SmallTranslation.v
+++ b/SmallTranslation.v
@@ -4,6 +4,8 @@ Require Import Common Notations FEqualDep.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 Local Infix "==" := JMeq.
 
 Section SmallSchemas.
diff --git a/SpecializedCategory.v b/SpecializedCategory.v
index 8f3d682..f4f99b0 100644
--- a/SpecializedCategory.v
+++ b/SpecializedCategory.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Infix "==" := JMeq.
 
 Record ComputationalCategory (obj : Type) :=
diff --git a/SpecializedCommaCategory.v b/SpecializedCommaCategory.v
index e68bda2..0a2bd89 100644
--- a/SpecializedCommaCategory.v
+++ b/SpecializedCommaCategory.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Infix "==" := JMeq.
 
 Local Open Scope category_scope.
diff --git a/SpecializedLaxCommaCategory.v b/SpecializedLaxCommaCategory.v
index a7e0ce7..529e8bd 100644
--- a/SpecializedLaxCommaCategory.v
+++ b/SpecializedLaxCommaCategory.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Open Scope category_scope.
 
 Section LaxSliceSpecializedCategory.
diff --git a/StructureEquality.v b/StructureEquality.v
index e4914ba..8bcb238 100644
--- a/StructureEquality.v
+++ b/StructureEquality.v
@@ -3,6 +3,8 @@ Require Import Common Notations FEqualDep.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 Local Infix "==" := JMeq.
 
 Ltac structures_eq_simpl_step_with tac := intros; simpl in *;
diff --git a/Subcategory.v b/Subcategory.v
index 968617b..92abe1a 100644
--- a/Subcategory.v
+++ b/Subcategory.v
@@ -2,6 +2,8 @@ Require Export SigCategory.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 Definition Subcategory := @SpecializedCategory_sig.
 Definition SubcategoryInclusionFunctor := @proj1_sig_functor.
 Definition FullSubcategory := @SpecializedCategory_sig_obj.
diff --git a/SubobjectClassifier.v b/SubobjectClassifier.v
index 85638bf..e48fb15 100644
--- a/SubobjectClassifier.v
+++ b/SubobjectClassifier.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section subobject_classifier.
   (** Quoting Wikipedia:
 
diff --git a/SumCategory.v b/SumCategory.v
index f4924ea..1e0c359 100644
--- a/SumCategory.v
+++ b/SumCategory.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section SumCategory.
   Context `(C : @SpecializedCategory objC).
   Context `(D : @SpecializedCategory objD).
diff --git a/SumInducedFunctors.v b/SumInducedFunctors.v
index 7187254..6417e16 100644
--- a/SumInducedFunctors.v
+++ b/SumInducedFunctors.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section SumCategoryFunctors.
   Section sum_functor.
     Context `(C : @SpecializedCategory objC).
diff --git a/Theorems.v b/Theorems.v
index b5f8c6c..8775124 100644
--- a/Theorems.v
+++ b/Theorems.v
@@ -3,6 +3,8 @@ Require Import Common Schema Category Instance Translation.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 Section Translation_Instance.
   Variables C D : Schema.
   Variable F : Translation C D.
diff --git a/Translation.v b/Translation.v
index 0d7d456..23e3ec6 100644
--- a/Translation.v
+++ b/Translation.v
@@ -4,6 +4,10 @@ Require Export Schema.
 
 Set Implicit Arguments.
 
+Set Asymmetric Patterns.
+
+Set Universe Polymorphism.
+
 Local Infix "==" := JMeq.
 
 Section Schemas.
diff --git a/TypeclassSimplification.v b/TypeclassSimplification.v
index 7b62935..c597c72 100644
--- a/TypeclassSimplification.v
+++ b/TypeclassSimplification.v
@@ -4,6 +4,10 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Asymmetric Patterns.
+
+Set Universe Polymorphism.
+
 Section SimplifiedMorphism.
   Inductive ReifiedMorphism : forall objC (C : SpecializedCategory objC), C -> C -> Type :=
   | ReifiedIdentityMorphism : forall objC C x, @ReifiedMorphism objC C x x
diff --git a/TypeclassUnreifiedSimplification.v b/TypeclassUnreifiedSimplification.v
index 6ca5d8e..eb22615 100644
--- a/TypeclassUnreifiedSimplification.v
+++ b/TypeclassUnreifiedSimplification.v
@@ -5,6 +5,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Section SimplifiedMorphism.
   Section single_category_definition.
     Context `{C : SpecializedCategory objC}.
diff --git a/UniversalProperties.v b/UniversalProperties.v
index 5fc1231..dce62ff 100644
--- a/UniversalProperties.v
+++ b/UniversalProperties.v
@@ -3,6 +3,8 @@ Require Import Common Notations DefinitionSimplification Eqdep.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 Section UniversalMorphism.
   (**
      Quoting Wikipedia:
diff --git a/Yoneda.v b/Yoneda.v
index a2ed914..7685136 100644
--- a/Yoneda.v
+++ b/Yoneda.v
@@ -6,6 +6,8 @@ Set Implicit Arguments.
 
 Generalizable All Variables.
 
+Set Universe Polymorphism.
+
 Local Open Scope category_scope.
 
 Local Ltac apply_commutes_by_transitivity_and_solve_with tac :=
diff --git a/dbs.v b/dbs.v
index c6865f0..73c3a12 100644
--- a/dbs.v
+++ b/dbs.v
@@ -2,6 +2,8 @@ Require Import List.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 
 (** * Types *)
 
diff --git a/deplists.v b/deplists.v
index ae0ca2b..6527a04 100644
--- a/deplists.v
+++ b/deplists.v
@@ -2,6 +2,8 @@ Require Import List String.
 
 Set Implicit Arguments.
 
+Set Universe Polymorphism.
+
 (* Largely copied from CPDT *)
 Section ilist.
   Variable A : Type.