Bug closed, now in polymorphic mode, Variables A B : Type give different levels to A and B.

1 files changed, 0 insertions, 77 deletions

diff --git a/test-suite/bugs/opened/HoTT_coq_101.v b/test-suite/bugs/opened/HoTT_coq_101.v
deleted file mode 100644
index 9419c25c30..0000000000
--- a/test-suite/bugs/opened/HoTT_coq_101.v
+++ /dev/null
@@ -1,77 +0,0 @@
-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.
-  Fail 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). *)