Add more regression tests for univ poly/prim proj

hese regression tests are aggregated from the various bugs I (and
others) have reported on https://github.com/HoTT/coq/issues relating to
universe polymorphism, primitive projections, and eta for records.

These are the tests that trunk currently fails.

I'm not sure about the naming scheme (HoTT_coq_###.v, where ### is the
number of the issue in GitHub), but I couldn't think of a better one.

42 files changed, 2893 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/3230.v b/test-suite/bugs/closed/3230.v
new file mode 100644
index 000000000..265310b1a
--- /dev/null
+++ b/test-suite/bugs/closed/3230.v
@@ -0,0 +1,14 @@
+Structure type : Type := Pack { ob : Type }.
+Polymorphic Record category := { foo : Type }.
+Definition FuncComp := Pack category.
+Axiom C : category.
+
+Check (C : ob FuncComp). (* OK *)
+
+Canonical Structure FuncComp.
+
+Check (C : ob FuncComp).
+(* Toplevel input, characters 15-39:
+Error:
+The term "C" has type "category" while it is expected to have type
+ "ob FuncComp". *)
diff --git a/test-suite/bugs/closed/HoTT_coq_007.v b/test-suite/bugs/closed/HoTT_coq_007.v
new file mode 100644
index 000000000..9c360c9f4
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_007.v
@@ -0,0 +1,110 @@
+Module Comment1.
+  Set Implicit Arguments.
+
+  Polymorphic Record Category (obj : Type) :=
+    {
+      Morphism : obj -> obj -> Type;
+      Identity : forall o, Morphism o o
+    }.
+
+  Polymorphic Record Functor objC (C :Category objC) objD (D : Category objD) :=
+    {
+      ObjectOf :> objC -> objD;
+      MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d);
+      FIdentityOf : forall o, MorphismOf _ _ (C.(Identity) o) = D.(Identity) (ObjectOf o)
+    }.
+
+  Create HintDb functor discriminated.
+
+  Hint Rewrite @FIdentityOf : functor.
+
+  Polymorphic Definition ComposeFunctors objC C objD D objE E (G : @Functor objD D objE E) (F : @Functor objC C objD D) : Functor C E.
+  refine {| ObjectOf := (fun c => G (F c));
+            MorphismOf := (fun _ _ m => G.(MorphismOf) _ _ (F.(MorphismOf) _ _ m))
+         |};
+    intros; autorewrite with functor; reflexivity.
+  Defined.
+
+  Definition Cat0 : Category Empty_set.
+    refine {|
+        Morphism := fun s d : Empty_set => s = d;
+        Identity := fun o : Empty_set => eq_refl
+      |};
+    admit.
+  Defined.
+
+  Set Printing All.
+  Set Printing Universes.
+
+  Lemma foo objC (C : @Category objC) (C0 : Category (Functor Cat0 C)) (x : Functor Cat0 Cat0) : forall (y : Functor C0 Cat0) z, (ComposeFunctors y z = x).
+    intro. (* Illegal application (Type Error) *)
+  Abort.
+End Comment1.
+
+Module Comment2.
+  Set Implicit Arguments.
+
+  Polymorphic Record Category (obj : Type) :=
+    {
+      Morphism : obj -> obj -> Type;
+
+      Identity : forall o, Morphism o o;
+      Compose : forall s d d2, Morphism d d2 -> Morphism s d -> Morphism s d2;
+
+      LeftIdentity : forall a b (f : Morphism a b), Compose (Identity b) f = f
+    }.
+
+  Polymorphic Record Functor objC (C : Category objC) objD (D : Category objD) :=
+    {
+      ObjectOf : objC -> objD;
+      MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d)
+    }.
+
+  Create HintDb morphism discriminated.
+
+  Polymorphic Hint Resolve @LeftIdentity : morphism.
+
+  Polymorphic Definition ProductCategory objC (C : Category objC) objD (D : Category objD) : @Category (objC * objD)%type.
+  refine {|
+      Morphism := (fun s d => (C.(Morphism) (fst s) (fst d) * D.(Morphism) (snd s) (snd d))%type);
+      Identity := (fun o => (Identity _ (fst o), Identity _ (snd o)));
+      Compose := (fun (s d d2 : (objC * objD)%type) m2 m1 => (C.(Compose) _ _ _ (fst m2) (fst m1), D.(Compose) _ _ _ (snd m2) (snd m1)))
+    |};
+    intros; apply injective_projections; simpl; auto with morphism. (* Replacing [auto with morphism] with [apply @LeftIdentity] removes the error *)
+  Defined.
+
+  Polymorphic Definition Cat0 : Category Empty_set.
+  refine {|
+      Morphism := fun s d : Empty_set => s = d;
+      Identity := fun o : Empty_set => eq_refl;
+      Compose := fun s d d2 m0 m1 => eq_trans m1 m0
+    |};
+    admit.
+  Defined.
+
+  Set Printing All.
+  Set Printing Universes.
+  Polymorphic Definition ProductLaw0Functor (objC : Type) (C : Category objC) : Functor (ProductCategory C Cat0) Cat0.
+  refine (Build_Functor (ProductCategory C Cat0) Cat0 _ _). (* Toplevel input, characters 15-71:
+Error: Refiner was given an argument
+ "prod (* Top.2289 Top.2289 *) objC Empty_set" of type
+"Type (* Top.2289 *)" instead of "Set". *)
+  Abort.
+  Polymorphic Definition ProductLaw0Functor (objC : Type) (C : Category objC) : Functor (ProductCategory C Cat0) Cat0.
+  econstructor. (* Toplevel input, characters 0-12:
+Error: No applicable tactic.
+                 *)
+  Abort.
+End Comment2.
+
+
+Module Comment3.
+  Polymorphic Lemma foo {obj : Type} : 1 = 1.
+  trivial.
+  Qed.
+
+  Polymorphic Hint Resolve foo. (* success *)
+  Polymorphic Hint Rewrite @foo. (* Success *)
+  Polymorphic Hint Resolve @foo. (* Error: @foo is a term and cannot be made a polymorphic hint, only global references can be polymorphic hints. *)
+  Polymorphic Hint Rewrite foo. (* Error: Cannot infer the implicit parameter obj of foo. *)
+End Comment3.
diff --git a/test-suite/bugs/closed/HoTT_coq_014.v b/test-suite/bugs/closed/HoTT_coq_014.v
new file mode 100644
index 000000000..1fd7e251f
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_014.v
@@ -0,0 +1,164 @@
+Set Implicit Arguments.
+Generalizable All Variables.
+
+
+Polymorphic Record SpecializedCategory (obj : Type) := Build_SpecializedCategory' {
+  Object :> _ := obj;
+  Morphism' : obj -> obj -> Type;
+
+  Identity' : forall o, Morphism' o o;
+  Compose' : forall s d d', Morphism' d d' -> Morphism' s d -> Morphism' s d'
+}.
+
+Polymorphic Definition Morphism obj (C : @SpecializedCategory obj) : forall s d : C, _ := Eval cbv beta delta [Morphism'] in C.(Morphism').
+
+(* eh, I'm not terribly happy.  meh. *)
+Polymorphic Definition SmallSpecializedCategory (obj : Set) (*mor : obj -> obj -> Set*) := SpecializedCategory obj.
+Identity Coercion SmallSpecializedCategory_LocallySmallSpecializedCategory_Id : SmallSpecializedCategory >-> SpecializedCategory.
+
+Polymorphic Record Category := {
+  CObject : Type;
+
+  UnderlyingCategory :> @SpecializedCategory CObject
+}.
+
+Polymorphic Definition GeneralizeCategory `(C : @SpecializedCategory obj) : Category.
+  refine {| CObject := C.(Object) |}; auto.
+Defined.
+
+Coercion GeneralizeCategory : SpecializedCategory >-> Category.
+
+
+
+Section SpecializedFunctor.
+  Set Universe Polymorphism.
+  Context `(C : @SpecializedCategory objC).
+  Context `(D : @SpecializedCategory objD).
+  Unset Universe Polymorphism.
+
+  Polymorphic Record SpecializedFunctor := {
+    ObjectOf' : objC -> objD;
+    MorphismOf' : forall s d, C.(Morphism') s d -> D.(Morphism') (ObjectOf' s) (ObjectOf' d);
+    FCompositionOf' : forall s d d' (m1 : C.(Morphism') s d) (m2: C.(Morphism') d d'),
+      MorphismOf' _ _ (C.(Compose') _ _ _ m2 m1) = D.(Compose') _ _ _ (MorphismOf' _ _ m2) (MorphismOf' _ _ m1);
+    FIdentityOf' : forall o, MorphismOf' _ _ (C.(Identity') o) = D.(Identity') (ObjectOf' o)
+  }.
+End SpecializedFunctor.
+
+Global Coercion ObjectOf' : SpecializedFunctor >-> Funclass.
+(*Unset Universe Polymorphism.*)
+Section Functor.
+  Variable C D : Category.
+
+  Polymorphic Definition Functor := SpecializedFunctor C D.
+End Functor.
+
+Identity Coercion Functor_SpecializedFunctor_Id : Functor >-> SpecializedFunctor.
+Polymorphic Definition GeneralizeFunctor objC C objD D (F : @SpecializedFunctor objC C objD D) : Functor C D := F.
+Coercion GeneralizeFunctor : SpecializedFunctor >-> Functor.
+
+Arguments SpecializedFunctor {objC} C {objD} D.
+
+
+Polymorphic Record SmallCategory := {
+  SObject : Set;
+
+  SUnderlyingCategory :> @SmallSpecializedCategory SObject
+}.
+
+Polymorphic Definition GeneralizeSmallCategory `(C : @SmallSpecializedCategory obj) : SmallCategory.
+  refine {| SObject := obj |}; destruct C; econstructor; eassumption.
+Defined.
+
+Coercion GeneralizeSmallCategory : SmallSpecializedCategory >-> SmallCategory.
+
+Bind Scope category_scope with SmallCategory.
+
+
+Polymorphic Definition TypeCat : @SpecializedCategory Type := (@Build_SpecializedCategory' Type
+                                                                                          (fun s d => s -> d)
+                                                                                          (fun _ => (fun x => x))
+                                                                                          (fun _ _ _ f g => (fun x => f (g x)))).
+(*Unset Universe Polymorphism.*)
+Polymorphic Definition FunctorCategory objC (C : @SpecializedCategory objC) objD (D : @SpecializedCategory objD) :
+  @SpecializedCategory (SpecializedFunctor C D).
+Admitted.
+
+Polymorphic Definition DiscreteCategory (O : Type) : @SpecializedCategory O.
+Admitted.
+
+Polymorphic Definition ComputableCategory (I : Type) (Index2Object : I -> Type) (Index2Cat : forall i : I, @SpecializedCategory (@Index2Object i)) :
+  @SpecializedCategory I.
+Admitted.
+
+Polymorphic Definition is_unique (A : Type) (x : A) := forall x' : A, x' = x.
+
+Polymorphic Definition InitialObject obj {C : SpecializedCategory obj} (o : C) :=
+    forall o', { m : C.(Morphism) o o' | is_unique m }.
+
+Polymorphic Definition SmallCat := ComputableCategory _ SUnderlyingCategory.
+
+Lemma InitialCategory_Initial : InitialObject (C := SmallCat) (DiscreteCategory Empty_set : SmallSpecializedCategory _).
+  admit.
+Qed.
+
+
+Section GraphObj.
+  Context `(C : @SpecializedCategory objC).
+
+  Inductive GraphIndex := GraphIndexSource | GraphIndexTarget.
+
+  Polymorphic Definition GraphIndex_Morphism (a b : GraphIndex) : Set :=
+    match (a, b) with
+      | (GraphIndexSource, GraphIndexSource) => unit
+      | (GraphIndexTarget, GraphIndexTarget) => unit
+      | (GraphIndexTarget, GraphIndexSource) => Empty_set
+      | (GraphIndexSource, GraphIndexTarget) => GraphIndex
+    end.
+
+  Global Arguments GraphIndex_Morphism a b /.
+
+  Polymorphic Definition GraphIndex_Compose s d d' (m1 : GraphIndex_Morphism d d') (m2 : GraphIndex_Morphism s d) :
+    GraphIndex_Morphism s d'.
+  Admitted.
+
+  Polymorphic Definition GraphIndexingCategory : @SpecializedCategory GraphIndex.
+    refine {|
+      Morphism' := GraphIndex_Morphism;
+      Identity' := (fun x => match x with GraphIndexSource => tt | GraphIndexTarget => tt end);
+      Compose' := GraphIndex_Compose
+    |};
+    admit.
+  Defined.
+
+  Polymorphic Definition UnderlyingGraph_ObjectOf x :=
+    match x with
+      | GraphIndexSource => { sd : objC * objC & C.(Morphism) (fst sd) (snd sd) }
+      | GraphIndexTarget => objC
+    end.
+
+  Global Arguments UnderlyingGraph_ObjectOf x /.
+
+  Polymorphic Definition UnderlyingGraph_MorphismOf s d (m : Morphism GraphIndexingCategory s d) :
+    UnderlyingGraph_ObjectOf s -> UnderlyingGraph_ObjectOf d.
+  Admitted.
+
+  Polymorphic Definition UnderlyingGraph : SpecializedFunctor GraphIndexingCategory TypeCat.
+  Proof.
+    match goal with
+      | [ |- SpecializedFunctor ?C ?D ] =>
+        refine (Build_SpecializedFunctor C D
+          UnderlyingGraph_ObjectOf
+          UnderlyingGraph_MorphismOf
+          _
+          _
+        )
+    end;
+    admit.
+  Defined.
+End GraphObj.
+
+
+Polymorphic Definition UnderlyingGraphFunctor_MorphismOf (C D : SmallCategory) (F : SpecializedFunctor C D) :
+  Morphism (FunctorCategory TypeCat GraphIndexingCategory) (UnderlyingGraph C) (UnderlyingGraph D). (* Anomaly: apply_coercion. Please report.*)
+Admitted.
diff --git a/test-suite/bugs/closed/HoTT_coq_020.v b/test-suite/bugs/closed/HoTT_coq_020.v
new file mode 100644
index 000000000..6747d6af2
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_020.v
@@ -0,0 +1,83 @@
+Set Implicit Arguments.
+
+Generalizable All Variables.
+
+Set Asymmetric Patterns.
+
+Polymorphic Record Category (obj : Type) :=
+  Build_Category {
+      Object :> _ := obj;
+      Morphism : obj -> obj -> Type;
+
+      Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
+    }.
+
+Polymorphic Record Functor objC (C : Category objC) objD (D : Category objD) :=
+  { ObjectOf :> objC -> objD }.
+
+Polymorphic Record NaturalTransformation objC C objD D (F G : Functor (objC := objC) C (objD := objD) D) :=
+  { ComponentsOf' :> forall c, D.(Morphism) (F.(ObjectOf) c) (G.(ObjectOf) c);
+    Commutes' : forall s d (m : C.(Morphism) s d), ComponentsOf' s = ComponentsOf' s }.
+
+Ltac present_obj from to :=
+  repeat match goal with
+           | [ _ : appcontext[from ?obj ?C] |- _ ] => progress change (from obj C) with (to obj C) in *
+           | [ |- appcontext[from ?obj ?C] ] => progress change (from obj C) with (to obj C) in *
+         end.
+
+Section NaturalTransformationComposition.
+  Set Universe Polymorphism.
+  Context `(C : @Category objC).
+  Context `(D : @Category objD).
+  Context `(E : @Category objE).
+  Variables F F' F'' : Functor C D.
+  Unset Universe Polymorphism.
+
+  Polymorphic Definition NTComposeT (T' : NaturalTransformation F' F'') (T : NaturalTransformation F F') :
+    NaturalTransformation F F''.
+    exists (fun c => Compose _ _ _ _ (T' c) (T c)).
+    progress present_obj @Morphism @Morphism. (* removing this line makes the error go away *)
+    intros. (* removing this line makes the error go away *)
+    admit.
+  Defined.
+End NaturalTransformationComposition.
+
+
+Polymorphic Definition FunctorCategory objC (C : Category objC) objD (D : Category objD) :
+  @Category (Functor C D)
+  := @Build_Category (Functor C D)
+                     (NaturalTransformation (C := C) (D := D))
+                     (NTComposeT (C := C) (D := D)).
+
+Polymorphic Definition Cat0 : Category Empty_set
+  := @Build_Category Empty_set
+                     (@eq _)
+                     (fun x => match x return _ with end).
+
+Polymorphic Definition FunctorFrom0 objC (C : Category objC) : Functor Cat0 C
+  := Build_Functor Cat0 C (fun x => match x with end).
+
+Section Law0.
+  Variable objC : Type.
+  Variable C : Category objC.
+
+  Set Printing All.
+  Set Printing Universes.
+  Set Printing Existential Instances.
+
+  Polymorphic Definition ExponentialLaw0Functor_Inverse_ObjectOf : Object (FunctorCategory Cat0 C).
+    hnf.
+    refine (@FunctorFrom0 _ _).
+    (* Toplevel input, characters 23-40:
+Error:
+In environment
+objC : Type (* Top.61069 *)
+C : Category (* Top.61069 Top.61071 *) objC
+The term
+ "@FunctorFrom0 (* Top.61077 Top.61078 *) ?69 (* [objC, C] *)
+    ?70 (* [objC, C] *)" has type
+ "@Functor (* Set Prop Top.61077 Top.61078 *) Empty_set Cat0
+    ?69 (* [objC, C] *) ?70 (* [objC, C] *)"
+ while it is expected to have type
+ "@Functor (* Set Prop Set Prop *) Empty_set Cat0 objC C".
+*)
diff --git a/test-suite/bugs/closed/HoTT_coq_027.v b/test-suite/bugs/closed/HoTT_coq_027.v
new file mode 100644
index 000000000..8132f51d2
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_027.v
@@ -0,0 +1,75 @@
+Set Implicit Arguments.
+Generalizable All Variables.
+Set Asymmetric Patterns.
+Set Universe Polymorphism.
+
+Record Category (obj : Type) := { Morphism : obj -> obj -> Type }.
+
+Record Functor `(C : Category objC) `(D : Category objD) :=
+  { ObjectOf :> objC -> objD;
+    MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d) }.
+
+Definition TypeCat : @Category Type := @Build_Category Type (fun s d => s -> d).
+Definition SetCat : @Category Set := @Build_Category Set (fun s d => s -> d).
+
+Definition FunctorToSet `(C : @Category objC) := Functor C SetCat.
+Definition FunctorToType `(C : @Category objC) := Functor C TypeCat.
+
+(* Removing the following line, as well as the [Definition] and [Identity Coercion] immediately following it, makes the file go through *)
+Identity Coercion FunctorToType_Id : FunctorToType >-> Functor.
+
+Definition FunctorTo_Set2Type `(C : @Category objC) (F : FunctorToSet C)
+: FunctorToType C.
+  refine (@Build_Functor _ C _ TypeCat
+                         (fun x => F.(ObjectOf) x)
+                         (fun s d m => F.(MorphismOf) _ _ m)).
+Defined. (* Toplevel input, characters 0-8:
+Error:
+The term
+ "fun (objC : Type) (C : Category objC) (F : FunctorToSet C) =>
+  {|
+  ObjectOf := fun x : objC => F x;
+  MorphismOf := fun (s d : objC) (m : Morphism C s d) => MorphismOf F s d m |}"
+has type
+ "forall (objC : Type) (C : Category objC),
+  FunctorToSet C -> Functor C TypeCat" while it is expected to have type
+ "forall (objC : Type) (C : Category objC), FunctorToSet C -> FunctorToType C".
+ *)
+
+Coercion FunctorTo_Set2Type : FunctorToSet >-> FunctorToType.
+
+Record GrothendieckPair `(C : @Category objC) (F : Functor C TypeCat) :=
+  { GrothendieckC : objC;
+    GrothendieckX : F GrothendieckC }.
+
+Record SetGrothendieckPair `(C : @Category objC) (F' : Functor C SetCat) :=
+  { SetGrothendieckC : objC;
+    SetGrothendieckX : F' SetGrothendieckC }.
+
+Section SetGrothendieckCoercion.
+  Context `(C : @Category objC).
+  Variable F : Functor C SetCat.
+  Let F' := (F : FunctorToSet _) : FunctorToType _.
+
+  Set Printing Universes.
+  Definition SetGrothendieck2Grothendieck (G : SetGrothendieckPair F) : GrothendieckPair F'
+    := {| GrothendieckC := G.(SetGrothendieckC); GrothendieckX := G.(SetGrothendieckX) : F' _ |}.
+  (* Toplevel input, characters 0-187:
+Error: Illegal application:
+The term "ObjectOf (* Top.8375 Top.8376 Top.8379 Set *)" of type
+ "forall (objC : Type (* Top.8375 *))
+    (C : Category (* Top.8375 Top.8376 *) objC) (objD : Type (* Top.8379 *))
+    (D : Category (* Top.8379 Set *) objD),
+  Functor (* Top.8375 Top.8376 Top.8379 Set *) C D -> objC -> objD"
+cannot be applied to the terms
+ "objC" : "Type (* Top.8375 *)"
+ "C" : "Category (* Top.8375 Top.8376 *) objC"
+ "Type (* Set *)" : "Type (* Set+1 *)"
+ "TypeCat (* Top.8379 Set *)" : "Category (* Top.8379 Set *) Set"
+ "F'" : "FunctorToType (* Top.8375 Top.8376 Top.8379 Set *) C"
+ "SetGrothendieckC (* Top.8375 Top.8376 Top.8379 *) G" : "objC"
+The 5th term has type "FunctorToType (* Top.8375 Top.8376 Top.8379 Set *) C"
+which should be coercible to
+ "Functor (* Top.8375 Top.8376 Top.8379 Set *) C TypeCat (* Top.8379 Set *)".
+ *)
+End SetGrothendieckCoercion.
diff --git a/test-suite/bugs/closed/HoTT_coq_029.v b/test-suite/bugs/closed/HoTT_coq_029.v
new file mode 100644
index 000000000..85a2714c7
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_029.v
@@ -0,0 +1,315 @@
+Module FirstComment.
+  Set Implicit Arguments.
+  Generalizable All Variables.
+  Set Asymmetric Patterns.
+  Set Universe Polymorphism.
+
+  Reserved Notation "x # y" (at level 40, left associativity).
+  Reserved Notation "x #m y" (at level 40, left associativity).
+
+  Delimit Scope object_scope with object.
+  Delimit Scope morphism_scope with morphism.
+  Delimit Scope category_scope with category.
+
+  Record Category (obj : Type) :=
+    {
+      Object :> _ := obj;
+      Morphism : obj -> obj -> Type;
+
+      Identity : forall x, Morphism x x;
+      Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
+    }.
+
+  Bind Scope object_scope with Object.
+  Bind Scope morphism_scope with Morphism.
+
+  Arguments Object {obj%type} C%category / : rename.
+  Arguments Morphism {obj%type} !C%category s d : rename. (* , simpl nomatch. *)
+  Arguments Identity {obj%type} [!C%category] x%object : rename.
+  Arguments Compose {obj%type} [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename.
+
+  Bind Scope category_scope with Category.
+
+  Record Functor
+         `(C : @Category objC)
+         `(D : @Category objD)
+    := {
+        ObjectOf :> objC -> objD;
+        MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d)
+      }.
+
+  Record NaturalTransformation
+         `(C : @Category objC)
+         `(D : @Category objD)
+         (F G : Functor C D)
+    := {
+        ComponentsOf :> forall c, D.(Morphism) (F c) (G c)
+      }.
+
+  Definition ProductCategory
+             `(C : @Category objC)
+             `(D : @Category objD)
+  : @Category (objC * objD)%type.
+    refine (@Build_Category _
+                            (fun s d => (C.(Morphism) (fst s) (fst d) * D.(Morphism) (snd s) (snd d))%type)
+                            (fun o => (Identity (fst o), Identity (snd o)))
+                            (fun s d d' m2 m1 => (Compose (fst m2) (fst m1), Compose (snd m2) (snd m1)))).
+
+  Defined.
+
+  Infix "*" := ProductCategory : category_scope.
+
+  Record IsomorphismOf `{C : @Category objC} {s d} (m : C.(Morphism) s d) :=
+    {
+      IsomorphismOf_Morphism :> C.(Morphism) s d := m;
+      Inverse : C.(Morphism) d s
+    }.
+
+  Record NaturalIsomorphism
+         `(C : @Category objC)
+         `(D : @Category objD)
+         (F G : Functor C D)
+    := {
+        NaturalIsomorphism_Transformation :> NaturalTransformation F G;
+        NaturalIsomorphism_Isomorphism : forall x : objC, IsomorphismOf (NaturalIsomorphism_Transformation x)
+      }.
+
+  Section PreMonoidalCategory.
+    Context `(C : @Category objC).
+
+    Variable TensorProduct : Functor (C * C) C.
+
+    Let src {C : @Category objC} {s d} (_ : Morphism C s d) := s.
+    Let dst {C : @Category objC} {s d} (_ : Morphism C s d) := d.
+
+    Local Notation "A # B" := (TensorProduct (A, B)).
+    Local Notation "A #m B" := (TensorProduct.(MorphismOf) ((@src _ _ _ A, @src _ _ _ B)) ((@dst _ _ _ A, @dst _ _ _ B)) (A, B)%morphism).
+
+    Let TriMonoidalProductL_ObjectOf (abc : C * C * C) : C :=
+      (fst (fst abc) # snd (fst abc)) # snd abc.
+
+    Let TriMonoidalProductR_ObjectOf (abc : C * C * C) : C :=
+      fst (fst abc) # (snd (fst abc) # snd abc).
+
+    Let TriMonoidalProductL_MorphismOf (s d : C * C * C) (m : Morphism (C * C * C) s d) :
+      Morphism C (TriMonoidalProductL_ObjectOf s) (TriMonoidalProductL_ObjectOf d).
+    Admitted.
+
+    Let TriMonoidalProductR_MorphismOf (s d : C * C * C) (m : Morphism (C * C * C) s d) :
+      Morphism C (TriMonoidalProductR_ObjectOf s) (TriMonoidalProductR_ObjectOf d).
+    Admitted.
+
+    Definition TriMonoidalProductL : Functor (C * C * C) C.
+      refine (Build_Functor (C * C * C) C
+                            TriMonoidalProductL_ObjectOf
+                            TriMonoidalProductL_MorphismOf).
+    Defined.
+
+    Definition TriMonoidalProductR : Functor (C * C * C) C.
+      refine (Build_Functor (C * C * C) C
+                            TriMonoidalProductR_ObjectOf
+                            TriMonoidalProductR_MorphismOf).
+    Defined.
+
+    Variable Associator : NaturalIsomorphism TriMonoidalProductL TriMonoidalProductR.
+
+    Section AssociatorCoherenceCondition.
+      Variables a b c d : C.
+
+      (* going from top-left *)
+      Let AssociatorCoherenceConditionT0 : Morphism C (((a # b) # c) # d) ((a # (b # c)) # d)
+        := Associator (a, b, c) #m Identity (C := C) d.
+      Let AssociatorCoherenceConditionT1 : Morphism C ((a # (b # c)) # d) (a # ((b # c) # d))
+        := Associator (a, b # c, d).
+      Let AssociatorCoherenceConditionT2 : Morphism C (a # ((b # c) # d)) (a # (b # (c # d)))
+        := Identity (C := C) a #m Associator (b, c, d).
+      Let AssociatorCoherenceConditionB0 : Morphism C (((a # b) # c) # d) ((a # b) # (c # d))
+        := Associator (a # b, c, d).
+      Let AssociatorCoherenceConditionB1 : Morphism C ((a # b) # (c # d)) (a # (b # (c # d)))
+        := Associator (a, b, c # d).
+
+      Definition AssociatorCoherenceCondition' :=
+        Compose AssociatorCoherenceConditionT2 (Compose AssociatorCoherenceConditionT1 AssociatorCoherenceConditionT0)
+        = Compose AssociatorCoherenceConditionB1 AssociatorCoherenceConditionB0.
+    End AssociatorCoherenceCondition.
+
+    Definition AssociatorCoherenceCondition := Eval unfold AssociatorCoherenceCondition' in
+                                                forall a b c d : C, AssociatorCoherenceCondition' a b c d.
+  End PreMonoidalCategory.
+
+  Section MonoidalCategory.
+    Variable objC : Type.
+
+    Let AssociatorCoherenceCondition' := Eval unfold AssociatorCoherenceCondition in @AssociatorCoherenceCondition.
+
+    Record MonoidalCategory :=
+      {
+        MonoidalUnderlyingCategory :> @Category objC;
+        TensorProduct : Functor (MonoidalUnderlyingCategory * MonoidalUnderlyingCategory) MonoidalUnderlyingCategory;
+        IdentityObject : objC;
+        Associator : NaturalIsomorphism (TriMonoidalProductL TensorProduct) (TriMonoidalProductR TensorProduct);
+        AssociatorCoherent : AssociatorCoherenceCondition' Associator
+      }.
+  End MonoidalCategory.
+
+  Section EnrichedCategory.
+    Context `(M : @MonoidalCategory objM).
+    Let x : M := IdentityObject M.
+    (* Anomaly: apply_coercion_args: mismatch between arguments and coercion. Please report.  *)
+  End EnrichedCategory.
+End FirstComment.
+
+Module SecondComment.
+  Set Implicit Arguments.
+  Set Universe Polymorphism.
+  Generalizable All Variables.
+
+  Record Category (obj : Type) :=
+    Build_Category {
+        Object :> _ := obj;
+        Morphism : obj -> obj -> Type;
+
+        Identity : forall x, Morphism x x;
+        Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
+      }.
+
+  Arguments Identity {obj%type} [!C] x : rename.
+  Arguments Compose {obj%type} [!C s d d'] m1 m2 : rename.
+
+  Record > Category' :=
+    {
+      LSObject : Type;
+
+      LSUnderlyingCategory :> @Category LSObject
+    }.
+
+  Section Functor.
+    Context `(C : @Category objC).
+    Context `(D : @Category objD).
+
+
+    Record Functor :=
+      {
+        ObjectOf :> objC -> objD;
+        MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d)
+      }.
+  End Functor.
+
+  Arguments MorphismOf {objC%type} [C] {objD%type} [D] F [s d] m : rename, simpl nomatch.
+
+  Section FunctorComposition.
+    Context `(C : @Category objC).
+    Context `(D : @Category objD).
+    Context `(E : @Category objE).
+
+    Definition ComposeFunctors (G : Functor D E) (F : Functor C D) : Functor C E.
+    Admitted.
+  End FunctorComposition.
+
+  Section IdentityFunctor.
+    Context `(C : @Category objC).
+
+
+    Definition IdentityFunctor : Functor C C.
+      refine {| ObjectOf := (fun x => x);
+                MorphismOf := (fun _ _ x => x)
+             |}.
+    Defined.
+  End IdentityFunctor.
+
+  Section ProductCategory.
+    Context `(C : @Category objC).
+    Context `(D : @Category objD).
+
+    Definition ProductCategory : @Category (objC * objD)%type.
+      refine (@Build_Category _
+                              (fun s d => (C.(Morphism) (fst s) (fst d) * D.(Morphism) (snd s) (snd d))%type)
+                              (fun o => (Identity (fst o), Identity (snd o)))
+                              (fun s d d' m2 m1 => (Compose (fst m2) (fst m1), Compose (snd m2) (snd m1)))).
+    Defined.
+  End ProductCategory.
+
+  Definition OppositeCategory `(C : @Category objC) : Category objC :=
+    @Build_Category objC
+                    (fun s d => Morphism C d s)
+                    (Identity (C := C))
+                    (fun _ _ _ m1 m2 => Compose m2 m1).
+
+  Parameter FunctorCategory : forall `(C : @Category objC) `(D : @Category objD), @Category (Functor C D).
+
+  Parameter TerminalCategory : Category unit.
+
+  Section ComputableCategory.
+    Variable I : Type.
+    Variable Index2Object : I -> Type.
+    Variable Index2Cat : forall i : I, @Category (@Index2Object i).
+
+    Local Coercion Index2Cat : I >-> Category.
+
+    Definition ComputableCategory : @Category I.
+      refine (@Build_Category _
+                              (fun C D : I => Functor C D)
+                              (fun o : I => IdentityFunctor o)
+                              (fun C D E : I => ComposeFunctors (C := C) (D := D) (E := E))).
+    Defined.
+  End ComputableCategory.
+
+  Section SmallCat.
+    Definition LocallySmallCat := ComputableCategory _ LSUnderlyingCategory.
+  End SmallCat.
+
+  Section CommaCategory.
+    Context `(A : @Category objA).
+    Context `(B : @Category objB).
+    Context `(C : @Category objC).
+    Variable S : Functor A C.
+    Variable T : Functor B C.
+
+    Record CommaCategory_Object := { CommaCategory_Object_Member :> { ab : objA * objB & C.(Morphism) (S (fst ab)) (T (snd ab)) } }.
+
+    Let SortPolymorphic_Helper (A T : Type) (Build_T : A -> T) := A.
+
+    Definition CommaCategory_ObjectT := Eval hnf in SortPolymorphic_Helper Build_CommaCategory_Object.
+    Definition Build_CommaCategory_Object' (mem : CommaCategory_ObjectT) := Build_CommaCategory_Object mem.
+    Global Coercion Build_CommaCategory_Object' : CommaCategory_ObjectT >-> CommaCategory_Object.
+
+    Definition CommaCategory : @Category CommaCategory_Object.
+    Admitted.
+  End CommaCategory.
+
+  Definition SliceCategory_Functor `(C : @Category objC) (a : C) : Functor TerminalCategory C
+    := {| ObjectOf := (fun _ => a);
+          MorphismOf := (fun _ _ _ => Identity a)
+       |}.
+
+  Definition SliceCategoryOver
+  : forall (objC : Type) (C : Category objC) (a : C),
+      Category
+        (CommaCategory_Object (IdentityFunctor C)
+                              (SliceCategory_Functor C a)).
+    admit.
+  Defined.
+
+  Section CommaCategoryProjectionFunctor.
+    Context `(A : Category objA).
+    Context `(B : Category objB).
+    Context `(C : Category objC).
+
+    Variable S : (OppositeCategory (FunctorCategory A C)).
+    Variable T : (FunctorCategory B C).
+
+    Definition CommaCategoryProjection : Functor (CommaCategory S T) (ProductCategory A B).
+    Admitted.
+
+    Definition CommaCategoryProjectionFunctor_ObjectOf
+    : @SliceCategoryOver _ LocallySmallCat (ProductCategory A B : Category _)
+      :=
+        existT _
+               ((CommaCategory S T : Category _) : Category', tt)
+               (CommaCategoryProjection) :
+          CommaCategory_ObjectT (IdentityFunctor _)
+                                (SliceCategory_Functor LocallySmallCat
+                                                       (ProductCategory A B : Category _)).
+    (* Anomaly: apply_coercion_args: mismatch between arguments and coercion. Please report. *)
+  End CommaCategoryProjectionFunctor.
+End SecondComment.
diff --git a/test-suite/bugs/closed/HoTT_coq_030.v b/test-suite/bugs/closed/HoTT_coq_030.v
new file mode 100644
index 000000000..c9d8fe137
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_030.v
@@ -0,0 +1,240 @@
+Set Implicit Arguments.
+Generalizable All Variables.
+Set Asymmetric Patterns.
+Set Universe Polymorphism.
+
+Delimit Scope object_scope with object.
+Delimit Scope morphism_scope with morphism.
+Delimit Scope category_scope with category.
+Delimit Scope functor_scope with functor.
+
+Local Open Scope category_scope.
+
+Record SpecializedCategory (obj : Type) :=
+  {
+    Object :> _ := obj;
+    Morphism : obj -> obj -> Type;
+
+    Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
+  }.
+
+Bind Scope category_scope with SpecializedCategory.
+Bind Scope object_scope with Object.
+Bind Scope morphism_scope with Morphism.
+
+Arguments Object {obj%type} C%category / : rename.
+Arguments Morphism {obj%type} !C%category s d : rename. (* , simpl nomatch. *)
+Arguments Compose {obj%type} [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename.
+
+Record Category := {
+  CObject : Type;
+
+  UnderlyingCategory :> @SpecializedCategory CObject
+}.
+
+Definition GeneralizeCategory `(C : @SpecializedCategory obj) : Category.
+  refine {| CObject := C.(Object) |}; auto. (* Changing this [auto] to [assumption] removes the universe inconsistency. *)
+Defined.
+
+Coercion GeneralizeCategory : SpecializedCategory >-> Category.
+
+Record SpecializedFunctor
+       `(C : @SpecializedCategory objC)
+       `(D : @SpecializedCategory objD)
+  := {
+      ObjectOf :> objC -> objD;
+      MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d)
+    }.
+
+Section Functor.
+  Variable C D : Category.
+
+  Definition Functor := SpecializedFunctor C D.
+End Functor.
+
+Bind Scope functor_scope with SpecializedFunctor.
+Bind Scope functor_scope with Functor.
+
+Arguments SpecializedFunctor {objC} C {objD} D.
+Arguments Functor C D.
+Arguments ObjectOf {objC%type C%category objD%type D%category} F%functor c%object : rename, simpl nomatch.
+Arguments MorphismOf {objC%type} [C%category] {objD%type} [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch.
+
+Section FunctorComposition.
+  Context `(B : @SpecializedCategory objB).
+  Context `(C : @SpecializedCategory objC).
+  Context `(D : @SpecializedCategory objD).
+  Context `(E : @SpecializedCategory objE).
+
+  Definition ComposeFunctors (G : SpecializedFunctor D E) (F : SpecializedFunctor C D) : SpecializedFunctor C E
+    := Build_SpecializedFunctor C E
+                                (fun c => G (F c))
+                                (fun _ _ m => G.(MorphismOf) (F.(MorphismOf) m)).
+End FunctorComposition.
+
+Record SpecializedNaturalTransformation
+       `{C : @SpecializedCategory objC}
+       `{D : @SpecializedCategory objD}
+       (F G : SpecializedFunctor C D)
+  := {
+      ComponentsOf :> forall c, D.(Morphism) (F c) (G c)
+    }.
+
+Definition ProductCategory
+           `(C : @SpecializedCategory objC)
+           `(D : @SpecializedCategory objD)
+: @SpecializedCategory (objC * objD)%type
+  := @Build_SpecializedCategory _
+                                (fun s d => (C.(Morphism) (fst s) (fst d) * D.(Morphism) (snd s) (snd d))%type)
+                                (fun s d d' m2 m1 => (Compose (fst m2) (fst m1), Compose (snd m2) (snd m1))).
+
+Infix "*" := ProductCategory : category_scope.
+
+Section ProductCategoryFunctors.
+  Context `{C : @SpecializedCategory objC}.
+  Context `{D : @SpecializedCategory objD}.
+
+  Definition fst_Functor : SpecializedFunctor (C * D) C
+    := Build_SpecializedFunctor (C * D) C
+                                (@fst _ _)
+                                (fun _ _ => @fst _ _).
+
+  Definition snd_Functor : SpecializedFunctor (C * D) D
+    := Build_SpecializedFunctor (C * D) D
+                                (@snd _ _)
+                                (fun _ _ => @snd _ _).
+End ProductCategoryFunctors.
+
+
+Definition OppositeCategory `(C : @SpecializedCategory objC) : @SpecializedCategory objC :=
+  @Build_SpecializedCategory objC
+                             (fun s d => Morphism C d s)
+                             (fun _ _ _ m1 m2 => Compose m2 m1).
+
+Section OppositeFunctor.
+  Context `(C : @SpecializedCategory objC).
+  Context `(D : @SpecializedCategory objD).
+  Variable F : SpecializedFunctor C D.
+  Let COp := OppositeCategory C.
+  Let DOp := OppositeCategory D.
+
+  Definition OppositeFunctor : SpecializedFunctor COp DOp
+    := Build_SpecializedFunctor COp DOp
+                                (fun c : COp => F c : DOp)
+                                (fun (s d : COp) (m : C.(Morphism) d s) => MorphismOf F (s := d) (d := s) m).
+End OppositeFunctor.
+
+Section FunctorProduct.
+  Context `(C : @SpecializedCategory objC).
+  Context `(D : @SpecializedCategory objD).
+  Context `(D' : @SpecializedCategory objD').
+
+  Definition FunctorProduct (F : Functor C D) (F' : Functor C D') : SpecializedFunctor C (D * D').
+    match goal with
+      | [ |- SpecializedFunctor ?C0 ?D0 ] =>
+        refine (Build_SpecializedFunctor
+                  C0 D0
+                  (fun c => (F c, F' c))
+                  (fun s d m => (MorphismOf F m, MorphismOf F' m)))
+    end.
+  Defined.
+End FunctorProduct.
+
+Section FunctorProduct'.
+  Context `(C : @SpecializedCategory objC).
+  Context `(D : @SpecializedCategory objD).
+  Context `(C' : @SpecializedCategory objC').
+  Context `(D' : @SpecializedCategory objD').
+  Variable F : Functor C D.
+  Variable F' : Functor C' D'.
+
+  Definition FunctorProduct' : SpecializedFunctor  (C * C') (D * D')
+    := FunctorProduct (ComposeFunctors F fst_Functor) (ComposeFunctors F' snd_Functor).
+End FunctorProduct'.
+
+(** XXX TODO(jgross): Change this to [FunctorProduct]. *)
+Infix "*" := FunctorProduct' : functor_scope.
+
+Definition TypeCat : @SpecializedCategory Type :=
+  (@Build_SpecializedCategory Type
+                              (fun s d => s -> d)
+                              (fun _ _ _ f g => (fun x => f (g x)))).
+
+Section HomFunctor.
+  Context `(C : @SpecializedCategory objC).
+  Let COp := OppositeCategory C.
+
+  Definition CovariantHomFunctor (A : COp) : SpecializedFunctor C TypeCat
+    := Build_SpecializedFunctor C TypeCat
+                                (fun X : C => C.(Morphism) A X : TypeCat)
+                                (fun X Y f => (fun g : C.(Morphism) A X => Compose f g)).
+
+  Definition hom_functor_object_of (c'c : COp * C) := C.(Morphism) (fst c'c) (snd c'c) : TypeCat.
+
+  Definition hom_functor_morphism_of (s's : (COp * C)%type) (d'd : (COp * C)%type) (hf : (COp * C).(Morphism) s's d'd) :
+    TypeCat.(Morphism) (hom_functor_object_of s's) (hom_functor_object_of d'd).
+    unfold hom_functor_object_of in *.
+    destruct s's as [ s' s ], d'd as [ d' d ].
+    destruct hf as [ h f ].
+    intro g.
+    exact (Compose f (Compose g h)).
+  Defined.
+
+  Definition HomFunctor : SpecializedFunctor (COp * C) TypeCat
+    := Build_SpecializedFunctor (COp * C) TypeCat
+                                (fun c'c : COp * C => C.(Morphism) (fst c'c) (snd c'c) : TypeCat)
+                                (fun X Y (hf : (COp * C).(Morphism) X Y) => hom_functor_morphism_of hf).
+End HomFunctor.
+
+Section FullFaithful.
+  Context `(C : @SpecializedCategory objC).
+  Context `(D : @SpecializedCategory objD).
+  Variable F : SpecializedFunctor C D.
+  Let COp := OppositeCategory C.
+  Let DOp := OppositeCategory D.
+  Let FOp := OppositeFunctor F.
+
+  Definition InducedHomNaturalTransformation :
+    SpecializedNaturalTransformation (HomFunctor C) (ComposeFunctors (HomFunctor D) (FOp * F))
+    := (Build_SpecializedNaturalTransformation (HomFunctor C) (ComposeFunctors (HomFunctor D) (FOp * F))
+                                               (fun sd : (COp * C) =>
+                                                  MorphismOf F (s := _) (d := _))).
+End FullFaithful.
+
+Definition FunctorCategory
+           `(C : @SpecializedCategory objC)
+           `(D : @SpecializedCategory objD)
+: @SpecializedCategory (SpecializedFunctor C D).
+  refine (@Build_SpecializedCategory _
+                                     (SpecializedNaturalTransformation (C := C) (D := D))
+                                     _);
+  admit.
+Defined.
+
+Notation "C ^ D" := (FunctorCategory D C) : category_scope.
+
+Section Yoneda.
+  Context `(C : @SpecializedCategory objC).
+  Let COp := OppositeCategory C.
+
+  Section Yoneda.
+    Let Yoneda_NT s d (f : COp.(Morphism) s d) : SpecializedNaturalTransformation (CovariantHomFunctor C s) (CovariantHomFunctor C d)
+      := Build_SpecializedNaturalTransformation
+           (CovariantHomFunctor C s)
+           (CovariantHomFunctor C d)
+           (fun c : C => (fun m : C.(Morphism) _ _ => Compose m f)).
+
+    Definition Yoneda : SpecializedFunctor COp (TypeCat ^ C)
+      := Build_SpecializedFunctor COp (TypeCat ^ C)
+                                  (fun c : COp => CovariantHomFunctor C c : TypeCat ^ C)
+                                  (fun s d (f : Morphism COp s d) => Yoneda_NT s d f).
+  End Yoneda.
+End Yoneda.
+
+Section FullyFaithful.
+  Context `(C : @SpecializedCategory objC).
+
+  Set Printing Universes.
+  Check InducedHomNaturalTransformation (Yoneda C).
+  (* Error: Universe inconsistency (cannot enforce Top.865 = Top.851 because
+Top.851 < Top.869 <= Top.864 <= Top.865). *)
diff --git a/test-suite/bugs/closed/HoTT_coq_032.v b/test-suite/bugs/closed/HoTT_coq_032.v
new file mode 100644
index 000000000..39a7103d1
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_032.v
@@ -0,0 +1,22 @@
+(* -*- mode: coq; coq-prog-args: ("-xml") -*- *)
+Set Implicit Arguments.
+Generalizable All Variables.
+Set Asymmetric Patterns.
+Set Universe Polymorphism.
+
+Delimit Scope object_scope with object.
+Delimit Scope morphism_scope with morphism.
+Delimit Scope category_scope with category.
+Delimit Scope functor_scope with functor.
+
+Local Open Scope category_scope.
+
+Record SpecializedCategory (obj : Type) :=
+  {
+    Object :> _ := obj;
+    Morphism : obj -> obj -> Type;
+
+    Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
+  }.
+(* Anomaly: Mismatched instance and context when building universe substitution.
+Please report. *)
diff --git a/test-suite/bugs/closed/HoTT_coq_033.v b/test-suite/bugs/closed/HoTT_coq_033.v
new file mode 100644
index 000000000..c4dbf74cd
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_033.v
@@ -0,0 +1,12 @@
+(** JMeq should be polymorphic *)
+Require Import JMeq.
+
+Set Implicit Arguments.
+
+Monomorphic Inductive JMeq' (A : Type) (x : A)
+: forall B : Type, B -> Prop :=
+  JMeq'_refl : JMeq' x x.
+
+Fail Monomorphic Definition foo := @JMeq' _ (@JMeq').
+
+Monomorphic Definition bar := @JMeq _ (@JMeq).
diff --git a/test-suite/bugs/closed/HoTT_coq_034.v b/test-suite/bugs/closed/HoTT_coq_034.v
new file mode 100644
index 000000000..9697928ff
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_034.v
@@ -0,0 +1,127 @@
+Module Short.
+  Set Universe Polymorphism.
+  Inductive relevant (A : Type) (B : Type) : Prop := .
+  Section foo.
+    Variables A B : Type.
+    Definition foo := prod (relevant A B) A.
+  End foo.
+
+  Section bar.
+    Variable A : Type.
+    Variable B : Type.
+    Definition bar := prod (relevant A B) A.
+  End bar.
+
+  Set Printing Universes.
+  Check bar nat Set : Set. (* success *)
+  Check foo nat Set : Set. (* Toplevel input, characters 6-17:
+Error:
+The term "foo (* Top.303 Top.304 *) nat Set" has type
+"Type (* Top.304 *)" while it is expected to have type
+"Set" (Universe inconsistency: Cannot enforce Top.304 = Set because Set
+< Top.304)). *)
+End Short.
+
+Section Long.
+  Set Universe Polymorphism.
+  Set Implicit Arguments.
+  Generalizable All Variables.
+
+  Record SpecializedCategory (obj : Type) :=
+    {
+      Object :> _ := obj;
+      Morphism : obj -> obj -> Type
+    }.
+
+
+  Record > Category :=
+    {
+      CObject : Type;
+
+      UnderlyingCategory :> @SpecializedCategory CObject
+    }.
+
+  Record SpecializedFunctor `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) :=
+    {
+      ObjectOf :> objC -> objD;
+      MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d)
+    }.
+
+  (* Replacing this with [Definition Functor (C D : Category) :=
+SpecializedFunctor C D.] gets rid of the universe inconsistency. *)
+  Section Functor.
+    Variable C D : Category.
+
+    Definition Functor := SpecializedFunctor C D.
+  End Functor.
+
+  Record SpecializedNaturalTransformation `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) (F G : SpecializedFunctor C D) :=
+    {
+      ComponentsOf :> forall c, D.(Morphism) (F c) (G c)
+    }.
+
+  Definition FunctorProduct' `(F : Functor C D) : SpecializedFunctor C D.
+    admit.
+  Defined.
+
+  Definition TypeCat : @SpecializedCategory Type.
+    admit.
+  Defined.
+
+
+  Definition CovariantHomFunctor `(C : @SpecializedCategory objC) : SpecializedFunctor C TypeCat.
+    refine (Build_SpecializedFunctor C TypeCat
+                                     (fun X : C => C.(Morphism) X X)
+                                     _
+           ); admit.
+  Defined.
+
+  Definition FunctorCategory `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) : @SpecializedCategory (SpecializedFunctor C D).
+    refine (@Build_SpecializedCategory _
+                                       (SpecializedNaturalTransformation (C := C) (D := D))).
+  Defined.
+
+  Definition Yoneda `(C : @SpecializedCategory objC) : SpecializedFunctor C (FunctorCategory C TypeCat).
+    match goal with
+      | [ |- SpecializedFunctor ?C0 ?D0 ] =>
+        refine (Build_SpecializedFunctor C0 D0
+                                         (fun c => CovariantHomFunctor C)
+                                         _
+               )
+    end;
+    admit.
+  Defined.
+
+  Section FullyFaithful.
+    Context `(C : @SpecializedCategory objC).
+    Let TypeCatC := FunctorCategory C TypeCat.
+    Let YC := (Yoneda C).
+    Set Printing Universes.
+    Check @FunctorProduct' C TypeCatC (Yoneda C).
+    (* Toplevel input, characters 35-43:
+Error:
+In environment
+objC : Type (* Top.186 *)
+C : SpecializedCategory (* Top.185 Top.186 *) objC
+TypeCatC := FunctorCategory (* Top.187 Top.185 Top.189 Top.186 Top.191
+              Top.192 *) C TypeCat (* Top.193 Top.192 Top.195 Top.191 *)
+         : SpecializedCategory (* Top.189 Top.187 *)
+             (SpecializedFunctor (* Top.192 Top.186 Top.191 Top.185 *) C
+                TypeCat (* Top.193 Top.192 Top.195 Top.191 *))
+YC := Yoneda (* Top.197 Top.198 Top.185 Top.186 Top.201 Top.202 Top.203
+        Top.204 Top.185 Top.206 *) C
+   : SpecializedFunctor (* Top.202 Top.186 Top.203 Top.185 *) C
+       (FunctorCategory (* Top.203 Top.185 Top.202 Top.186 Top.197 Top.198 *)
+          C TypeCat (* Top.185 Top.198 Top.204 Top.197 *))
+The term
+ "Yoneda (* Top.225 Top.226 Top.227 Top.186 Top.229 Top.230 Top.231 Top.232
+    Top.185 Top.234 *) C" has type
+ "SpecializedFunctor (* Top.230 Top.228 Top.231 Top.233 *) C
+    (FunctorCategory (* Top.231 Top.233 Top.230 Top.228 Top.225 Top.226 *) C
+       TypeCat (* Top.227 Top.226 Top.232 Top.225 *))"
+while it is expected to have type
+ "Functor (* Top.216 Top.219 Top.217 Top.220 *) C TypeCatC"
+(Universe inconsistency: Cannot enforce Top.230 = Top.217 because Top.217
+<= Top.227 < Top.225 <= Top.231 <= Top.230)).
+     *)
+End Long.
diff --git a/test-suite/bugs/closed/HoTT_coq_036.v b/test-suite/bugs/closed/HoTT_coq_036.v
new file mode 100644
index 000000000..b06830dd0
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_036.v
@@ -0,0 +1,132 @@
+Module Version1.
+  Set Implicit Arguments.
+  Set Universe Polymorphism.
+  Generalizable All Variables.
+
+  Record SpecializedCategory (obj : Type) :=
+    {
+      Object :> _ := obj
+    }.
+
+  Record > Category :=
+    {
+      CObject : Type;
+      UnderlyingCategory :> @SpecializedCategory CObject
+    }.
+
+  Record SpecializedFunctor `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) :=
+    {
+      ObjectOf :> objC -> objD
+    }.
+
+  Definition Functor (C D : Category) := SpecializedFunctor C D.
+
+  Parameter TerminalCategory : SpecializedCategory unit.
+
+  Definition focus A (_ : A) := True.
+
+  Definition CommaCategory_Object (A : Category) (S : Functor TerminalCategory A) : Type.
+    assert (Hf : focus ((S tt) = (S tt))) by constructor.
+    progress change CObject with (fun C => @Object (CObject C) C) in *.
+    simpl in *.
+    match type of Hf with
+      | focus ?V => exact V
+    end.
+  Defined.
+
+  Definition Build_SliceCategory (A : Category) (F : Functor TerminalCategory A) := @Build_SpecializedCategory (CommaCategory_Object F).
+  Parameter SetCat : @SpecializedCategory Set.
+
+  Set Printing Universes.
+  Check (fun (A : Category) (F : Functor TerminalCategory A) => @Build_SpecializedCategory (CommaCategory_Object F)) SetCat.
+  (* (fun (A : Category (* Top.68 *))
+   (F : Functor (* Set Top.68 *) TerminalCategory A) =>
+ {|  |}) SetCat (* Top.68 *)
+     : forall
+         F : Functor (* Set Top.68 *) TerminalCategory SetCat (* Top.68 *),
+       let Object := CommaCategory_Object (* Top.68 Top.69 Top.68 *) F in
+       SpecializedCategory (* Top.69 *)
+         (CommaCategory_Object (* Top.68 Top.69 Top.68 *) F) *)
+  Check @Build_SliceCategory SetCat. (* Toplevel input, characters 0-34:
+Error: Universe inconsistency (cannot enforce Top.51 <= Set because Set
+< Top.51). *)
+End Version1.
+
+Module Version2.
+  Set Implicit Arguments.
+  Set Universe Polymorphism.
+
+  Record SpecializedCategory (obj : Type) :=
+    {
+      Object : _ := obj
+    }.
+
+  Record > Category :=
+    {
+      CObject : Type;
+      UnderlyingCategory :> @SpecializedCategory CObject
+    }.
+
+  Parameter TerminalCategory : SpecializedCategory unit.
+
+  Definition focus A (_ : A) := True.
+  Parameter ObjectOf' : forall (objC : Type) (C : SpecializedCategory objC)
+                               (objD : Type) (D : SpecializedCategory objD), Prop.
+  Definition CommaCategory_Object (A : Category) : Type.
+    assert (Hf : focus (@ObjectOf' _ (@Build_Category unit TerminalCategory) _ A)) by constructor.
+    progress change CObject with (fun C => @Object (CObject C) C) in *;
+      simpl in *.
+    match type of Hf with
+      | focus ?V => exact V
+    end.
+  Defined.
+
+  Definition Build_SliceCategory := @CommaCategory_Object.
+  Parameter SetCat : @SpecializedCategory Set.
+
+  Set Printing Universes.
+  Check @Build_SliceCategory SetCat.
+End Version2.
+
+Module OtherBug.
+  Set Implicit Arguments.
+  Set Universe Polymorphism.
+
+  Record SpecializedCategory (obj : Type) :=
+    {
+      Object : _ := obj
+    }.
+
+  Record > Category :=
+    {
+      CObject : Type;
+      UnderlyingCategory :> @SpecializedCategory CObject
+    }.
+
+  Parameter TerminalCategory : SpecializedCategory unit.
+
+  Definition focus A (_ : A) := True.
+
+  Parameter ObjectOf' : forall (objC : Type) (C : SpecializedCategory objC)
+                               (objD : Type) (D : SpecializedCategory objD), Prop.
+  Definition CommaCategory_Object (A : Category) : Type.
+    assert (Hf : focus (@ObjectOf' _ (@Build_Category unit TerminalCategory) _ A)) by constructor.
+    progress change CObject with (fun C => @Object (CObject C) C) in *;
+      simpl in *.
+    match type of Hf with
+      | focus ?V => exact V
+    end.
+  Defined.
+
+  Parameter SetCat : @SpecializedCategory Set.
+
+  Set Printing Universes.
+  Definition Build_SliceCategory := @CommaCategory_Object.
+  Check @CommaCategory_Object SetCat.
+  (* CommaCategory_Object (* Top.43 Top.44 Top.43 *) SetCat (* Top.43 *)
+     : Type (* Top.44 *) *)
+  Check @Build_SliceCategory SetCat.
+  (* Toplevel input, characters 0-34:
+Error: Universe inconsistency (cannot enforce Top.36 <= Set because Set
+< Top.36). *)
+End OtherBug.
diff --git a/test-suite/bugs/closed/HoTT_coq_045.v b/test-suite/bugs/closed/HoTT_coq_045.v
new file mode 100644
index 000000000..590bdd157
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_045.v
@@ -0,0 +1,50 @@
+Set Implicit Arguments.
+Set Universe Polymorphism.
+Generalizable All Variables.
+
+Record SpecializedCategory (obj : Type) :=
+  {
+    Object :> _ := obj
+  }.
+
+Record > Category :=
+  {
+    CObject : Type;
+    UnderlyingCategory :> @SpecializedCategory CObject
+  }.
+
+Record SpecializedFunctor `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) :=
+  {
+    ObjectOf :> objC -> objD
+  }.
+
+Definition Functor (C D : Category) := SpecializedFunctor C D.
+
+Parameter TerminalCategory : SpecializedCategory unit.
+
+Definition focus A (_ : A) := True.
+
+Definition CommaCategory_Object (A : Category) (S : Functor TerminalCategory A) : Type.
+  assert (Hf : focus ((S tt) = (S tt))) by constructor.
+  progress change CObject with (fun C => @Object (CObject C) C) in *.
+  simpl in *.
+  let V := match type of Hf with
+             | focus ?V => constr:(V)
+           end
+  in exact V.
+(* Toplevel input, characters 89-96:
+Error: Illegal application:
+The term "ObjectOf" of type
+ "forall (objC : Set) (C : SpecializedCategory objC)
+    (objD : Type) (D : SpecializedCategory objD),
+  SpecializedFunctor C D -> objC -> objD"
+cannot be applied to the terms
+ "Object TerminalCategory" : "Type"
+ "TerminalCategory" : "SpecializedCategory unit"
+ "Object A" : "Type"
+ "UnderlyingCategory A" : "SpecializedCategory (CObject A)"
+ "S" : "Functor TerminalCategory A"
+ "tt" : "unit"
+The 1st term has type "Type" which should be coercible to
+"Set". *)
+Defined.
diff --git a/test-suite/bugs/closed/HoTT_coq_052.v b/test-suite/bugs/closed/HoTT_coq_052.v
new file mode 100644
index 000000000..dac575b54
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_052.v
@@ -0,0 +1,19 @@
+Goal Type = Type.
+  match goal with |- ?x = ?x => idtac end.
+Abort.
+
+Goal Prop.
+  Fail match goal with |- Type => idtac end.
+Abort.
+
+Goal Prop = Set.
+  Fail match goal with |- ?x = ?x => idtac end.
+Abort.
+
+Goal Type = Prop.
+  Fail match goal with |- ?x = ?x => idtac end.
+Abort.
+
+Goal Type = Set.
+  Fail match goal with |- ?x = ?x => idtac end.
+Abort.
diff --git a/test-suite/bugs/closed/HoTT_coq_053.v b/test-suite/bugs/closed/HoTT_coq_053.v
new file mode 100644
index 000000000..a14fb6aa5
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_053.v
@@ -0,0 +1,50 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+Set Printing Universes.
+Set Implicit Arguments.
+Generalizable All Variables.
+Set Asymmetric Patterns.
+Set Universe Polymorphism.
+
+Inductive Unit : Type :=
+    tt : Unit.
+
+Inductive Bool : Type :=
+  | true : Bool
+  | false : Bool.
+
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+
+Record PreCategory :=
+  {
+    Object :> Type;
+    Morphism : Object -> Object -> Type
+  }.
+
+Definition DiscreteCategory X : PreCategory
+  := @Build_PreCategory X
+                        (@paths X).
+
+Definition IndiscreteCategory X : PreCategory
+  := @Build_PreCategory X
+                         (fun _ _ => Unit).
+
+Definition NatCategory (n : nat) :=
+  match n with
+    | 0 => IndiscreteCategory Unit
+    | _ => DiscreteCategory Bool
+  end.
+(* Error: Universe inconsistency (cannot enforce Set <= Prop).*)
+
+Definition NatCategory' (n : nat) :=
+  match n with
+    | 0 => (fun X => @Build_PreCategory X
+                         (fun _ _ => Unit : Prop)) Unit
+    | _ => DiscreteCategory Bool
+  end.
+
+Definition NatCategory'' (n : nat) :=
+  match n with
+    | 0 => IndiscreteCategory Unit
+    | _ => DiscreteCategory Bool
+  end.
diff --git a/test-suite/bugs/closed/HoTT_coq_054.v b/test-suite/bugs/closed/HoTT_coq_054.v
new file mode 100644
index 000000000..f79fe1c1e
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_054.v
@@ -0,0 +1,94 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+Inductive Empty : Prop := .
+
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+
+Arguments idpath {A a} , [A] a.
+
+Definition idmap {A : Type} : A -> A := fun x => x.
+
+Definition path_sum {A B : Type} (z z' : A + B)
+           (pq : match z, z' with
+                   | inl z0, inl z'0 => z0 = z'0
+                   | inr z0, inr z'0 => z0 = z'0
+                   | _, _ => Empty
+                 end)
+: z = z'.
+  destruct z, z', pq; exact idpath.
+Defined.
+
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+  := match p with idpath => idpath end.
+
+Theorem ex2_8 {A B A' B' : Type} (g : A -> A') (h : B -> B') (x y : A + B)
+              (* Fortunately, this unifies properly *)
+              (pq : match (x, y) with (inl x', inl y') => x' = y' | (inr x', inr y') => x' = y' | _ => Empty end) :
+  let f z := match z with inl z' => inl (g z') | inr z' => inr (h z') end in
+  ap f (path_sum x y pq) = path_sum (f x) (f y)
+     (* Coq appears to require *ALL* of the annotations *)
+     ((match x as x return match (x, y) with
+              (inl x', inl y') => x' = y'
+            | (inr x', inr y') => x' = y'
+            | _ => Empty
+          end -> match (f x, f y) with
+               | (inl x', inl y') => x' = y'
+               | (inr x', inr y') => x' = y'
+               | _ => Empty end with
+           | inl x' => match y as y return match y with
+                                               inl y' => x' = y'
+                                             | _ => Empty
+                                           end -> match f y with
+                                                    | inl y' => g x' = y'
+                                                    | _ => Empty end with
+                         | inl y' => ap g
+                         | inr y' => idmap
+                       end
+           | inr x' => match y as y return match y with
+                                               inr y' => x' = y'
+                                             | _ => Empty
+                                           end -> match f y with
+                                                    | inr y' => h x' = y'
+                                                    | _ => Empty end with
+                         | inl y' => idmap
+                         | inr y' => ap h
+                       end
+       end) pq).
+  destruct x; destruct y; destruct pq; reflexivity.
+Qed.
+(* Toplevel input, characters 1367-1374:
+Error:
+In environment
+A : Type
+B : Type
+A' : Type
+B' : Type
+g : A -> A'
+h : B -> B'
+x : A + B
+y : A + B
+pq :
+match x with
+| inl x' => match y with
+            | inl y' => x' = y'
+            | inr _ => Empty
+            end
+| inr x' => match y with
+            | inl _ => Empty
+            | inr y' => x' = y'
+            end
+end
+f :=
+fun z : A + B =>
+match z with
+| inl z' => inl (g z')
+| inr z' => inr (h z')
+end : A + B -> A' + B'
+x' : B
+y0 : A + B
+y' : B
+The term "x' = y'" has type "Type" while it is expected to have type
+"Prop" (Universe inconsistency). *)
diff --git a/test-suite/bugs/closed/HoTT_coq_061.v b/test-suite/bugs/closed/HoTT_coq_061.v
new file mode 100644
index 000000000..d1ea16ec3
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_061.v
@@ -0,0 +1,126 @@
+(* File reduced by coq-bug-finder from 9039 lines to 7786 lines, then from 7245 lines to 476 lines, then from 417 lines to 249 lines, then from 171 lines to 127 lines. *)
+
+Set Implicit Arguments.
+Set Universe Polymorphism.
+Definition admit {T} : T.
+Admitted.
+Delimit Scope object_scope with object.
+Delimit Scope morphism_scope with morphism.
+Delimit Scope category_scope with category.
+Delimit Scope functor_scope with functor.
+Delimit Scope natural_transformation_scope with natural_transformation.
+Reserved Infix "o" (at level 40, left associativity).
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+
+Arguments idpath {A a} , [A] a.
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+Definition inverse {A : Type} {x y : A} (p : x = y) : y = x
+  := match p with idpath => idpath end.
+
+Record PreCategory :=
+  {
+    Object :> Type;
+    Morphism : Object -> Object -> Type;
+
+    Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d' where "f 'o' g" := (Compose f g)
+  }.
+Bind Scope category_scope with PreCategory.
+
+Arguments Compose [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename.
+
+Infix "o" := Compose : morphism_scope.
+Local Open Scope morphism_scope.
+
+Record Functor (C D : PreCategory) :=
+  {
+    ObjectOf :> C -> D;
+    MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d);
+    FCompositionOf : forall s d d' (m1 : C.(Morphism) s d) (m2: C.(Morphism) d d'),
+                       MorphismOf _ _ (m2 o m1) = (MorphismOf _ _ m2) o (MorphismOf _ _ m1)
+  }.
+
+Bind Scope functor_scope with Functor.
+
+Arguments MorphismOf [C%category] [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch.
+
+Definition ComposeFunctors C D E
+           (G : Functor D E) (F : Functor C D) : Functor C E
+  := Build_Functor C E
+                   (fun c => G (F c))
+                   admit
+                   admit.
+
+Infix "o" := ComposeFunctors : functor_scope.
+
+Record NaturalTransformation C D (F G : Functor C D) :=
+  {
+    ComponentsOf :> forall c, D.(Morphism) (F c) (G c);
+    Commutes : forall s d (m : C.(Morphism) s d),
+                 ComponentsOf d o F.(MorphismOf) m = G.(MorphismOf) m o ComponentsOf s
+  }.
+
+Generalizable All Variables.
+
+Section NTComposeT.
+
+  Variable C : PreCategory.
+  Variable D : PreCategory.
+
+  Variables F F' F'' : Functor C D.
+
+  Variable T' : NaturalTransformation F' F''.
+  Variable T : NaturalTransformation F F'.
+  Let CO := fun c => T' c o T c.
+  Definition NTComposeT_Commutes s d (m : Morphism C s d)
+  : CO d o MorphismOf F m = MorphismOf F'' m o CO s.
+
+    admit.
+  Defined.
+  Definition NTComposeT
+  : NaturalTransformation F F''
+    := Build_NaturalTransformation F F''
+                                   (fun c => T' c o T c)
+                                   NTComposeT_Commutes.
+End NTComposeT.
+Definition NTWhiskerR C D E (F F' : Functor D E) (T : NaturalTransformation F F')
+           (G : Functor C D)
+  := Build_NaturalTransformation (F o G) (F' o G)
+                                 (fun c => T (G c))
+                                 admit.
+Global Class NTC_Composable A B (a : A) (b : B) (T : Type) (term : T) := {}.
+
+Definition NTC_Composable_term `{@NTC_Composable A B a b T term} := term.
+Notation "T 'o' U"
+  := (@NTC_Composable_term _ _ T%natural_transformation U%natural_transformation _ _ _)
+     : natural_transformation_scope.
+
+Local Open Scope natural_transformation_scope.
+
+Lemma NTWhiskerR_CompositionOf C D
+      (F G H : Functor C D)
+      (T : NaturalTransformation G H)
+      (T' : NaturalTransformation F G) B (I : Functor B C)
+: NTWhiskerR (NTComposeT T T') I = NTComposeT (NTWhiskerR T I) (NTWhiskerR T' I).
+
+  admit.
+Defined.
+Definition FunctorCategory C D : PreCategory
+  := @Build_PreCategory (Functor C D)
+                        (NaturalTransformation (C := C) (D := D))
+                        admit.
+
+Notation "[ C , D ]" := (FunctorCategory C D) : category_scope.
+
+Variable C : PreCategory.
+Variable D : PreCategory.
+Variable E : PreCategory.
+Definition NTWhiskerR_Functorial (G : [C, D]%category)
+: [[D, E], [C, E]]%category
+  := Build_Functor
+       [C, D] [C, E]
+       (fun F => F o G)
+       (fun _ _ T => T o G)
+       (fun _ _ _ _ _ => inverse (NTWhiskerR_CompositionOf _ _ _)).
+(* Anomaly: Uncaught exception Not_found(_). Please report. *)
diff --git a/test-suite/bugs/closed/HoTT_coq_062.v b/test-suite/bugs/closed/HoTT_coq_062.v
new file mode 100644
index 000000000..6c0221479
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_062.v
@@ -0,0 +1,95 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
+(* File reduced by coq-bug-finder from 5012 lines to 4659 lines, then from 4220 lines to 501 lines, then from 513 lines to 495 lines, then from 513 lines to 495 lines, then from 412 lines to 79 lines, then from 412 lines to 79 lines. *)
+Set Universe Polymorphism.
+Definition admit {T} : T.
+Admitted.
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+
+Arguments idpath {A a} , [A] a.
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+
+Delimit Scope path_scope with path.
+Local Open Scope path_scope.
+
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y :=
+  match p with idpath => u end.
+
+Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing) : path_scope.
+
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+  := match p with idpath => idpath end.
+
+Definition apD {A:Type} {B:A->Type} (f:forall a:A, B a) {x y:A} (p:x=y):
+  p # (f x) = f y
+  :=
+    match p with idpath => idpath end.
+
+Class IsEquiv {A B : Type} (f : A -> B) :=
+  BuildIsEquiv {
+      equiv_inv : B -> A
+    }.
+
+Record Equiv A B :=
+  BuildEquiv {
+      equiv_fun :> A -> B ;
+      equiv_isequiv :> IsEquiv equiv_fun
+    }.
+
+Existing Instance equiv_isequiv.
+
+Notation "A <~> B" := (Equiv A B) (at level 85) : equiv_scope.
+
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3) : equiv_scope.
+
+Inductive Bool : Type := true | false.
+
+Local Open Scope equiv_scope.
+Definition equiv_path (A B : Type) (p : A = B) : A <~> B
+  := BuildEquiv _ _ (transport (fun X:Type => X) p) admit.
+
+Class Univalence := { isequiv_equiv_path :> forall (A B : Type), IsEquiv (equiv_path A B) }.
+
+Section Univalence.
+  Context `{Univalence}.
+  Definition path_universe_uncurried {A B : Type} (f : A <~> B) : A = B
+    := (equiv_path A B)^-1 f.
+
+  Definition path_universe {A B : Type} (f : A -> B) {feq : IsEquiv f} : (A = B)
+    := path_universe_uncurried (BuildEquiv _ _ f feq).
+End Univalence.
+
+Definition e : Bool <~> Bool.
+  admit.
+Defined.
+
+Definition p `{Univalence} : Bool = Bool := path_universe e.
+
+Theorem thm `{Univalence} : (forall A, ((A -> False) -> False) -> A) -> False.
+  intro f.
+  Set Printing Universes.
+  Set Printing All.
+  pose proof (apD f (path_universe e)).
+  pose proof (apD f p).
+(* Toplevel input, characters 18-19:
+Error:
+In environment
+H : Univalence (* Top.148 Top.149 Top.150 Top.151 *)
+f : forall (A : Type (* Top.153 *))
+      (_ : forall _ : forall _ : A, False, False), A
+X : @paths (* Top.155 *)
+      ((fun A : Type (* Top.153 *) =>
+        forall _ : forall _ : forall _ : A, False, False, A) Bool)
+      (@transport (* Top.154 Top.155 *) Type (* Top.153 *)
+         (fun A : Type (* Top.153 *) =>
+          forall _ : forall _ : forall _ : A, False, False, A) Bool Bool
+         (@path_universe (* Top.148 Top.150 Top.151 Top.159 Top.153 Top.154
+            Top.149 Top.153 *) H Bool Bool
+            (equiv_fun (* Top.153 Top.153 *) Bool Bool e (* Top.153 *))
+            (equiv_isequiv (* Top.153 Top.153 *) Bool Bool e (* Top.153 *)))
+         (f Bool)) (f Bool)
+The term "@p (* Top.148 Top.172 Top.151 Top.150 Top.149 *) H" has type
+ "@paths (* Top.171 *) Set Bool Bool" while it is expected to have type
+ "@paths (* Top.169 *) Type (* Top.153 *) ?62 ?63"
+(Universe inconsistency: Cannot enforce Set = Top.153)). *)
diff --git a/test-suite/bugs/closed/HoTT_coq_063.v b/test-suite/bugs/closed/HoTT_coq_063.v
new file mode 100644
index 000000000..1c584d295
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_063.v
@@ -0,0 +1,26 @@
+Set Universe Polymorphism.
+Module A.
+  Inductive paths A (x : A) : A -> Type := idpath : paths A x x.
+
+  Notation "x = y" := (paths _ x y).
+
+  Inductive IsTrunc : nat -> Type -> Type :=
+  | BuildContr : forall A (center : A) (contr : forall y, center = y), IsTrunc 0 A
+  | trunc_S : forall A n, (forall x y : A, IsTrunc n (x = y)) -> IsTrunc (S n) A.
+
+  Existing Class IsTrunc.
+  (* Anomaly: Mismatched instance and context when building universe substitution.
+Please report. *)
+End A.
+
+Module B.
+  Fixpoint IsTrunc (n : nat) (A : Type) : Type :=
+    match n with
+      | O => True
+      | S _ => False
+    end.
+
+  Existing Class IsTrunc.
+  (* Anomaly: Mismatched instance and context when building universe substitution.
+Please report. *)
+End B.
diff --git a/test-suite/bugs/closed/HoTT_coq_064.v b/test-suite/bugs/closed/HoTT_coq_064.v
new file mode 100644
index 000000000..fae954f81
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_064.v
@@ -0,0 +1,187 @@
+(* File reduced by coq-bug-finder from 279 lines to 219 lines. *)
+
+Set Implicit Arguments.
+Set Universe Polymorphism.
+Definition admit {T} : T.
+Admitted.
+Module Export Overture.
+  Reserved Notation "g 'o' f" (at level 40, left associativity).
+
+  Inductive paths {A : Type} (a : A) : A -> Type :=
+    idpath : paths a a.
+
+  Arguments idpath {A a} , [A] a.
+
+  Notation "x = y :> A" := (@paths A x y) : type_scope.
+
+  Notation "x = y" := (x = y :>_) : type_scope.
+
+  Delimit Scope path_scope with path.
+
+  Local Open Scope path_scope.
+
+  Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+    := match p with idpath => idpath end.
+
+  Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g)
+  : forall x, f x = g x
+    := fun x => match h with idpath => idpath end.
+
+  Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { equiv_inv : B -> A }.
+
+  Delimit Scope equiv_scope with equiv.
+  Local Open Scope equiv_scope.
+
+  Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3) : equiv_scope.
+
+  Class Funext :=
+    { isequiv_apD10 :> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) }.
+
+  Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A, P x) :
+    (forall x, f x = g x) -> f = g
+    :=
+      (@apD10 A P f g)^-1.
+
+End Overture.
+
+Module Export Core.
+
+  Set Implicit Arguments.
+  Delimit Scope morphism_scope with morphism.
+  Delimit Scope category_scope with category.
+  Delimit Scope object_scope with object.
+
+  Record PreCategory :=
+    {
+      object :> Type;
+      morphism : object -> object -> Type;
+
+      compose : forall s d d',
+                  morphism d d'
+                  -> morphism s d
+                  -> morphism s d'
+                              where "f 'o' g" := (compose f g);
+
+      associativity : forall x1 x2 x3 x4
+                             (m1 : morphism x1 x2)
+                             (m2 : morphism x2 x3)
+                             (m3 : morphism x3 x4),
+                        (m3 o m2) o m1 = m3 o (m2 o m1)
+    }.
+  Bind Scope category_scope with PreCategory.
+  Arguments compose [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename.
+
+  Infix "o" := compose : morphism_scope.
+
+End Core.
+
+Local Open Scope morphism_scope.
+Record Functor (C D : PreCategory) :=
+  {
+    object_of :> C -> D;
+    morphism_of : forall s d, morphism C s d
+                              -> morphism D (object_of s) (object_of d)
+  }.
+
+Inductive Unit : Set :=
+  tt : Unit.
+
+Definition indiscrete_category (X : Type) : PreCategory
+  := @Build_PreCategory X
+                        (fun _ _ => Unit)
+                        (fun _ _ _ _ _ => tt)
+                        (fun _ _ _ _ _ _ _ => idpath).
+
+
+Record NaturalTransformation C D (F G : Functor C D) := { components_of :> forall c, morphism D (F c) (G c) }.
+Section path_natural_transformation.
+  Context `{Funext}.
+  Variable C : PreCategory.
+  Variable D : PreCategory.
+  Variables F G : Functor C D.
+
+  Section path.
+    Variables T U : NaturalTransformation F G.
+    Lemma path'_natural_transformation
+    : components_of T = components_of U
+      -> T = U.
+      admit.
+    Defined.
+    Lemma path_natural_transformation
+    : (forall x, T x = U x)
+      -> T = U.
+    Proof.
+      intros.
+      apply path'_natural_transformation.
+      apply path_forall; assumption.
+    Qed.
+  End path.
+End path_natural_transformation.
+Ltac path_natural_transformation :=
+  repeat match goal with
+           | _ => intro
+           | _ => apply path_natural_transformation; simpl
+         end.
+Definition comma_category A B C (S : Functor A C) (T : Functor B C)
+: PreCategory.
+  admit.
+Defined.
+Definition compose C D (F F' F'' : Functor C D)
+           (T' : NaturalTransformation F' F'') (T : NaturalTransformation F F')
+: NaturalTransformation F F''
+  := Build_NaturalTransformation F F''
+                                 (fun c => T' c o T c).
+
+Infix "o" := compose : natural_transformation_scope.
+
+Local Open Scope natural_transformation_scope.
+
+Definition associativity `{fs : Funext}
+           C D F G H I
+           (V : @NaturalTransformation C D F G)
+           (U : @NaturalTransformation C D G H)
+           (T : @NaturalTransformation C D H I)
+: (T o U) o V = T o (U o V).
+Proof.
+  path_natural_transformation.
+
+  apply associativity.
+Qed.
+Definition functor_category `{Funext} (C D : PreCategory) : PreCategory
+  := @Build_PreCategory (Functor C D)
+                        (@NaturalTransformation C D)
+                        (@compose C D)
+                        (@associativity _ C D).
+
+Notation "C -> D" := (functor_category C D) : category_scope.
+
+Definition compose_functor `{Funext} (C D E : PreCategory) : object ((C -> D) -> ((D -> E) -> (C -> E))).
+  admit.
+
+Defined.
+
+Definition pullback_along `{Funext} (C C' D : PreCategory) (p : Functor C C')
+: object ((C' -> D) -> (C -> D))
+  := Eval hnf in compose_functor _ _ _ p.
+
+Definition IsColimit `{Funext} C D (F : Functor D C) (x : object
+                                                            (@comma_category (indiscrete_category Unit)
+                                                                             (@functor_category H (indiscrete_category Unit) C)
+                                                                             (@functor_category H D C)
+                                                                             admit
+                                                                             (@pullback_along H D (indiscrete_category Unit) C
+                                                                                              admit))) : Type
+  := admit.
+
+Generalizable All Variables.
+Axiom fs : Funext.
+
+Section bar.
+
+  Variable D : PreCategory.
+
+  Context `(has_colimits
+            : forall F : Functor D C,
+                @IsColimit _ C D F (colimits F)).
+(* Error: Unsatisfied constraints: Top.3773 <= Set
+ (maybe a bugged tactic). *)
diff --git a/test-suite/bugs/closed/HoTT_coq_078.v b/test-suite/bugs/closed/HoTT_coq_078.v
new file mode 100644
index 000000000..6c02cad56
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_078.v
@@ -0,0 +1,45 @@
+Set Implicit Arguments.
+Require Import Logic.
+
+(*Global Set Universe Polymorphism.*)
+Global Set Asymmetric Patterns.
+Local Set Primitive Projections.
+
+Local Open Scope type_scope.
+
+Record prod (A B : Type) : Type :=
+  pair { fst : A; snd : B }.
+
+Arguments pair {A B} _ _.
+
+Notation "x * y" := (prod x y) : type_scope.
+Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
+
+Generalizable Variables X A B f g n.
+
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+
+Arguments idpath {A a} , [A] a.
+
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y :=
+  match p with idpath => u end.
+
+Definition transport_prod' {A : Type} {P Q : A -> Type} {a a' : A} (p : a = a')
+  (z : P a * Q a)
+  : transport (fun a => P a * Q a) p z  =  (transport _ p (fst z), transport _ p (snd z))
+  := match p as p' return transport (fun a0 => P a0 * Q a0) p' z = (transport P p' (fst z), transport Q p' (snd z)) with
+       | idpath => idpath
+     end. (* success *)
+
+Definition transport_prod {A : Type} {P Q : A -> Type} {a a' : A} (p : a = a')
+  (z : P a * Q a)
+  : transport (fun a => P a * Q a) p z  =  (transport _ p (fst z), transport _ p (snd z))
+  := match p with
+       | idpath => idpath
+     end.
+(** Toplevel input, characters 15-255:
+Error: Conversion test raised an anomaly *)
diff --git a/test-suite/bugs/closed/HoTT_coq_080.v b/test-suite/bugs/closed/HoTT_coq_080.v
new file mode 100644
index 000000000..36f478002
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_080.v
@@ -0,0 +1,34 @@
+Set Primitive Projections.
+Set Implicit Arguments.
+Set Universe Polymorphism.
+Set Asymmetric Patterns.
+
+Inductive sum A B := inl : A -> sum A B | inr : B -> sum A B.
+Inductive Empty :=.
+
+Record category :=
+  { ob :> Type;
+    hom : ob -> ob -> Type
+  }.
+Set Printing All.
+Definition sum_category (C D : category) : category :=
+  {|
+    ob := sum (ob C) (ob D);
+    hom x y := match x, y with
+                 | inl x, inl y => @hom C x y
+                 | inr x, inr y => @hom D x y
+                 | _, _ => Empty
+               end |}.
+
+Goal forall C D (x y : ob (sum_category C D)), Type.
+intros C D x y.
+hnf in x, y.
+exact (hom x y). (* Toplevel input, characters 26-27:
+Error:
+In environment
+C : category
+D : category
+x : sum (ob C) (ob D)
+y : sum (ob C) (ob D)
+The term "x" has type "sum (ob C) (ob D)" while it is expected to have type
+ "ob ?16". *)
diff --git a/test-suite/bugs/closed/HoTT_coq_081.v b/test-suite/bugs/closed/HoTT_coq_081.v
new file mode 100644
index 000000000..6de3ebdbd
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_081.v
@@ -0,0 +1,12 @@
+Set Primitive Projections.
+Set Implicit Arguments.
+Set Universe Polymorphism.
+
+Record category :=
+  { ob :> Type;
+    hom : ob -> ob -> Type
+  }.
+
+Record foo := { C : category; x :> ob C }.
+(* Toplevel input, characters 0-42:
+Error: Cannot find the target class. *)
diff --git a/test-suite/bugs/closed/HoTT_coq_082.v b/test-suite/bugs/closed/HoTT_coq_082.v
new file mode 100644
index 000000000..03886695c
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_082.v
@@ -0,0 +1,19 @@
+Set Implicit Arguments.
+Set Universe Polymorphism.
+
+Record category :=
+  { ob : Type }.
+
+Existing Class category. (*
+Toplevel input, characters 0-24:
+Anomaly: Mismatched instance and context when building universe substitution.
+Please report. *)
+
+Record category' :=
+  { ob : Type;
+    hom : ob -> ob -> Type }.
+
+Existing Class category'. (*
+Toplevel input, characters 0-24:
+Anomaly: Mismatched instance and context when building universe substitution.
+Please report. *)
diff --git a/test-suite/bugs/closed/HoTT_coq_083.v b/test-suite/bugs/closed/HoTT_coq_083.v
new file mode 100644
index 000000000..494b25c7b
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_083.v
@@ -0,0 +1,29 @@
+Set Primitive Projections.
+Set Implicit Arguments.
+Set Universe Polymorphism.
+
+Record category :=
+  { ob : Type }.
+
+Goal forall C, ob C -> ob C.
+intros.
+generalize dependent (ob C).
+(* 1 subgoals, subgoal 1 (ID 7)
+
+  C : category
+  ============================
+   forall T : Type, T -> T
+(dependent evars:) *)
+intros T t.
+Undo 2.
+generalize dependent (@ob C).
+(* 1 subgoals, subgoal 1 (ID 6)
+
+  C : category
+  X : ob C
+  ============================
+   Type -> ob C
+(dependent evars:) *)
+intros T t.
+(* Toplevel input, characters 9-10:
+Error: No product even after head-reduction. *)
diff --git a/test-suite/bugs/closed/HoTT_coq_084.v b/test-suite/bugs/closed/HoTT_coq_084.v
new file mode 100644
index 000000000..d007e4e23
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_084.v
@@ -0,0 +1,49 @@
+Set Implicit Arguments.
+Set Universe Polymorphism.
+
+Module success.
+  Unset Primitive Projections.
+
+  Record group :=
+    { carrier : Type;
+      id : carrier }.
+
+  Notation "1" := (id _) : g_scope.
+
+  Delimit Scope g_scope with g.
+  Bind Scope g_scope with carrier.
+
+  Section foo.
+    Variable g : group.
+    Variable comp : carrier g -> carrier g -> carrier g.
+
+    Check comp 1 1.
+  End foo.
+End success.
+
+Module failure.
+  Set Primitive Projections.
+
+  Record group :=
+    { carrier : Type;
+      id : carrier }.
+
+  Notation "1" := (id _) : g_scope.
+
+  Delimit Scope g_scope with g.
+  Bind Scope g_scope with carrier.
+
+  Section foo.
+    Variable g : group.
+    Variable comp : carrier g -> carrier g -> carrier g.
+
+    Check comp 1 1.
+    (* Toplevel input, characters 11-12:
+Error:
+In environment
+g : group
+comp : carrier g -> carrier g -> carrier g
+The term "1" has type "nat" while it is expected to have type "carrier g".
+    *)
+  End foo.
+End failure.
diff --git a/test-suite/bugs/closed/HoTT_coq_085.v b/test-suite/bugs/closed/HoTT_coq_085.v
new file mode 100644
index 000000000..041c67997
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_085.v
@@ -0,0 +1,74 @@
+Set Implicit Arguments.
+Set Universe Polymorphism.
+
+Module success.
+  Unset Primitive Projections.
+
+  Record category :=
+    { ob : Type;
+      hom : ob -> ob -> Type;
+      comp : forall x y z, hom y z -> hom x y -> hom x z }.
+
+  Delimit Scope hom_scope with hom.
+  Bind Scope hom_scope with hom.
+  Arguments hom : clear implicits.
+  Arguments comp _ _ _ _ _%hom _%hom : clear implicits.
+
+  Notation "f 'o' g" := (comp _ _ _ _ f g) (at level 40, left associativity) : hom_scope.
+
+  Record functor (C D : category) :=
+    { ob_of : ob C -> ob D;
+      hom_of : forall x y, hom C x y -> hom D (ob_of x) (ob_of y) }.
+
+  Delimit Scope functor_scope with functor.
+  Bind Scope functor_scope with functor.
+
+  Arguments hom_of _ _ _%functor _ _ _%hom.
+
+  Notation "F '_1' m" := (hom_of F _ _ m) (at level 10, no associativity) : hom_scope.
+
+  Axiom f_comp : forall C D E, functor D E -> functor C D -> functor C E.
+  Notation "f 'o' g" := (@f_comp _ _ _ f g) (at level 40, left associativity) : functor_scope.
+
+  Check ((_ o _) _1 _)%hom. (* ((?16 o ?17) _1 ?20)%hom
+     : hom ?15 (ob_of (?16 o ?17) ?18) (ob_of (?16 o ?17) ?19) *)
+End success.
+
+Module failure.
+  Set Primitive Projections.
+
+  Record category :=
+    { ob : Type;
+      hom : ob -> ob -> Type;
+      comp : forall x y z, hom y z -> hom x y -> hom x z }.
+
+  Delimit Scope hom_scope with hom.
+  Bind Scope hom_scope with hom.
+  Arguments hom : clear implicits.
+  Arguments comp _ _ _ _ _%hom _%hom : clear implicits.
+
+  Notation "f 'o' g" := (comp _ _ _ _ f g) (at level 40, left associativity) : hom_scope.
+
+  Record functor (C D : category) :=
+    { ob_of : ob C -> ob D;
+      hom_of : forall x y, hom C x y -> hom D (ob_of x) (ob_of y) }.
+
+  Delimit Scope functor_scope with functor.
+  Bind Scope functor_scope with functor.
+
+  Arguments hom_of _ _ _%functor _ _ _%hom.
+
+  Notation "F '_1' m" := (hom_of F _ _ m) (at level 10, no associativity) : hom_scope.
+  Notation "F '_2' m" := (hom_of F%functor _ _ m) (at level 10, no associativity) : hom_scope.
+
+  Axiom f_comp : forall C D E, functor D E -> functor C D -> functor C E.
+  Notation "f 'o' g" := (@f_comp _ _ _ f g) (at level 40, left associativity) : functor_scope.
+
+  Check ((_ o _) _2 _)%hom. (* ((?14 o ?15)%functor _1 ?18)%hom
+     : hom ?13 (ob_of (?14 o ?15)%functor ?16)
+         (ob_of (?14 o ?15)%functor ?17) *)
+  Check ((_ o _) _1 _)%hom. (* Toplevel input, characters 7-19:
+Error:
+The term "(?23 o ?24)%hom" has type "hom ?19 ?20 ?22"
+while it is expected to have type "functor ?25 ?26". *)
+End failure.
diff --git a/test-suite/bugs/closed/HoTT_coq_089.v b/test-suite/bugs/closed/HoTT_coq_089.v
new file mode 100644
index 000000000..54ae4704a
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_089.v
@@ -0,0 +1,42 @@
+Set Universe Polymorphism.
+Set Printing Universes.
+
+Inductive type_paths (A : Type) : Type -> Prop
+  := idtypepath : type_paths A A.
+Monomorphic Definition comp_type_paths := Eval compute in type_paths.
+Check comp_type_paths.
+(* comp_type_paths
+     : Type (* Top.12 *) -> Type (* Top.12 *) -> Prop *)
+(* This is terrible. *)
+
+Inductive type_paths' (A : Type) : Type -> Prop
+  := idtypepath' : type_paths' A A
+   | other_type_path : False -> forall B : Set, type_paths' A B.
+Monomorphic Definition comp_type_paths' := Eval compute in type_paths'.
+Check comp_type_paths'.
+(* comp_type_paths'
+     : Type (* Top.24 *) -> Type (* Top.23 *) -> Prop *)
+(* Ok, then ... *)
+
+(** Fail if it's [U0 -> U0 -> _], but not on [U0 -> U1 -> _]. *)
+Goal Type.
+Proof.
+  match type of comp_type_paths' with
+    | ?U0 -> ?U1 -> ?R
+      => exact (@comp_type_paths' nat U0)
+  end.
+Defined.
+
+Goal Type.
+Proof.
+  match type of comp_type_paths with
+    | ?U0 -> ?U1 -> ?R
+      => exact (@comp_type_paths nat U0)
+  end.
+  (* Toplevel input, characters 110-112:
+Error:
+The term "Type (* Top.51 *)" has type "Type (* Top.51+1 *)"
+while it is expected to have type "Type (* Top.51 *)"
+(Universe inconsistency: Cannot enforce Top.51 < Top.51 because Top.51
+= Top.51)). *)
+Defined.
diff --git a/test-suite/bugs/closed/HoTT_coq_098.v b/test-suite/bugs/closed/HoTT_coq_098.v
new file mode 100644
index 000000000..1e7be20d5
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_098.v
@@ -0,0 +1,84 @@
+Set Implicit Arguments.
+Generalizable All Variables.
+
+Polymorphic Record SpecializedCategory (obj : Type) := Build_SpecializedCategory' {
+  Object :> _ := obj;
+  Morphism' : obj -> obj -> Type;
+
+  Identity' : forall o, Morphism' o o;
+  Compose' : forall s d d', Morphism' d d' -> Morphism' s d -> Morphism' s d'
+}.
+
+Polymorphic Definition TypeCat : @SpecializedCategory Type
+  := (@Build_SpecializedCategory' Type
+                                  (fun s d => s -> d)
+                                  (fun _ => (fun x => x))
+                                  (fun _ _ _ f g => (fun x => f (g x)))).
+
+Inductive GraphIndex := GraphIndexSource | GraphIndexTarget.
+Polymorphic Definition GraphIndexingCategory : @SpecializedCategory GraphIndex.
+Admitted.
+
+Module success.
+  Section SpecializedFunctor.
+    Set Universe Polymorphism.
+    Context `(C : @SpecializedCategory objC).
+    Context `(D : @SpecializedCategory objD).
+    Unset Universe Polymorphism.
+
+    Polymorphic Record SpecializedFunctor
+      := {
+          ObjectOf' : objC -> objD;
+          MorphismOf' : forall s d, C.(Morphism') s d -> D.(Morphism') (ObjectOf' s) (ObjectOf' d)
+        }.
+  End SpecializedFunctor.
+
+  Polymorphic Definition UnderlyingGraph : SpecializedFunctor GraphIndexingCategory TypeCat.
+  Admitted.
+End success.
+
+Module failure.
+  Section SpecializedFunctor.
+    Context `(C : @SpecializedCategory objC).
+    Context `(D : @SpecializedCategory objD).
+
+    Polymorphic Record SpecializedFunctor
+      := {
+          ObjectOf' : objC -> objD;
+          MorphismOf' : forall s d, C.(Morphism') s d -> D.(Morphism') (ObjectOf' s) (ObjectOf' d)
+        }.
+  End SpecializedFunctor.
+
+  Set Printing Universes.
+  Fail Polymorphic Definition UnderlyingGraph : SpecializedFunctor GraphIndexingCategory TypeCat.
+  (* Toplevel input, characters 73-94:
+Error:
+The term "GraphIndexingCategory (* Top.563 *)" has type
+ "SpecializedCategory (* Top.563 Set *) GraphIndex"
+while it is expected to have type
+ "SpecializedCategory (* Top.550 Top.551 *) ?7"
+(Universe inconsistency: Cannot enforce Set = Top.551)). *)
+End failure.
+
+Module polycontext.
+  Section SpecializedFunctor.
+    Polymorphic Context `(C : @SpecializedCategory objC).
+    Polymorphic Context `(D : @SpecializedCategory objD).
+
+    Polymorphic Record SpecializedFunctor
+      := {
+          ObjectOf' : objC -> objD;
+          MorphismOf' : forall s d, C.(Morphism') s d -> D.(Morphism') (ObjectOf' s) (ObjectOf' d)
+        }.
+  End SpecializedFunctor.
+
+  Set Printing Universes.
+  Fail Polymorphic Definition UnderlyingGraph : SpecializedFunctor GraphIndexingCategory TypeCat.
+  (* Toplevel input, characters 73-94:
+Error:
+The term "GraphIndexingCategory (* Top.563 *)" has type
+ "SpecializedCategory (* Top.563 Set *) GraphIndex"
+while it is expected to have type
+ "SpecializedCategory (* Top.550 Top.551 *) ?7"
+(Universe inconsistency: Cannot enforce Set = Top.551)). *)
+End polycontext.
diff --git a/test-suite/bugs/closed/HoTT_coq_101.v b/test-suite/bugs/closed/HoTT_coq_101.v
new file mode 100644
index 000000000..9c89a6ab9
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_101.v
@@ -0,0 +1,77 @@
+Set Universe Polymorphism.
+Set Implicit Arguments.
+Generalizable All Variables.
+
+Record SpecializedCategory (obj : Type) :=
+  {
+    Object :> _ := obj;
+    Morphism : obj -> obj -> Type
+  }.
+
+
+Record > Category :=
+  {
+    CObject : Type;
+
+    UnderlyingCategory :> @SpecializedCategory CObject
+  }.
+
+Record SpecializedFunctor `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) :=
+  {
+    ObjectOf :> objC -> objD;
+    MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d)
+  }.
+
+(* Replacing this with [Definition Functor (C D : Category) :=
+SpecializedFunctor C D.] gets rid of the universe inconsistency. *)
+Section Functor.
+  Variable C D : Category.
+
+  Definition Functor := SpecializedFunctor C D.
+End Functor.
+
+Record SpecializedNaturalTransformation `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) (F G : SpecializedFunctor C D) :=
+  {
+    ComponentsOf :> forall c, D.(Morphism) (F c) (G c)
+  }.
+
+Definition FunctorProduct' `(F : Functor C D) : SpecializedFunctor C D.
+admit.
+Defined.
+
+Definition TypeCat : @SpecializedCategory Type.
+  admit.
+Defined.
+
+
+Definition CovariantHomFunctor `(C : @SpecializedCategory objC) : SpecializedFunctor C TypeCat.
+  refine (Build_SpecializedFunctor C TypeCat
+                                   (fun X : C => C.(Morphism) X X)
+                                   _
+         ); admit.
+Defined.
+
+Definition FunctorCategory `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) : @SpecializedCategory (SpecializedFunctor C D).
+  refine (@Build_SpecializedCategory _
+                                     (SpecializedNaturalTransformation (C := C) (D := D))).
+Defined.
+
+Definition Yoneda `(C : @SpecializedCategory objC) : SpecializedFunctor C (FunctorCategory C TypeCat).
+  match goal with
+    | [ |- SpecializedFunctor ?C0 ?D0 ] =>
+      refine (Build_SpecializedFunctor C0 D0
+                                       (fun c => CovariantHomFunctor C)
+                                       _
+             )
+  end;
+  admit.
+Defined.
+
+Section FullyFaithful.
+  Context `(C : @SpecializedCategory objC).
+  Let TypeCatC := FunctorCategory C TypeCat.
+  Let YC := (Yoneda C).
+  Set Printing Universes.
+  Check @FunctorProduct' C TypeCatC YC. (* Toplevel input, characters 0-37:
+Error: Universe inconsistency. Cannot enforce Top.187 = Top.186 because
+Top.186 <= Top.189 < Top.191 <= Top.187). *)
diff --git a/test-suite/bugs/closed/HoTT_coq_102.v b/test-suite/bugs/closed/HoTT_coq_102.v
new file mode 100644
index 000000000..72b4ffe94
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_102.v
@@ -0,0 +1,23 @@
+(* File reduced by coq-bug-finder from 64 lines to 30 lines. *)
+Set Implicit Arguments.
+Set Universe Polymorphism.
+Generalizable All Variables.
+Record SpecializedCategory (obj : Type) := { Object :> _ := obj }.
+
+Record > Category :=
+  { CObject : Type;
+    UnderlyingCategory :> @SpecializedCategory CObject }.
+
+Record SpecializedFunctor `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) :=
+  { ObjectOf :> objC -> objD }.
+
+Definition Functor (C D : Category) := SpecializedFunctor C D.
+
+Parameter TerminalCategory : SpecializedCategory unit.
+
+Definition focus A (_ : A) := True.
+
+Definition CommaCategory_Object (A : Category) (S : Functor TerminalCategory A) : Type.
+  assert (Hf : focus ((S tt) = (S tt))) by constructor.
+  progress change CObject with (fun C => @Object (CObject C) C) in *.
+  (* not convertible *)
diff --git a/test-suite/bugs/closed/HoTT_coq_103.v b/test-suite/bugs/closed/HoTT_coq_103.v
new file mode 100644
index 000000000..7b1dc8dea
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_103.v
@@ -0,0 +1,4 @@
+Check (nat : Type) : Set.
+(* Error:
+The term "nat:Type" has type "Type" while it is expected to have type
+"Set" (Universe inconsistency). *)
diff --git a/test-suite/bugs/closed/HoTT_coq_104.v b/test-suite/bugs/closed/HoTT_coq_104.v
new file mode 100644
index 000000000..5bb7fa8c1
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_104.v
@@ -0,0 +1,13 @@
+Set Implicit Arguments.
+
+Require Import Logic.
+
+Global Set Universe Polymorphism.
+Global Set Asymmetric Patterns.
+Local Set Record Elimination Schemes.
+Local Set Primitive Projections.
+
+Record prod (A B : Type) : Type :=
+  pair { fst : A; snd : B }.
+
+Check fun x : prod Set Set => eq_refl : x = pair (fst x) (snd x).
diff --git a/test-suite/bugs/closed/HoTT_coq_105.v b/test-suite/bugs/closed/HoTT_coq_105.v
new file mode 100644
index 000000000..86001d26e
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_105.v
@@ -0,0 +1,32 @@
+Set Primitive Projections.
+Set Implicit Arguments.
+Set Universe Polymorphism.
+Set Asymmetric Patterns.
+
+Inductive sum A B := inl : A -> sum A B | inr : B -> sum A B.
+Inductive Empty :=.
+
+Record category :=
+  { ob :> Type;
+    hom : ob -> ob -> Type
+  }.
+Set Printing All.
+Definition sum_category (C D : category) : category :=
+  {|
+    ob := sum (ob C) (ob D);
+    hom x y := match x, y with
+                 | inl x, inl y => @hom _ x y (* Toplevel input, characters 177-178:
+Error:
+In environment
+C : category
+D : category
+x : sum (ob C) (ob D)
+y : sum (ob C) (ob D)
+x0 : ob C
+y0 : ob C
+The term "x0" has type "ob C" while it is expected to have type
+"ob ?6" (unable to find a well-typed instantiation for
+"?6": cannot unify"Type" and "category"). *)
+                 | inr x, inr y => @hom _ x y
+                 | _, _ => Empty
+               end |}.
diff --git a/test-suite/bugs/closed/HoTT_coq_106.v b/test-suite/bugs/closed/HoTT_coq_106.v
new file mode 100644
index 000000000..d3ef9f58c
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_106.v
@@ -0,0 +1,51 @@
+(* File reduced by coq-bug-finder from 520 lines to 9 lines. *)
+Set Universe Polymorphism.
+Class IsPointed (A : Type) := point : A.
+
+Generalizable Variables A B f.
+
+Instance ispointed_forall `{H : forall a : A, IsPointed (B a)}
+: IsPointed (forall a, B a)
+  := fun a => @point (B a) (H a).
+
+Instance ispointed_sigma `{IsPointed A} `{IsPointed (B (point A))}
+: IsPointed (sigT B).
+(* Toplevel input, characters 20-108:
+Error: Unable to satisfy the following constraints:
+UNDEFINED EVARS:
+ ?8==[A H B |- IsPointed (forall x : Type, ?13)] (parameter IsPointed of
+       @point)
+ ?12==[A H {B} x |- Type] (parameter A of @point)
+ ?13==[A H {B} x |- Type] (parameter A of @point)
+ ?15==[A H {B} x |- Type] (parameter A of @point)UNIVERSES:
+ {Top.38 Top.30 Top.39 Top.40 Top.29 Top.36 Top.31 Top.35 Top.37 Top.34 Top.32 Top.33} |= Top.30 < Top.29
+                                                  Top.30 < Top.36
+                                                  Top.32 < Top.34
+                                                  Top.38 <= Top.37
+                                                  Top.38 <= Top.33
+                                                  Top.40 <= Top.38
+                                                  Top.40 <= Coq.Init.Specif.7
+                                                  Top.40 <= Top.39
+                                                  Top.36 <= Top.35
+                                                  Top.37 <= Top.35
+                                                  Top.34 <= Top.31
+                                                  Top.32 <= Top.39
+                                                  Top.32 <= Coq.Init.Specif.8
+                                                  Top.33 <= Top.31
+
+ALGEBRAIC UNIVERSES:
+ {Top.38 Top.40 Top.29 Top.36 Top.31 Top.37 Top.34 Top.33}
+UNDEFINED UNIVERSES:
+ Top.38
+ Top.30
+ Top.39
+ Top.40
+ Top.29
+ Top.36
+ Top.31
+ Top.35
+ Top.37
+ Top.34
+ Top.32
+ Top.33CONSTRAINTS:[] [A H B] |- ?13 == ?12
+[] [A H B H0] |- ?12 == ?15 *)
diff --git a/test-suite/bugs/closed/HoTT_coq_107.v b/test-suite/bugs/closed/HoTT_coq_107.v
new file mode 100644
index 000000000..c3a83627e
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_107.v
@@ -0,0 +1,106 @@
+(* -*- mode: coq; coq-prog-args: ("-nois" "-emacs") -*- *)
+(* File reduced by coq-bug-finder from 4897 lines to 2605 lines, then from 2297 lines to 236 lines, then from 239 lines to 137 lines, then from 118 lines to 67 lines, then from 520 lines to 76 lines. *)
+(** Note: The bug here is the same as the #113, that is, HoTT_coq_113.v *)
+Require Import Coq.Init.Logic.
+Global Set Universe Polymorphism.
+Global Set Asymmetric Patterns.
+Set Implicit Arguments.
+
+Inductive sigT (A:Type) (P:A -> Type) : Type :=
+  existT : forall x:A, P x -> sigT P.
+
+Notation "{ x : A  & P }" := (sigT (fun x:A => P)) : type_scope.
+
+Generalizable All Variables.
+Definition admit {T} : T.
+Admitted.
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y :=
+  match p with idpath => u end.
+Class Contr_internal (A : Type) :=
+  BuildContr {
+      center : A ;
+      contr : (forall y : A, center = y)
+    }.
+
+Arguments center A {_}.
+
+Inductive trunc_index : Type :=
+| minus_two : trunc_index
+| trunc_S : trunc_index -> trunc_index.
+
+Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
+  match n with
+    | minus_two => Contr_internal A
+    | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y)
+  end.
+
+Class IsTrunc (n : trunc_index) (A : Type) : Type :=
+  Trunc_is_trunc : IsTrunc_internal n A.
+
+Notation Contr := (IsTrunc minus_two).
+
+Hint Extern 0 => progress change Contr_internal with Contr in * : typeclass_instances.
+
+Definition path_contr `{Contr A} (x y : A) : x = y
+  := admit.
+
+Definition path_sigma' {A : Type} (P : A -> Type) {x x' : A} {y : P x} {y' : P x'}
+           (p : x = x') (q : transport _ p y = y')
+: existT _ x y = existT _ x' y'
+  := admit.
+Instance trunc_sigma `{P : A -> Type}
+         `{IsTrunc n A} `{forall a, IsTrunc n (P a)}
+: IsTrunc n (sigT P) | 100.
+
+Proof.
+  generalize dependent A.
+  induction n; [ | admit ]; simpl; intros A P ac Pc.
+  (exists (existT _ (center A) (center (P (center A))))).
+  intros [a ?].
+  refine (path_sigma' P (contr a) (path_contr _ _)).
+Defined.
+Inductive Bool : Set := true | false.
+Definition trunc_sum' n A B `{IsTrunc n Bool, IsTrunc n A, IsTrunc n B}
+: (IsTrunc n { b : Bool & if b then A else B }).
+Proof.
+  Set Printing All.
+  Set Printing Universes.
+  refine (@trunc_sigma Bool (fun b => if b then A else B) n _ _).
+  (* Toplevel input, characters 23-76:
+Error:
+In environment
+n : trunc_index
+A : Type (* Top.193 *)
+B : Type (* Top.194 *)
+H : IsTrunc (* Set *) n Bool
+H0 : IsTrunc (* Top.193 *) n A
+H1 : IsTrunc (* Top.194 *) n B
+The term
+ "@trunc_sigma (* Top.198 Top.199 Top.200 Top.201 *) Bool
+    (fun b : Bool =>
+     match b return Type (* Top.199 *) with
+     | true => A
+     | false => B
+     end) n ?49 ?50" has type
+ "IsTrunc (* Top.200 *) n
+    (@sig (* Top.199 Top.199 *) Bool
+       (fun b : Bool =>
+        match b return Type (* Top.199 *) with
+        | true => A
+        | false => B
+        end))" while it is expected to have type
+ "IsTrunc (* Top.195 *) n
+    (@sig (* Set Top.197 *) Bool
+       (fun b : Bool =>
+        match b return Type (* Top.197 *) with
+        | true => A
+        | false => B
+        end))" (Universe inconsistency: Cannot enforce Top.197 = Set)).
+ *)
+  admit.
+Defined.
diff --git a/test-suite/bugs/closed/HoTT_coq_110.v b/test-suite/bugs/closed/HoTT_coq_110.v
new file mode 100644
index 000000000..5ec40dbcb
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_110.v
@@ -0,0 +1,23 @@
+Module X.
+  Inductive paths A (x : A) : A -> Type := idpath : paths A x x.
+  Notation "x = y" := (@paths _ x y) : type_scope.
+
+  Axioms A B : Type.
+  Axiom P : A = B.
+  Definition foo : A = B.
+    abstract (rewrite <- P; reflexivity).
+  (* Error: internal_paths_rew already exists. *)
+  Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *)
+End X.
+
+Module Y.
+  Inductive paths A (x : A) : A -> Type := idpath : paths A x x.
+  Notation "x = y" := (@paths _ x y) : type_scope.
+
+  Axioms A B : Type.
+  Axiom P : A = B.
+  Definition foo : (A = B) * (A = B).
+    split; abstract (rewrite <- P; reflexivity).
+  (* Error: internal_paths_rew already exists. *)
+  Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *)
+End Y.
diff --git a/test-suite/bugs/closed/HoTT_coq_111.v b/test-suite/bugs/closed/HoTT_coq_111.v
new file mode 100644
index 000000000..56feadb40
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_111.v
@@ -0,0 +1,25 @@
+Module X.
+  Set Universe Polymorphism.
+  Inductive paths A (x : A) : forall _ : A, Type := idpath : paths A x x.
+  Notation "x = y" := (@paths _ x y) (at level 70, no associativity) : type_scope.
+
+  Axioms A B : Type.
+  Axiom P : A = B.
+  Definition foo : A = B.
+    abstract (rewrite <- P; reflexivity).
+  (* Error: internal_paths_rew already exists. *)
+  Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *)
+End X.
+
+Module Y.
+  Set Universe Polymorphism.
+  Inductive paths A (x : A) : forall _ : A, Type := idpath : paths A x x.
+  Notation "x = y" := (@paths _ x y) (at level 70, no associativity) : type_scope.
+
+  Axioms A B : Type.
+  Axiom P : A = B.
+  Definition foo : (A = B) * (A = B).
+    split; abstract (rewrite <- P; reflexivity).
+  (* Error: internal_paths_rew already exists. *)
+  Defined. (* Anomaly: Uncaught exception Not_found(_). Please report. *)
+End Y.
diff --git a/test-suite/bugs/closed/HoTT_coq_113.v b/test-suite/bugs/closed/HoTT_coq_113.v
new file mode 100644
index 000000000..3ef531bc9
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_113.v
@@ -0,0 +1,19 @@
+(* File reduced by coq-bug-finder from original input, then from 3329 lines to 153 lines, then from 118 lines to 49 lines, then from 55 lines to 38 lines, then from 46 lines to 16 lines *)
+
+Generalizable All Variables.
+Set Universe Polymorphism.
+Class Foo (A : Type) := {}.
+Definition Baz := Foo.
+Definition Bar {A B} `{Foo A, Foo B} : True.
+Proof.
+  Set Printing Universes.
+  (* [change] should give fresh universes for each [Foo] *)
+  change Foo with Baz in *.
+  admit.
+Defined.
+Definition foo := @Bar nat.
+Check @foo Set.
+(* Toplevel input, characters 26-29:
+Error:
+The term "Set" has type "Type (* Set+1 *)" while it is expected to have type
+ "Set" (Universe inconsistency: Cannot enforce Set < Set because Set = Set)). *)
diff --git a/test-suite/bugs/closed/HoTT_coq_115.v b/test-suite/bugs/closed/HoTT_coq_115.v
new file mode 100644
index 000000000..c1e133eeb
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_115.v
@@ -0,0 +1 @@
+Inductive T : let U := Type in U := t. (* Anomaly: not an arity. Please report. *)
diff --git a/test-suite/bugs/closed/HoTT_coq_120.v b/test-suite/bugs/closed/HoTT_coq_120.v
new file mode 100644
index 000000000..7a0494911
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_120.v
@@ -0,0 +1,136 @@
+(* File reduced by coq-bug-finder from original input, then from 8249 lines to 907 lines, then from 843 lines to 357 lines, then from 351 lines to 260 lines, then from 208 lines to 162 lines, then from 167 lines to 154 lines *)
+Set Universe Polymorphism.
+Generalizable All Variables.
+Reserved Notation "g 'o' f" (at level 40, left associativity).
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+Arguments idpath {A a} , [A] a.
+Notation "x = y" := (@paths _ x y) : type_scope.
+
+Class IsEquiv {A B : Type} (f : A -> B) := {}.
+
+Class Contr_internal (A : Type) := BuildContr {
+                                       center : A ;
+                                       contr : (forall y : A, center = y)
+                                     }.
+
+Inductive trunc_index : Type :=
+| minus_two : trunc_index
+| trunc_S : trunc_index -> trunc_index.
+
+Fixpoint nat_to_trunc_index (n : nat) : trunc_index
+  := match n with
+       | 0 => trunc_S (trunc_S minus_two)
+       | S n' => trunc_S (nat_to_trunc_index n')
+     end.
+
+Coercion nat_to_trunc_index : nat >-> trunc_index.
+
+Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
+  match n with
+    | minus_two => Contr_internal A
+    | trunc_S n' => forall (x y : A), IsTrunc_internal n' (x = y)
+  end.
+
+Notation minus_one:=(trunc_S minus_two).
+
+Class IsTrunc (n : trunc_index) (A : Type) : Type := Trunc_is_trunc : IsTrunc_internal n A.
+
+Notation Contr := (IsTrunc minus_two).
+Notation IsHProp := (IsTrunc minus_one).
+Notation IsHSet := (IsTrunc 0).
+
+Class Funext := {}.
+Inductive Unit : Set := tt.
+
+Instance contr_unit : Contr Unit | 0 := let x := {|
+                                              center := tt;
+                                              contr := fun t : Unit => match t with tt => idpath end
+                                            |} in x.
+Instance trunc_succ `{IsTrunc n A} : IsTrunc (trunc_S n) A | 1000.
+admit.
+Defined.
+Record hProp := hp { hproptype :> Type ; isp : IsHProp hproptype}.
+Definition Unit_hp:hProp:=(hp Unit _).
+Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}.
+Canonical Structure default_HSet:= fun T P => (@BuildhSet T P).
+Definition ismono {X Y} (f : X -> Y)
+  := forall Z : hSet,
+     forall g h : Z -> X, (fun x => f (g x)) = (fun x => f (h x)) -> g = h.
+
+Delimit Scope morphism_scope with morphism.
+Delimit Scope category_scope with category.
+Delimit Scope object_scope with object.
+Record PreCategory :=
+  Build_PreCategory {
+      object :> Type;
+      morphism : object -> object -> Type;
+      compose : forall s d d', morphism d d' -> morphism s d -> morphism s d'
+    }.
+Arguments compose [!C s d d'] m1 m2 : rename.
+
+Infix "o" := compose : morphism_scope.
+Local Open Scope morphism_scope.
+
+Class IsEpimorphism {C} {x y} (m : morphism C x y) :=
+  is_epimorphism : forall z (m1 m2 : morphism C y z),
+                     m1 o m = m2 o m
+                     -> m1 = m2.
+
+Class IsMonomorphism {C} {x y} (m : morphism C x y) :=
+  is_monomorphism : forall z (m1 m2 : morphism C z x),
+                      m o m1 = m o m2
+                      -> m1 = m2.
+Class Univalence := {}.
+Global Instance isset_hProp `{Funext} : IsHSet hProp | 0. Admitted.
+
+Definition set_cat : PreCategory
+  := @Build_PreCategory hSet
+                        (fun x y => forall _ : x, y)%core
+                        (fun _ _ _ f g x => f (g x))%core.
+Local Inductive minus1Trunc (A :Type) : Type := min1 : A -> minus1Trunc A.
+Instance minus1Trunc_is_prop {A : Type} : IsHProp (minus1Trunc A) | 0. Admitted.
+Definition hexists {X} (P:X->Type):Type:= minus1Trunc (sigT  P).
+Definition isepi {X Y} `(f:X->Y) := forall Z: hSet,
+                                    forall g h: Y -> Z, (fun x => g (f x)) = (fun x => h (f x)) -> g = h.
+Definition issurj {X Y} (f:X->Y) := forall y:Y , hexists (fun x => (f x) = y).
+Lemma isepi_issurj `{fs:Funext} `{ua:Univalence} `{fs' : Funext} {X Y} (f:X->Y): isepi f -> issurj f.
+Proof.
+  intros epif y.
+  set (g :=fun _:Y => Unit_hp).
+  set (h:=(fun y:Y => (hp (hexists (fun _ : Unit => {x:X & y = (f x)})) _ ))).
+  clear fs'.
+  hnf in epif.
+  specialize (epif (BuildhSet hProp _) g h).
+  admit.
+Defined.
+Definition isequiv_isepi_ismono `{Univalence, fs0 : Funext} (X Y : hSet) (f : X -> Y) (epif : isepi f) (monof : ismono f)
+: IsEquiv f.
+Proof.
+  pose proof (@isepi_issurj _ _ _ _ _ f epif) as surjf.
+  admit.
+Defined.
+Section fully_faithful_helpers.
+  Context `{fs0 : Funext}.
+  Variables x y : hSet.
+  Variable m : x -> y.
+
+  Let isequiv_isepi_ismono_helper ua := (@isequiv_isepi_ismono ua fs0 x y m : isepi m -> ismono m -> IsEquiv m).
+
+  Goal True.
+  set (isequiv_isepimorphism_ismonomorphism
+       := fun `{Univalence}
+              (Hepi : IsEpimorphism (m : morphism set_cat x y))
+              (Hmono : IsMonomorphism (m : morphism set_cat x y))
+          => (@isequiv_isepi_ismono_helper _ Hepi Hmono : @IsEquiv _ _ m)).
+  admit.
+  Undo.
+  set (isequiv_isepimorphism_ismonomorphism'
+       := fun `{Univalence}
+              (Hepi : IsEpimorphism (m : morphism set_cat x y))
+              (Hmono : IsMonomorphism (m : morphism set_cat x y))
+          => ((let _ := @isequiv_isepimorphism_ismonomorphism _ Hepi Hmono in @isequiv_isepi_ismono _ fs0 x y m Hepi Hmono)
+              : @IsEquiv _ _ m)).
+  Set Printing Universes.
+  admit. (* Error: Universe inconsistency (cannot enforce Top.235 <= Set because Set
+< Top.235). *)
diff --git a/test-suite/bugs/closed/HoTT_coq_122.v b/test-suite/bugs/closed/HoTT_coq_122.v
new file mode 100644
index 000000000..1ba8e5c34
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_122.v
@@ -0,0 +1,25 @@
+(* File reduced by coq-bug-finder from original input, then from 669 lines to 79 lines, then from 89 lines to 44 lines *)
+Set Primitive Projections.
+Reserved Notation "g 'o' f" (at level 40, left associativity).
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+Notation "x = y" := (@paths _ x y) : type_scope.
+
+Set Implicit Arguments.
+
+Record PreCategory :=
+  Build_PreCategory' {
+      object :> Type;
+      morphism : object -> object -> Type;
+
+      identity : forall x, morphism x x;
+      compose : forall s d d',
+                  morphism d d'
+                  -> morphism s d
+                  -> morphism s d'
+                              where "f 'o' g" := (compose f g);
+
+      left_identity : forall a b (f : morphism a b), identity b o f = f
+    }.
+
+Hint Rewrite @left_identity. (* stack overflow *)
diff --git a/test-suite/bugs/closed/HoTT_coq_124.v b/test-suite/bugs/closed/HoTT_coq_124.v
new file mode 100644
index 000000000..e6e90ada8
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_124.v
@@ -0,0 +1,29 @@
+Set Implicit Arguments.
+Set Primitive Projections.
+
+Polymorphic Inductive eqp A (x : A) : A -> Type := eqp_refl : eqp x x.
+Monomorphic Inductive eqm A (x : A) : A -> Type := eqm_refl : eqm x x.
+
+Polymorphic Record prodp (A B : Type) : Type := pairp { fstp : A; sndp : B }.
+Monomorphic Record prodm (A B : Type) : Type := pairm { fstm : A; sndm : B }.
+
+Check eqm_refl _ : eqm (fun x : prodm Set Set => pairm (fstm x) (sndm x)) (fun x => x). (* success *)
+Check eqp_refl _ : eqp (fun x : prodm Set Set => pairm (fstm x) (sndm x)) (fun x => x). (* success *)
+Check eqm_refl _ : eqm (fun x : prodp Set Set => pairp (fstp x) (sndp x)) (fun x => x). (* Error:
+The term
+ "eqm_refl (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |})"
+has type
+ "eqm (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |})
+    (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |})"
+while it is expected to have type
+ "eqm (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |})
+    (fun x : prodp Set Set => x)". *)
+Check eqp_refl _ : eqp (fun x : prodp Set Set => pairp (fstp x) (sndp x)) (fun x => x). (* Error:
+The term
+ "eqp_refl (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |})"
+has type
+ "eqp (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |})
+    (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |})"
+while it is expected to have type
+ "eqp (fun x : prodp Set Set => {| fstp := fstp x; sndp := sndp x |})
+    (fun x : prodp Set Set => x)". *)