refine (@Build_Category _
(fun s d => (C.(Morphism) (fst s) (fst d) * D.(Morphism) (snd s) (snd d))%type)
(fun o => (Identity (fst o), Identity (snd o)))
(fun s d d' m2 m1 => (Compose (fst m2) (fst m1), Compose (snd m2) (snd m1)))). Defined. End ProductCategory. Parameter TerminalCategory : Category unit.
Section ComputableCategory.
Variable I : Type. Variable Index2Object : I -> Type. Variable Index2Cat : forall i : I, @Category (@Index2Object i). Local Coercion Index2Cat : I >-> Category.
Definition ComputableCategory : @Category I.
refine (@Build_Category _
(fun C D : I => Functor C D)
(fun o : I => IdentityFunctor o)
(fun C D E : I => ComposeFunctors (C := C) (D := D) (E := E))). Defined. End ComputableCategory. Definition LocallySmallCat := ComputableCategory _ LSUnderlyingCategory. Section CommaCategory.
Context `(A : @Category objA).
Context `(B : @Category objB).
Context `(C : @Category objC). Variable S : Functor A C. Variable T : Functor B C.
Record CommaCategory_Object := { CommaCategory_Object_Member :> { ab : objA * objB & C.(Morphism) (S (fst ab)) (T (snd ab)) } }.
End CommaCategory. Definition SliceCategory_Functor `(C : @Category objC) (a : C) : Functor TerminalCategory C
:= {| ObjectOf := (fun _ => a);
MorphismOf := (fun _ _ _ => Identity a)
|}.
Definition SliceCategoryOver
: forall (objC : Type) (C : Category objC) (a : C),
Category
(CommaCategory_Object (IdentityFunctor C)
(SliceCategory_Functor C a)).
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.
