Update various polyproj bugs w.r.t. latest trunk

9 files changed, 762 insertions, 0 deletions

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 0000000000..f10856bc7e
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_036.v
@@ -0,0 +1,135 @@
+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.
+    let C1 := constr:(CObject) in
+    let C2 := constr:(fun C => @Object (CObject C) C) in
+    unify C1 C2.
+    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 0000000000..00588ffb0f
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_045.v
@@ -0,0 +1,53 @@
+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.
+  let C1 := constr:(CObject) in
+  let C2 := constr:(fun C => @Object (CObject C) C) in
+  unify C1 C2.
+  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_053.v b/test-suite/bugs/closed/HoTT_coq_053.v
new file mode 100644
index 0000000000..a14fb6aa57
--- /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 0000000000..f79fe1c1e7
--- /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_064.v b/test-suite/bugs/closed/HoTT_coq_064.v
new file mode 100644
index 0000000000..fe9773ecd5
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_064.v
@@ -0,0 +1,188 @@
+(* 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). *)
+End bar.
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 0000000000..fc15a88f7b
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_098.v
@@ -0,0 +1,88 @@
+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.
+  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)). *)
+  admit.
+  Defined.
+End failure.
+
+Module polycontext.
+  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.
+  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)). *)
+  admit.
+  Defined.
+End polycontext.
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 0000000000..71becfd2e5
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_102.v
@@ -0,0 +1,29 @@
+(* 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.
+  let C1 := constr:(CObject) in
+  let C2 := constr:(fun C => @Object (CObject C) C) in
+  let check := constr:(eq_refl : C1 = C2) in
+  unify C1 C2.
+  progress change CObject with (fun C => @Object (CObject C) C) in *.
+  (* not convertible *)
+  admit.
+Defined.
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 0000000000..c3a83627ee
--- /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_113.v b/test-suite/bugs/closed/HoTT_coq_113.v
new file mode 100644
index 0000000000..3ef531bc96
--- /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)). *)