diff options
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_030.v')
-rw-r--r-- | test-suite/bugs/closed/HoTT_coq_030.v | 241 |
1 files changed, 241 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_030.v b/test-suite/bugs/closed/HoTT_coq_030.v new file mode 100644 index 00000000..fa5ee25c --- /dev/null +++ b/test-suite/bugs/closed/HoTT_coq_030.v @@ -0,0 +1,241 @@ +Set Implicit Arguments. +Generalizable All Variables. +Set Asymmetric Patterns. +Set Universe Polymorphism. + +Delimit Scope object_scope with object. +Delimit Scope morphism_scope with morphism. +Delimit Scope category_scope with category. +Delimit Scope functor_scope with functor. + +Local Open Scope category_scope. + +Record SpecializedCategory (obj : Type) := + { + Object :> _ := obj; + Morphism : obj -> obj -> Type; + + Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d' + }. + +Bind Scope category_scope with SpecializedCategory. +Bind Scope object_scope with Object. +Bind Scope morphism_scope with Morphism. + +Arguments Object {obj%type} C%category / : rename. +Arguments Morphism {obj%type} !C%category s d : rename. (* , simpl nomatch. *) +Arguments Compose {obj%type} [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename. + +Record Category := { + CObject : Type; + + UnderlyingCategory :> @SpecializedCategory CObject +}. + +Definition GeneralizeCategory `(C : @SpecializedCategory obj) : Category. + refine {| CObject := C.(Object) |}; auto. (* Changing this [auto] to [assumption] removes the universe inconsistency. *) +Defined. + +Coercion GeneralizeCategory : SpecializedCategory >-> Category. + +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) + }. + +Section Functor. + Context (C D : Category). + + Definition Functor := SpecializedFunctor C D. +End Functor. + +Bind Scope functor_scope with SpecializedFunctor. +Bind Scope functor_scope with Functor. + +Arguments SpecializedFunctor {objC} C {objD} D. +Arguments Functor C D. +Arguments ObjectOf {objC%type C%category objD%type D%category} F%functor c%object : rename, simpl nomatch. +Arguments MorphismOf {objC%type} [C%category] {objD%type} [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch. + +Section FunctorComposition. + Context `(B : @SpecializedCategory objB). + Context `(C : @SpecializedCategory objC). + Context `(D : @SpecializedCategory objD). + Context `(E : @SpecializedCategory objE). + + Definition ComposeFunctors (G : SpecializedFunctor D E) (F : SpecializedFunctor C D) : SpecializedFunctor C E + := Build_SpecializedFunctor C E + (fun c => G (F c)) + (fun _ _ m => G.(MorphismOf) (F.(MorphismOf) m)). +End FunctorComposition. + +Record SpecializedNaturalTransformation + `{C : @SpecializedCategory objC} + `{D : @SpecializedCategory objD} + (F G : SpecializedFunctor C D) + := { + ComponentsOf :> forall c, D.(Morphism) (F c) (G c) + }. + +Definition ProductCategory + `(C : @SpecializedCategory objC) + `(D : @SpecializedCategory objD) +: @SpecializedCategory (objC * objD)%type + := @Build_SpecializedCategory _ + (fun s d => (C.(Morphism) (fst s) (fst d) * D.(Morphism) (snd s) (snd d))%type) + (fun s d d' m2 m1 => (Compose (fst m2) (fst m1), Compose (snd m2) (snd m1))). + +Infix "*" := ProductCategory : category_scope. + +Section ProductCategoryFunctors. + Context `{C : @SpecializedCategory objC}. + Context `{D : @SpecializedCategory objD}. + + Definition fst_Functor : SpecializedFunctor (C * D) C + := Build_SpecializedFunctor (C * D) C + (@fst _ _) + (fun _ _ => @fst _ _). + + Definition snd_Functor : SpecializedFunctor (C * D) D + := Build_SpecializedFunctor (C * D) D + (@snd _ _) + (fun _ _ => @snd _ _). +End ProductCategoryFunctors. + + +Definition OppositeCategory `(C : @SpecializedCategory objC) : @SpecializedCategory objC := + @Build_SpecializedCategory objC + (fun s d => Morphism C d s) + (fun _ _ _ m1 m2 => Compose m2 m1). + +Section OppositeFunctor. + Context `(C : @SpecializedCategory objC). + Context `(D : @SpecializedCategory objD). + Variable F : SpecializedFunctor C D. + Let COp := OppositeCategory C. + Let DOp := OppositeCategory D. + + Definition OppositeFunctor : SpecializedFunctor COp DOp + := Build_SpecializedFunctor COp DOp + (fun c : COp => F c : DOp) + (fun (s d : COp) (m : C.(Morphism) d s) => MorphismOf F (s := d) (d := s) m). +End OppositeFunctor. + +Section FunctorProduct. + Context `(C : @SpecializedCategory objC). + Context `(D : @SpecializedCategory objD). + Context `(D' : @SpecializedCategory objD'). + + Definition FunctorProduct (F : Functor C D) (F' : Functor C D') : SpecializedFunctor C (D * D'). + match goal with + | [ |- SpecializedFunctor ?C0 ?D0 ] => + refine (Build_SpecializedFunctor + C0 D0 + (fun c => (F c, F' c)) + (fun s d m => (MorphismOf F m, MorphismOf F' m))) + end. + Defined. +End FunctorProduct. + +Section FunctorProduct'. + Context `(C : @SpecializedCategory objC). + Context `(D : @SpecializedCategory objD). + Context `(C' : @SpecializedCategory objC'). + Context `(D' : @SpecializedCategory objD'). + Variable F : Functor C D. + Variable F' : Functor C' D'. + + Definition FunctorProduct' : SpecializedFunctor (C * C') (D * D') + := FunctorProduct (ComposeFunctors F fst_Functor) (ComposeFunctors F' snd_Functor). +End FunctorProduct'. + +(** XXX TODO(jgross): Change this to [FunctorProduct]. *) +Infix "*" := FunctorProduct' : functor_scope. + +Definition TypeCat : @SpecializedCategory Type := + (@Build_SpecializedCategory Type + (fun s d => s -> d) + (fun _ _ _ f g => (fun x => f (g x)))). + +Section HomFunctor. + Context `(C : @SpecializedCategory objC). + Let COp := OppositeCategory C. + + Definition CovariantHomFunctor (A : COp) : SpecializedFunctor C TypeCat + := Build_SpecializedFunctor C TypeCat + (fun X : C => C.(Morphism) A X : TypeCat) + (fun X Y f => (fun g : C.(Morphism) A X => Compose f g)). + + Definition hom_functor_object_of (c'c : COp * C) := C.(Morphism) (fst c'c) (snd c'c) : TypeCat. + + Definition hom_functor_morphism_of (s's : (COp * C)%type) (d'd : (COp * C)%type) (hf : (COp * C).(Morphism) s's d'd) : + TypeCat.(Morphism) (hom_functor_object_of s's) (hom_functor_object_of d'd). + unfold hom_functor_object_of in *. + destruct s's as [ s' s ], d'd as [ d' d ]. + destruct hf as [ h f ]. + intro g. + exact (Compose f (Compose g h)). + Defined. + + Definition HomFunctor : SpecializedFunctor (COp * C) TypeCat + := Build_SpecializedFunctor (COp * C) TypeCat + (fun c'c : COp * C => C.(Morphism) (fst c'c) (snd c'c) : TypeCat) + (fun X Y (hf : (COp * C).(Morphism) X Y) => hom_functor_morphism_of hf). +End HomFunctor. + +Section FullFaithful. + Context `(C : @SpecializedCategory objC). + Context `(D : @SpecializedCategory objD). + Variable F : SpecializedFunctor C D. + Let COp := OppositeCategory C. + Let DOp := OppositeCategory D. + Let FOp := OppositeFunctor F. + + Definition InducedHomNaturalTransformation : + SpecializedNaturalTransformation (HomFunctor C) (ComposeFunctors (HomFunctor D) (FOp * F)) + := (Build_SpecializedNaturalTransformation (HomFunctor C) (ComposeFunctors (HomFunctor D) (FOp * F)) + (fun sd : (COp * C) => + MorphismOf F (s := _) (d := _))). +End FullFaithful. + +Definition FunctorCategory + `(C : @SpecializedCategory objC) + `(D : @SpecializedCategory objD) +: @SpecializedCategory (SpecializedFunctor C D). + refine (@Build_SpecializedCategory _ + (SpecializedNaturalTransformation (C := C) (D := D)) + _); + admit. +Defined. + +Notation "C ^ D" := (FunctorCategory D C) : category_scope. + +Section Yoneda. + Context `(C : @SpecializedCategory objC). + Let COp := OppositeCategory C. + + Section Yoneda. + Let Yoneda_NT s d (f : COp.(Morphism) s d) : SpecializedNaturalTransformation (CovariantHomFunctor C s) (CovariantHomFunctor C d) + := Build_SpecializedNaturalTransformation + (CovariantHomFunctor C s) + (CovariantHomFunctor C d) + (fun c : C => (fun m : C.(Morphism) _ _ => Compose m f)). + + Definition Yoneda : SpecializedFunctor COp (TypeCat ^ C) + := Build_SpecializedFunctor COp (TypeCat ^ C) + (fun c : COp => CovariantHomFunctor C c : TypeCat ^ C) + (fun s d (f : Morphism COp s d) => Yoneda_NT s d f). + End Yoneda. +End Yoneda. + +Section FullyFaithful. + Context `(C : @SpecializedCategory objC). + + Set Printing Universes. + Check InducedHomNaturalTransformation (Yoneda C). + (* Error: Universe inconsistency (cannot enforce Top.865 = Top.851 because +Top.851 < Top.869 <= Top.864 <= Top.865). *) +End FullyFaithful. |