From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- test-suite/bugs/closed/3685.v | 75 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 75 insertions(+) create mode 100644 test-suite/bugs/closed/3685.v (limited to 'test-suite/bugs/closed/3685.v') diff --git a/test-suite/bugs/closed/3685.v b/test-suite/bugs/closed/3685.v new file mode 100644 index 00000000..a5bea34a --- /dev/null +++ b/test-suite/bugs/closed/3685.v @@ -0,0 +1,75 @@ +Require Import TestSuite.admit. +Set Universe Polymorphism. +Class Funext := { }. +Delimit Scope category_scope with category. +Record PreCategory := { object :> Type ; morphism : object -> object -> Type }. +Set Implicit Arguments. +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 `{Funext} (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. +Record NaturalTransformation C D (F G : Functor C D) := {}. +Definition functor_category (C D : PreCategory) : PreCategory. +Proof. + exact (@Build_PreCategory (Functor C D) (@NaturalTransformation C D)). +Defined. +Local Notation "C -> D" := (functor_category C D) : category_scope. +Module Export PointwiseCore. + Local Open Scope category_scope. + 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. +Module Success. + Definition functor_uncurried `{Funext} (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)) + := Eval cbv zeta in + 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 _ _ _ _). +End Success. +Module Bad. + Include PointwiseCore. + Definition functor_uncurried `{Funext} (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)) + := Eval cbv zeta in + 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 _ _ _ _). -- cgit v1.2.3