From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- test-suite/bugs/closed/3686.v | 62 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 62 insertions(+) create mode 100644 test-suite/bugs/closed/3686.v (limited to 'test-suite/bugs/closed/3686.v') diff --git a/test-suite/bugs/closed/3686.v b/test-suite/bugs/closed/3686.v new file mode 100644 index 00000000..ee6b334b --- /dev/null +++ b/test-suite/bugs/closed/3686.v @@ -0,0 +1,62 @@ +Set Universe Polymorphism. +Set Implicit Arguments. +Record PreCategory := { object :> Type ; morphism : object -> object -> Type }. +Bind Scope category_scope with PreCategory. +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); + identity_of : forall s m, morphism_of s s m = morphism_of s s m }. +Definition sub_pre_cat (P : PreCategory -> Type) : PreCategory. +Proof. + exact (@Build_PreCategory PreCategory Functor). +Defined. +Definition opposite (C : PreCategory) : PreCategory. +Proof. + exact (@Build_PreCategory C (fun s d => morphism C d s)). +Defined. +Local Notation "C ^op" := (opposite C) (at level 3, format "C '^op'") : category_scope. +Definition prod (C D : PreCategory) : PreCategory. +Proof. + refine (@Build_PreCategory + (C * D)%type + (fun s d => (morphism C (fst s) (fst d) * morphism D (snd s) (snd d))%type)). +Defined. +Local Infix "*" := prod : category_scope. +Axiom functor_category : PreCategory -> PreCategory -> PreCategory. +Local Notation "C -> D" := (functor_category C D) : category_scope. +Module Export PointwiseCore. + Definition pointwise + (C C' : PreCategory) + (F : Functor C' C) + (D D' : PreCategory) + (G : Functor D D') + : Functor (C -> D) (C' -> D'). + Proof. + refine (Build_Functor + (C -> D) (C' -> D') + _ + _ + _); + abstract admit. + Defined. +End PointwiseCore. +Axiom Pidentity_of : forall (C D : PreCategory) (F : Functor C C) (G : Functor D D), pointwise F G = pointwise F G. +Local Open Scope category_scope. +Definition functor_uncurried (P : PreCategory -> Type) + (has_functor_categories : forall C D : @sub_pre_cat P, P (C -> D)) +: object (((@sub_pre_cat P)^op * (@sub_pre_cat P)) -> (@sub_pre_cat P)). +Proof. + pose (let object_of := (fun CD => (((fst CD) -> (snd CD)))) + in Build_Functor + ((@sub_pre_cat P)^op * (@sub_pre_cat P)) (@sub_pre_cat P) + object_of + (fun CD C'D' FG => pointwise (fst FG) (snd FG)) + (fun _ _ => Pidentity_of _ _)) || fail "early". + Include PointwiseCore. + pose (let object_of := (fun CD => (((fst CD) -> (snd CD)))) + in Build_Functor + ((@sub_pre_cat P)^op * (@sub_pre_cat P)) (@sub_pre_cat P) + object_of + (fun CD C'D' FG => pointwise (fst FG) (snd FG)) + (fun _ _ => Pidentity_of _ _)). +Abort. -- cgit v1.2.3