Move opened bugs to bugs/opened

1 files changed, 0 insertions, 315 deletions

diff --git a/test-suite/bugs/closed/HoTT_coq_029.v b/test-suite/bugs/closed/HoTT_coq_029.v
deleted file mode 100644
index 85a2714c7..000000000
--- a/test-suite/bugs/closed/HoTT_coq_029.v
+++ /dev/null
@@ -1,315 +0,0 @@
-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 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 : Category _)
-      :=
-        existT _
-               ((CommaCategory S T : Category _) : Category', tt)
-               (CommaCategoryProjection) :
-          CommaCategory_ObjectT (IdentityFunctor _)
-                                (SliceCategory_Functor LocallySmallCat
-                                                       (ProductCategory A B : Category _)).
-    (* Anomaly: apply_coercion_args: mismatch between arguments and coercion. Please report. *)
-  End CommaCategoryProjectionFunctor.
-End SecondComment.