diff options
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_064.v')
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_064.v | 190 |
1 files changed, 190 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_064.v b/test-suite/bugs/closed/HoTT_coq_064.v new file mode 100644 index 00000000..5f0a541b --- /dev/null +++ b/test-suite/bugs/closed/HoTT_coq_064.v @@ -0,0 +1,190 @@ +(* File reduced by coq-bug-finder from 279 lines to 219 lines. *) + +Set Implicit Arguments. +Set Universe Polymorphism. +Definition admit {T} : T. +Admitted. +Module Export Overture. + Reserved Notation "g 'o' f" (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. + + Delimit Scope path_scope with path. + + Local Open Scope path_scope. + + Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y + := match p with idpath => idpath end. + + Definition apD10 {A} {B:A->Type} {f g : forall x, B x} (h:f=g) + : forall x, f x = g x + := fun x => match h with idpath => idpath end. + + Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv { equiv_inv : B -> A }. + + Delimit Scope equiv_scope with equiv. + Local Open Scope equiv_scope. + + Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3) : equiv_scope. + + Class Funext. + Axiom isequiv_apD10 : `{Funext} -> forall (A : Type) (P : A -> Type) f g, IsEquiv (@apD10 A P f g) . + Existing Instance isequiv_apD10. + + Definition path_forall `{Funext} {A : Type} {P : A -> Type} (f g : forall x : A, P x) : + (forall x, f x = g x) -> f = g + := + (@apD10 A P f g)^-1. + +End Overture. + +Module Export Core. + + Set Implicit Arguments. + Delimit Scope morphism_scope with morphism. + Delimit Scope category_scope with category. + Delimit Scope object_scope with object. + + 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); + + associativity : forall x1 x2 x3 x4 + (m1 : morphism x1 x2) + (m2 : morphism x2 x3) + (m3 : morphism x3 x4), + (m3 o m2) o m1 = m3 o (m2 o m1) + }. + 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. + +End Core. + +Local Open Scope morphism_scope. +Record Functor (C D : PreCategory) := + { + object_of :> C -> D; + morphism_of : forall s d, morphism C s d + -> morphism D (object_of s) (object_of d) + }. + +Inductive Unit : Set := + tt : Unit. + +Definition indiscrete_category (X : Type) : PreCategory + := @Build_PreCategory X + (fun _ _ => Unit) + (fun _ _ _ _ _ => tt) + (fun _ _ _ _ _ _ _ => idpath). + + +Record NaturalTransformation C D (F G : Functor C D) := { components_of :> forall c, morphism D (F c) (G c) }. +Section path_natural_transformation. + Context `{Funext}. + Variable C : PreCategory. + Variable D : PreCategory. + Variables F G : Functor C D. + + Section path. + Variables T U : NaturalTransformation F G. + Lemma path'_natural_transformation + : components_of T = components_of U + -> T = U. + admit. + Defined. + Lemma path_natural_transformation + : (forall x, T x = U x) + -> T = U. + Proof. + intros. + apply path'_natural_transformation. + apply path_forall; assumption. + Qed. + End path. +End path_natural_transformation. +Ltac path_natural_transformation := + repeat match goal with + | _ => intro + | _ => apply path_natural_transformation; simpl + end. +Definition comma_category A B C (S : Functor A C) (T : Functor B C) +: PreCategory. + admit. +Defined. +Definition compose C D (F F' F'' : Functor C D) + (T' : NaturalTransformation F' F'') (T : NaturalTransformation F F') +: NaturalTransformation F F'' + := Build_NaturalTransformation F F'' + (fun c => T' c o T c). + +Infix "o" := compose : natural_transformation_scope. + +Local Open Scope natural_transformation_scope. + +Definition associativity `{fs : Funext} + C D F G H I + (V : @NaturalTransformation C D F G) + (U : @NaturalTransformation C D G H) + (T : @NaturalTransformation C D H I) +: (T o U) o V = T o (U o V). +Proof. + path_natural_transformation. + + apply associativity. +Qed. +Definition functor_category `{Funext} (C D : PreCategory) : PreCategory + := @Build_PreCategory (Functor C D) + (@NaturalTransformation C D) + (@compose C D) + (@associativity _ C D). + +Notation "C -> D" := (functor_category C D) : category_scope. + +Definition compose_functor `{Funext} (C D E : PreCategory) : object ((C -> D) -> ((D -> E) -> (C -> E))). + admit. + +Defined. + +Definition pullback_along `{Funext} (C C' D : PreCategory) (p : Functor C C') +: object ((C' -> D) -> (C -> D)) + := Eval hnf in compose_functor _ _ _ p. + +Definition IsColimit `{Funext} C D (F : Functor D C) + (x : object + (@comma_category (indiscrete_category Unit) + (@functor_category H (indiscrete_category Unit) C) + (@functor_category H D C) + admit + (@pullback_along H D (indiscrete_category Unit) C + admit))) : Type + := admit. + +Generalizable All Variables. +Axiom fs : Funext. + +Section bar. + + Variable D : PreCategory. + + Context `(has_colimits + : forall F : Functor D C, + @IsColimit _ C D F (colimits F)). +(* Error: Unsatisfied constraints: Top.3773 <= Set + (maybe a bugged tactic). *) +End bar. |