diff options
author | 2014-05-09 10:13:32 -0400 | |
---|---|---|
committer | 2014-05-10 15:39:39 +0200 | |
commit | c7284415e4bdd3315c84c7d15d140d3fee000bc5 (patch) | |
tree | cc8ded3feba7e1da0dd4f7d17b7e5f974de752c3 /test-suite/bugs/closed/HoTT_coq_030.v | |
parent | 3f64bd23a343bcd7be0ef07afa7d9e3249df24ec (diff) |
Move opened bugs to bugs/opened
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_030.v')
-rw-r--r-- | test-suite/bugs/closed/HoTT_coq_030.v | 240 |
1 files changed, 0 insertions, 240 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_030.v b/test-suite/bugs/closed/HoTT_coq_030.v deleted file mode 100644 index c9d8fe137..000000000 --- a/test-suite/bugs/closed/HoTT_coq_030.v +++ /dev/null @@ -1,240 +0,0 @@ -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. - Variable 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). *) |