Imported Upstream version 8.5~beta1+dfsg

1 files changed, 335 insertions, 0 deletions

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 00000000..4fd54b56
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_029.v
@@ -0,0 +1,335 @@
+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 prod (A B : Type) := pair { fst : A; snd : B }.
+  Arguments fst {A B} _.
+  Arguments snd {A B} _.
+  Infix "*" := prod : type_scope.
+  Notation " ( x , y ) " := (@pair _ _ x y).
+  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)
+      :=
+        existT _
+               ((CommaCategory S T) : Category', tt)
+               (CommaCategoryProjection) :
+          CommaCategory_ObjectT (IdentityFunctor _)
+                                (SliceCategory_Functor LocallySmallCat
+                                                       (ProductCategory A B)).
+    (* Anomaly: apply_coercion_args: mismatch between arguments and coercion. Please report. *)
+    (* Toplevel input, characters 110-142:
+Error:
+In environment
+objA : Type
+A : Category objA
+objB : Type
+B : Category objB
+objC : Type
+C : Category objC
+S : OppositeCategory (FunctorCategory A C)
+T : FunctorCategory B C
+The term "ProductCategory A B:Category (objA * objB)" has type
+ "Category (objA * objB)" while it is expected to have type
+ "Object LocallySmallCat".
+ *)
+  End CommaCategoryProjectionFunctor.
+End SecondComment.