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

1 files changed, 77 insertions, 0 deletions

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 0000000000..9c89a6ab9d
--- /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). *)