1 files changed, 241 insertions, 0 deletions
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 00000000..fa5ee25c
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_030.v
@@ -0,0 +1,241 @@
+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.
+  Context (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). *)
+End FullyFaithful.