diff options
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_034.v')
-rw-r--r-- | test-suite/bugs/closed/HoTT_coq_034.v | 127 |
1 files changed, 127 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_034.v b/test-suite/bugs/closed/HoTT_coq_034.v new file mode 100644 index 000000000..9697928ff --- /dev/null +++ b/test-suite/bugs/closed/HoTT_coq_034.v @@ -0,0 +1,127 @@ +Module Short. + Set Universe Polymorphism. + Inductive relevant (A : Type) (B : Type) : Prop := . + Section foo. + Variables A B : Type. + Definition foo := prod (relevant A B) A. + End foo. + + Section bar. + Variable A : Type. + Variable B : Type. + Definition bar := prod (relevant A B) A. + End bar. + + Set Printing Universes. + Check bar nat Set : Set. (* success *) + Check foo nat Set : Set. (* Toplevel input, characters 6-17: +Error: +The term "foo (* Top.303 Top.304 *) nat Set" has type +"Type (* Top.304 *)" while it is expected to have type +"Set" (Universe inconsistency: Cannot enforce Top.304 = Set because Set +< Top.304)). *) +End Short. + +Section Long. + Set Universe Polymorphism. + Set Implicit Arguments. + Generalizable All Variables. + + Record SpecializedCategory (obj : Type) := + { + Object :> _ := obj; + Morphism : obj -> obj -> Type + }. + + + Record > Category := + { + CObject : Type; + + UnderlyingCategory :> @SpecializedCategory CObject + }. + + Record SpecializedFunctor `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) := + { + ObjectOf :> objC -> objD; + MorphismOf : forall s d, C.(Morphism) s d -> D.(Morphism) (ObjectOf s) (ObjectOf d) + }. + + (* Replacing this with [Definition Functor (C D : Category) := +SpecializedFunctor C D.] gets rid of the universe inconsistency. *) + Section Functor. + Variable C D : Category. + + Definition Functor := SpecializedFunctor C D. + End Functor. + + Record SpecializedNaturalTransformation `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) (F G : SpecializedFunctor C D) := + { + ComponentsOf :> forall c, D.(Morphism) (F c) (G c) + }. + + Definition FunctorProduct' `(F : Functor C D) : SpecializedFunctor C D. + admit. + Defined. + + Definition TypeCat : @SpecializedCategory Type. + admit. + Defined. + + + Definition CovariantHomFunctor `(C : @SpecializedCategory objC) : SpecializedFunctor C TypeCat. + refine (Build_SpecializedFunctor C TypeCat + (fun X : C => C.(Morphism) X X) + _ + ); admit. + Defined. + + Definition FunctorCategory `(C : @SpecializedCategory objC) `(D : @SpecializedCategory objD) : @SpecializedCategory (SpecializedFunctor C D). + refine (@Build_SpecializedCategory _ + (SpecializedNaturalTransformation (C := C) (D := D))). + Defined. + + Definition Yoneda `(C : @SpecializedCategory objC) : SpecializedFunctor C (FunctorCategory C TypeCat). + match goal with + | [ |- SpecializedFunctor ?C0 ?D0 ] => + refine (Build_SpecializedFunctor C0 D0 + (fun c => CovariantHomFunctor C) + _ + ) + end; + admit. + Defined. + + Section FullyFaithful. + Context `(C : @SpecializedCategory objC). + Let TypeCatC := FunctorCategory C TypeCat. + Let YC := (Yoneda C). + Set Printing Universes. + Check @FunctorProduct' C TypeCatC (Yoneda C). + (* Toplevel input, characters 35-43: +Error: +In environment +objC : Type (* Top.186 *) +C : SpecializedCategory (* Top.185 Top.186 *) objC +TypeCatC := FunctorCategory (* Top.187 Top.185 Top.189 Top.186 Top.191 + Top.192 *) C TypeCat (* Top.193 Top.192 Top.195 Top.191 *) + : SpecializedCategory (* Top.189 Top.187 *) + (SpecializedFunctor (* Top.192 Top.186 Top.191 Top.185 *) C + TypeCat (* Top.193 Top.192 Top.195 Top.191 *)) +YC := Yoneda (* Top.197 Top.198 Top.185 Top.186 Top.201 Top.202 Top.203 + Top.204 Top.185 Top.206 *) C + : SpecializedFunctor (* Top.202 Top.186 Top.203 Top.185 *) C + (FunctorCategory (* Top.203 Top.185 Top.202 Top.186 Top.197 Top.198 *) + C TypeCat (* Top.185 Top.198 Top.204 Top.197 *)) +The term + "Yoneda (* Top.225 Top.226 Top.227 Top.186 Top.229 Top.230 Top.231 Top.232 + Top.185 Top.234 *) C" has type + "SpecializedFunctor (* Top.230 Top.228 Top.231 Top.233 *) C + (FunctorCategory (* Top.231 Top.233 Top.230 Top.228 Top.225 Top.226 *) C + TypeCat (* Top.227 Top.226 Top.232 Top.225 *))" +while it is expected to have type + "Functor (* Top.216 Top.219 Top.217 Top.220 *) C TypeCatC" +(Universe inconsistency: Cannot enforce Top.230 = Top.217 because Top.217 +<= Top.227 < Top.225 <= Top.231 <= Top.230)). + *) +End Long. |