Require Import TestSuite.admit.
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.
¤ Dauer der Verarbeitung: 0.17 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|