diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /test-suite/bugs/closed/HoTT_coq_101.v | |
parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) |
Imported Upstream version 8.5~beta1+dfsg
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_101.v')
-rw-r--r-- | test-suite/bugs/closed/HoTT_coq_101.v | 77 |
1 files changed, 77 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_101.v b/test-suite/bugs/closed/HoTT_coq_101.v new file mode 100644 index 00000000..9c89a6ab --- /dev/null +++ b/test-suite/bugs/closed/HoTT_coq_101.v @@ -0,0 +1,77 @@ +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 YC. (* Toplevel input, characters 0-37: +Error: Universe inconsistency. Cannot enforce Top.187 = Top.186 because +Top.186 <= Top.189 < Top.191 <= Top.187). *) |