From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Sun, 25 Jan 2015 14:42:51 +0100
Subject: Imported Upstream version 8.5~beta1+dfsg

---
 test-suite/bugs/closed/HoTT_coq_061.v | 132 ++++++++++++++++++++++++++++++++++
 1 file changed, 132 insertions(+)
 create mode 100644 test-suite/bugs/closed/HoTT_coq_061.v

(limited to 'test-suite/bugs/closed/HoTT_coq_061.v')

diff --git a/test-suite/bugs/closed/HoTT_coq_061.v b/test-suite/bugs/closed/HoTT_coq_061.v
new file mode 100644
index 00000000..26c1f963
--- /dev/null
+++ b/test-suite/bugs/closed/HoTT_coq_061.v
@@ -0,0 +1,132 @@
+(* There are some problems in materialize_evar with local definitions,
+   as CO below; this is not completely sorted out yet, but at least
+   it fails in a smooth way at the time of today [HH] *)
+
+(* File reduced by coq-bug-finder from 9039 lines to 7786 lines, then
+   from 7245 lines to 476 lines, then from 417 lines to 249 lines,
+   then from 171 lines to 127 lines. *)
+
+Set Implicit Arguments.
+Set Universe Polymorphism.
+Definition admit {T} : T.
+Admitted.
+Delimit Scope object_scope with object.
+Delimit Scope morphism_scope with morphism.
+Delimit Scope category_scope with category.
+Delimit Scope functor_scope with functor.
+Delimit Scope natural_transformation_scope with natural_transformation.
+Reserved Infix "o" (at level 40, left associativity).
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+
+Arguments idpath {A a} , [A] a.
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+Definition inverse {A : Type} {x y : A} (p : x = y) : y = x
+  := match p with idpath => idpath end.
+
+Record PreCategory :=
+  {
+    Object :> Type;
+    Morphism : Object -> Object -> Type;
+
+    Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d' where "f 'o' g" := (Compose f g)
+  }.
+Bind Scope category_scope with PreCategory.
+
+Arguments Compose [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename.
+
+Infix "o" := Compose : morphism_scope.
+Local Open Scope morphism_scope.
+
+Record Functor (C D : PreCategory) :=
+  {
+    ObjectOf :> C -> D;
+    MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d);
+    FCompositionOf : forall s d d' (m1 : C.(Morphism) s d) (m2: C.(Morphism) d d'),
+                       MorphismOf _ _ (m2 o m1) = (MorphismOf _ _ m2) o (MorphismOf _ _ m1)
+  }.
+
+Bind Scope functor_scope with Functor.
+
+Arguments MorphismOf [C%category] [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch.
+
+Definition ComposeFunctors C D E
+           (G : Functor D E) (F : Functor C D) : Functor C E
+  := Build_Functor C E
+                   (fun c => G (F c))
+                   admit
+                   admit.
+
+Infix "o" := ComposeFunctors : functor_scope.
+
+Record NaturalTransformation C D (F G : Functor C D) :=
+  {
+    ComponentsOf :> forall c, D.(Morphism) (F c) (G c);
+    Commutes : forall s d (m : C.(Morphism) s d),
+                 ComponentsOf d o F.(MorphismOf) m = G.(MorphismOf) m o ComponentsOf s
+  }.
+
+Generalizable All Variables.
+
+Section NTComposeT.
+
+  Variable C : PreCategory.
+  Variable D : PreCategory.
+
+  Variables F F' F'' : Functor C D.
+
+  Variable T' : NaturalTransformation F' F''.
+  Variable T : NaturalTransformation F F'.
+  Let CO := fun c => T' c o T c.
+  Definition NTComposeT_Commutes s d (m : Morphism C s d)
+  : CO d o MorphismOf F m = MorphismOf F'' m o CO s.
+
+    admit.
+  Defined.
+  Definition NTComposeT
+  : NaturalTransformation F F''
+    := Build_NaturalTransformation F F''
+                                   (fun c => T' c o T c)
+                                   NTComposeT_Commutes.
+End NTComposeT.
+Definition NTWhiskerR C D E (F F' : Functor D E) (T : NaturalTransformation F F')
+           (G : Functor C D)
+  := Build_NaturalTransformation (F o G) (F' o G)
+                                 (fun c => T (G c))
+                                 admit.
+Global Class NTC_Composable A B (a : A) (b : B) (T : Type) (term : T) := {}.
+
+Definition NTC_Composable_term `{@NTC_Composable A B a b T term} := term.
+Notation "T 'o' U"
+  := (@NTC_Composable_term _ _ T%natural_transformation U%natural_transformation _ _ _)
+     : natural_transformation_scope.
+
+Local Open Scope natural_transformation_scope.
+
+Lemma NTWhiskerR_CompositionOf C D
+      (F G H : Functor C D)
+      (T : NaturalTransformation G H)
+      (T' : NaturalTransformation F G) B (I : Functor B C)
+: NTWhiskerR (NTComposeT T T') I = NTComposeT (NTWhiskerR T I) (NTWhiskerR T' I).
+
+  admit.
+Defined.
+Definition FunctorCategory C D : PreCategory
+  := @Build_PreCategory (Functor C D)
+                        (NaturalTransformation (C := C) (D := D))
+                        admit.
+
+Notation "[ C , D ]" := (FunctorCategory C D) : category_scope.
+
+Variable C : PreCategory.
+Variable D : PreCategory.
+Variable E : PreCategory.
+Fail Definition NTWhiskerR_Functorial (G : [C, D]%category)
+: [[D, E], [C, E]]%category
+  := Build_Functor
+       [C, D] [C, E]
+       (fun F => F o G)
+       (fun _ _ T => T o G)
+       (fun _ _ _ _ _ => inverse (NTWhiskerR_CompositionOf _ _ _)).
+(* Anomaly: Uncaught exception Not_found(_). Please report. *)
-- 
cgit v1.2.3