avewright/proofwiki-math huggingface dataset:
Theorem: Correlation need not imply Causation

Let $X$ and $Y$ be random variables which show correlation between them.
Then it is not necessarily the case that they linked by cause and effect.

Proof:
Take the example of car ownership and alcohol sales.
{{:Correlation/Examples/Car Ownership and Alcohol Sales}}{{qed}}
Theorem: Hom Bifunctor With Left Functor is Covariant Functor

Let $\mathbf {Set}$ be the category of sets.
Let $\mathbf C$ and $\mathbf D$ be locally small categories.
Let $L : \mathbf D \to \mathbf C$ be a covariant functor.
Let $\map {\operatorname{Hom}_{\mathbf C} } {L-, -} : \mathbf D^{\text{op} } \times \mathbf C \to \mathbf {Set}$ denote the hom bifunctor with left functor.
Then:
:$\map {\operatorname{Hom}_{\mathbf C} } {L-, -}$ is a covariant functor.

Proof:
=== Object Functor is Well-defined ===
By definition of functor:
:for each object $D$ in $\mathbf D$: 
::$LD$ is an object in $\mathbf C$
By definition of dual category:
:for each object $D^\text{op}$ in $\mathbf D^\text{op}$: 
::$LD$ is an object in $\mathbf C$
By definition of locally small category:
:for each object $D^\text{op}$ in $\mathbf D^\text{op}$ and each object $C$ in $\mathbf C$: 
::$\map {\operatorname{Hom}_{\mathbf C} } {LD, C}$ is a set
That is:
:for each object $D^\text{op}$ in $\mathbf D^\text{op}$ and each object $C$ in $\mathbf C$: 
::$\map {\operatorname{Hom}_{\mathbf C} } {LD, C}$ is an object of $\mathbf {Set}$
By definition of hom bifunctor with left functor:
:for each object $D^\text{op}$ in $\mathbf D^\text{op}$ and each object $C$ in $\mathbf C$: 
::$\map {\operatorname{Hom}_{\mathbf C} } {LD^{\text{op} }, C} = \map {\operatorname{Hom}_{\mathbf C} } {LD, C}$
It follows that $\map {\operatorname{Hom}_{\mathbf C} } {L-, -}$ is a well-defined object functor from $\mathbf D^{\text{op} } \times \mathbf C$ to $\mathbf {Set}$.
{{qed|lemma}}
Theorem: Hom Bifunctor With Right Functor is Covariant Functor

Let $\mathbf {Set}$ be the category of sets.
Let $\mathbf C$ and $\mathbf D$ be locally small categories.
Let $R : \mathbf C \to \mathbf D$ be a covariant functor.
Let $\map {\operatorname{Hom}_{\mathbf D} } {-, R-} : \mathbf D^{\text{op} } \times \mathbf C \to \mathbf {Set}$ denote the hom bifunctor with right functor.
Then:
:$\map {\operatorname{Hom}_{\mathbf D} } {-, R-}$ is a covariant functor.

Proof:
=== Object Functor is Well-defined ===
By definition of functor:
:for each object $C$ in $\mathbf C$: 
::$RC$ is an object in $\mathbf D$
By definition of locally small category:
:for each object $\tuple{D^\text{op}, C}$ in $\mathbf D^\text{op} \times \mathbf C$: 
::$\map {\operatorname{Hom}_{\mathbf D} } {D, RC}$ is a set
That is:
:for each object $\tuple{D^\text{op}, C}$ in $\mathbf D^\text{op} \times \mathbf C$: 
::$\map {\operatorname{Hom}_{\mathbf D} } {D, RC}$ is an object of $\mathbf {Set}$
By definition of hom bifunctor with right functor:
:for each object $\tuple{D^\text{op}, C}$ in $\mathbf D^\text{op} \times \mathbf C$: 
::$\map {\operatorname{Hom}_{\mathbf D} } {D^{\text{op} }, RC} = \map {\operatorname{Hom}_{\mathbf D} } {D, RC}$
It follows that $\map {\operatorname{Hom}_{\mathbf D} } {-, R-}$ is a well-defined object functor from $\mathbf D^{\text{op} } \times \mathbf C$ to $\mathbf {Set}$.
{{qed|lemma}}
Theorem: Hom Bifunctor With Left Identity Functor is Hom Bifunctor

Let $\mathbf {Set}$ be the category of sets.
Let $\mathbf C$ be a locally small category.
Let $\operatorname{id}_{\mathbf C} : \mathbf C \to \mathbf C$ denote the identity functor.
Let $\map {\operatorname{Hom}_{\mathbf C} } {\operatorname{id}_{\mathbf C}-, -} : \mathbf C^{\text{op} } \times \mathbf C \to \mathbf {Set}$ denote the hom bifunctor with left functor $\operatorname{id}_{\mathbf C}$.
Let $\map {\operatorname{Hom}_{\mathbf C} } {-, -} : \mathbf C^{\text{op} } \times \mathbf C \to \mathbf {Set}$ denote the hom bifunctor.
Then:
:$\map {\operatorname{Hom}_{\mathbf C} } {\operatorname{id}_{\mathbf C} -, -} = \map {\operatorname{Hom}_{\mathbf C} } {-, -}$

Proof:
For each object $\tuple {D^\text{op}, C}$ in $\mathbf C^{\text{op} } \times \mathbf C$ we have:
{{begin-eqn}}
{{eqn | l = \map {\operatorname{Hom}_{\mathbf C} } {\operatorname{id}_{\mathbf C} D^\text{op}, C}
      | r = \map {\operatorname{Hom}_{\mathbf C} } {\operatorname{id}_{\mathbf C} D, C}
      | c = {{Defof|Hom Bifunctor With Left Functor}} 
}}
{{eqn | r = \map {\operatorname{Hom}_{\mathbf C} } {D, C}
      | c = {{Defof|Identity Functor}} 
}}
{{eqn | r = \map {\operatorname{Hom}_{\mathbf C} } {D^\text{op}, C}
      | c = {{Defof|Hom Bifunctor}} 
}}
{{end-eqn}}
For each morphism $\tuple {f^\text{op} : D_1^\text{op} \to D_2^\text{op}, g: C_1 \to C_2}$ in $\mathbf C^{\text{op} } \times \mathbf C$ we have:
{{begin-eqn}}
{{eqn | l = \map {\operatorname{Hom}_{\mathbf C} } {\operatorname{id}_{\mathbf C} f^\text{op}, g}
      | r = \forall h \in \map {\operatorname{Hom}_{\mathbf C} } {\operatorname{id}_{\mathbf C} D, C}: h \mapsto g \circ h \circ \operatorname{id}_{\mathbf C} f
      | c = {{Defof|Hom Bifunctor With Left Functor}} 
}}
{{eqn | r = \forall h \in \map {\operatorname{Hom}_{\mathbf C} } {D, C}: h \mapsto g \circ h \circ f
      | c = {{Defof|Identity Functor}} 
}}
{{eqn | r = \map {\operatorname{Hom}_{\mathbf C} } {f^\text{op}, g}
      | c = {{Defof|Hom Bifunctor}} 
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Hom Bifunctor With Right Identity Functor is Hom Bifunctor

Let $\mathbf {Set}$ be the category of sets.
Let $\mathbf C$ be a locally small category.
Let $\operatorname{id}_{\mathbf C} : \mathbf C \to \mathbf C$ denote the identity functor.
Let $\map {\operatorname{Hom}_{\mathbf C} } {-, \operatorname{id}_{\mathbf C}-} : \mathbf C^{\text{op} } \times \mathbf C \to \mathbf {Set}$ denote the hom bifunctor with right functor $\operatorname{id}_{\mathbf C}$.
Let $\map {\operatorname{Hom}_{\mathbf C} } {-, -} : \mathbf C^{\text{op} } \times \mathbf C \to \mathbf {Set}$ denote the hom bifunctor.
Then:
:$\map {\operatorname{Hom}_{\mathbf C} } {-, \operatorname{id}_{\mathbf C}-} = \map {\operatorname{Hom}_{\mathbf C} } {-, -}$

Proof:
For each object $\tuple {D^\text{op}, C}$ in $\mathbf C^{\text{op} } \times \mathbf C$ we have:
{{begin-eqn}}
{{eqn | l = \map {\operatorname{Hom}_{\mathbf C} } {D^\text{op}, \operatorname{id}_{\mathbf C} C}
      | r = \map {\operatorname{Hom}_{\mathbf C} } {D, \operatorname{id}_{\mathbf C} C}
      | c = {{Defof|Hom Bifunctor With Right Functor}} 
}}
{{eqn | r = \map {\operatorname{Hom}_{\mathbf C} } {D, C}
      | c = {{Defof|Identity Functor}} 
}}
{{eqn | r = \map {\operatorname{Hom}_{\mathbf C} } {D^\text{op}, C}
      | c = {{Defof|Hom Bifunctor}}
}}
{{end-eqn}}
For each morphism $\tuple {f^\text{op} : D_1^\text{op} \to D_2^\text{op}, g: C_1 \to C_2}$ in $\mathbf C^{\text{op} } \times \mathbf C$ we have:
{{begin-eqn}}
{{eqn | l = \map {\operatorname{Hom}_{\mathbf C} } {f^\text{op}, \operatorname{id}_{\mathbf C} g}
      | r = \forall h \in \map {\operatorname{Hom}_{\mathbf C} } {D_1, \operatorname{id}_{\mathbf C} C_1}: h \mapsto \operatorname{id}_{\mathbf C} g \circ h \circ f
      | c = {{Defof|Hom Bifunctor With Right Functor}} 
}}
{{eqn | r = \forall h \in \map {\operatorname{Hom}_{\mathbf C} } {D_1, C_1}: h \mapsto g \circ h \circ f
      | c = {{Defof|Identity Functor}} 
}}
{{eqn | r = \map {\operatorname{Hom}_{\mathbf C} } {f^\text{op}, g}
      | c = {{Defof|Hom Bifunctor}} 
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Curve with Constant Zero Curvature is Straight Line

Let $\CC$ be a curve whose curvature is constant and zero.
Then $\CC$ is a straight line.

Proof:
From Straight Line has Zero Curvature, if $\CC$ is a straight line then its curvature is indeed constant and zero.
It remains to be demonstrated that every such curve with constant zero curvature is a straight line.
{{ProofWanted}}
Theorem: Open Real Interval is not Homeomorphic to Half-Open Real Interval

Let $I_o$ denote the open real interval $\openint 0 1$.
Let $I_h$ denote the half-open real interval $\hointl 0 1$.
Then $I_o$ and $I_h$ are not homeomorphic.

Proof:
From Every Point except Endpoint in Connected Linearly Ordered Space is Cut Point:
:every point of $I_o$ is a cut point
:not every point of $I_h$ is a cut point.
Indeed, the point $1$ is not a cut point of $I_h$, as:
:$I_h \setminus \set 1 = I_o$
which is a connected space.
{{qed}}
Theorem: Comma Category is Category

Let $\mathbf C$, $\mathbf D$ and $\mathbf E$ be categories.
Let $F : \mathbf D \to \mathbf C$ and $G : \mathbf E \to \mathbf C$ be covariant functors.
Let $\paren{G \downarrow F}$ denote the comma category $G$ over $F$.
Then:
:$\paren{G \downarrow F}$ is a metacategory.

Proof:
Let us verify the axioms $(\text C 1)$ up to $(\text C 3)$ for a metacategory.
Theorem: Functor Under Object Comma Category is Category

Let $\mathbf C$, $\mathbf D$ be categories.
Let $C$ be an object of $\mathbf C$.
Let $F : \mathbf D \to \mathbf C$ be a covariant functor.
Let $\paren{C \downarrow F}$ denote the comma category $F$ under $C$.
Then:
:$\paren{C \downarrow F}$ is a metacategory.

Proof:
Let us verify the axioms $(\text C 1)$ up to $(\text C 3)$ for a metacategory.
Theorem: Functor Over Object Comma Category is Category

Let $\mathbf C$, $\mathbf E$ be categories.
Let $C$ be an object of $\mathbf C$.
Let $G : \mathbf E \to \mathbf C$ be a covariant functor.
Let $\paren{G \downarrow C}$ denote the comma category $G$ over $C$.
Then:
:$\paren{G \downarrow C}$ is a metacategory

Proof:
Let us verify the axioms $(\text C 1)$ up to $(\text C 3)$ for a metacategory.
Theorem: Functor Under Object Comma Category is Isomorphic to Comma Category

Let $\mathbf C$, $\mathbf D$ be categories.
Let $C$ be an object of $\mathbf C$.
Let $F : \mathbf D \to \mathbf C$ be a covariant functor.
Let $\mathbf 1$ denote the category one.
Let $G: \mathbf 1\to \mathbf C$ be the functor defined by:
{{DefineFunctor
|ob = $G* = C$
|mor = $G \operatorname{id}_* = \operatorname{id}_C$
}}
Let $\paren{C \downarrow F}$ denote the comma category $F$ under $C$.
Let $\paren{G \downarrow F}$ denote the comma category $G$ over $F$.
Then:
:$\paren{C \downarrow F} \cong \paren{G \downarrow F}$
with isomorphisms of categories:
:$I: \paren{C \downarrow F} \to \paren{G \downarrow F}$ defined by:
{{DefineFunctor
|ob = for each object $\tuple{D,f}$ in $\paren{C \downarrow F}$:
:$I\tuple{D, f} = \tuple{*, D, f}$
|mor = for each morphism $h : \tuple{D, f} \to \tuple{D', f'}$ in $\paren{C \downarrow F}$:
:$Ih = \tuple{\operatorname{id}_*, h}$
}}
::as per commutative diagrams:
::<nowiki>$\begin{xy}
<6em,2em> ="ID",
<11em,2em> ="IC",
"ID";"IC" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{I},
<-3em,0em>*+{F D} = "FD",
<3em,0em>*+{F D'} = "FD2",
<0em,4em>*+{C} = "C",
"FD";"FD2" **@{-} ?>*@{>}  ?*!/^1em/{F h},
"C";"FD" **@{-} ?>*@{>} ?*!/^.6em/{f},
"C";"FD2" **@{-} ?>*@{>} ?<>(.6)*!/_1em/{f'},
<15em,4em>*+{G* = C} = "GE",
<27em,4em>*+{G* = C} = "GE2",
<15em,0em>*+{F D} = "FD",
<27em,0em>*+{F D'} = "FD2",
"GE";"GE2" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{G \operatorname{id}_* = \operatorname{id}_C},
"FD";"FD2" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{F h},
"GE";"FD" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{f},
"GE2";"FD2" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{f'},
\end{xy}$</nowiki>
and:
:$J: \paren{G \downarrow F} \to \paren{C \downarrow F}$ defined by:
{{DefineFunctor
|ob = for each object $\tuple{*, D, f}$ in $\paren{G \downarrow F}$:
:$J\tuple{*, D, f} = \tuple{D, f}$
|mor = for each morphism $\tuple{\operatorname{id}_*, h:D \to D'} : \tuple{*, D, f} \to \tuple{*, D', f'}$ in $\paren{G \downarrow F}$:
:$J\tuple{\operatorname{id}_*, h} = h$
}}
::as per commutative diagrams:
::<nowiki>$\begin{xy}
<13em,2em> ="ID",
<18em,2em> ="IC",
"ID";"IC" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{J},
<-3em,4em>*+{G* = C} = "GE",
<9em,4em>*+{G* = C} = "GE2",
<-3em,0em>*+{F D} = "FD",
<9em,0em>*+{F D'} = "FD2",
"GE";"GE2" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{G \operatorname{id}_* = \operatorname{id}_C},
"FD";"FD2" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{F h},
"GE";"FD" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{f},
"GE2";"FD2" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{f'},
<21em,0em>*+{F D} = "FD",
<27em,0em>*+{F D'} = "FD2",
<24em,4em>*+{C} = "C",
"FD";"FD2" **@{-} ?>*@{>}  ?*!/^1em/{F h},
"C";"FD" **@{-} ?>*@{>} ?*!/^.6em/{f},
"C";"FD2" **@{-} ?>*@{>} ?<>(.6)*!/_1em/{f'},
\end{xy}$</nowiki>

Proof:
=== Lemma 1 ===
{{:Functor Under Object Comma Category is Isomorphic to Comma Category/Lemma 1}}{{qed|lemma}}
Theorem: Functor Over Object Comma Category is Isomorphic to Comma Category

Let $\mathbf C$, $\mathbf D$ be categories.
Let $C$ be an object of $\mathbf C$.
Let $G : \mathbf D \to \mathbf C$ be a covariant functor.
Let $\mathbf 1$ denote the category one.
Let $F: \mathbf 1\to \mathbf C$ be the functor defined by:
{{DefineFunctor
|ob = $F* = C$
|mor = $F \operatorname{id}_* = \operatorname{id}_C$
}}
Let $\paren{G \downarrow C}$ denote the comma category $G$ over $C$.
Let $\paren{G \downarrow F}$ denote the comma category $G$ over $F$.
Then:
:$\paren{G \downarrow C} \cong \paren{G \downarrow F}$
with isomorphisms of categories:
:$I: \paren{G \downarrow C} \to \paren{G \downarrow F}$ defined by:
{{DefineFunctor
|ob = for each object $\tuple{E, g}$ in $\paren{C \downarrow F}$:
:$I\tuple{E, g} = \tuple{E, *, g}$
|mor = for each morphism $h : \tuple{E, g} \to \tuple{E', g'}$ in $\paren{C \downarrow F}$:
:$Ih = \tuple{h, \operatorname{id}_*}$
}}
::as per commutative diagrams:
::<nowiki>$\begin{xy}
<6em,2em> ="ID",
<11em,2em> ="IC",
"ID";"IC" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{I},
<-3em,4em>*+{G E} = "GE",
<3em,4em>*+{G E'} = "GE2",
<0em,0em>*+{C} = "C",
"GE";"GE2" **@{-} ?>*@{>} ?*!/_1em/{G h},
"GE";"C" **@{-} ?>*@{>} ?<>(.3)*!/^1em/{g},
"GE2";"C" **@{-} ?>*@{>} ?<>(.3)*!/_1em/{g'},
<15em,4em>*+{G E} = "GE",
<27em,4em>*+{G E'} = "GE2",
<15em,0em>*+{F * = C} = "FD",
<27em,0em>*+{F * = C} = "FD2",
"GE";"GE2" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{G h},
"FD";"FD2" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{F \operatorname{id}_* = \operatorname{id}_C},
"GE";"FD" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{g},
"GE2";"FD2" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{g'},
\end{xy}$</nowiki>
and:
:$J: \paren{G \downarrow F} \to \paren{G \downarrow C}$ defined by:
{{DefineFunctor
|ob = for each object $\tuple{E, *, g}$ in $\paren{G \downarrow F}$:
:$J\tuple{E, *, g} = \tuple{E, g}$
|mor = for each morphism $\tuple{h:E \to E', \operatorname{id}_*} : \tuple{E, *, g} \to \tuple{E', *, g'}$ in $\paren{G \downarrow F}$:
:$J\tuple{h, \operatorname{id}_*} = h$
}}
::as per commutative diagrams:
::<nowiki>$\begin{xy}
<13em,2em> ="ID",
<18em,2em> ="IC",
"ID";"IC" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{J},
<-3em,4em>*+{G E} = "GE",
<9em,4em>*+{G E'} = "GE2",
<-3em,0em>*+{F * = C} = "FD",
<9em,0em>*+{F * = C} = "FD2",
"GE";"GE2" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{G h},
"FD";"FD2" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{F \operatorname{id}_* = \operatorname{id}_C},
"GE";"FD" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{g},
"GE2";"FD2" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{g'},
<21em,4em>*+{G E} = "GE",
<27em,4em>*+{G E'} = "GE2",
<24em,0em>*+{C} = "C",
"GE";"GE2" **@{-} ?>*@{>}  ?*!/_1em/{G h},
"GE";"C" **@{-} ?>*@{>} ?*!/^.6em/{g},
"GE2";"C" **@{-} ?>*@{>} ?<>(.6)*!/_1em/{g'},
\end{xy}$</nowiki>

Proof:
=== Lemma 1===
{{:Functor Over Object Comma Category is Isomorphic to Comma Category/Lemma 1}}{{qed|lemma}}
Theorem: Coslice Category is Isomorphic to Comma Category

Let $\mathbf C$ be a category.
Let $C$ be an object of $\mathbf C$.
Let $\operatorname{id}_{\mathbf C}$ denote the identity functor on $\mathbf C$.
Let $\mathbf 1$ denote the category one.
Let $G: \mathbf 1\to \mathbf C$ be the functor defined by:
:$G* = C$
and
:$G \operatorname{id}_* = \operatorname{id}_C$
Let $C / \mathbf C$ denote the coslice category $\mathbf C$ under $C$.
Let $\paren {G \downarrow \operatorname{id}_{\mathbf C}}$ denote the comma category $G$ over $\operatorname{id}_{\mathbf C}$.
Then:
:$C / \mathbf C \cong \paren {G \downarrow \operatorname{id}_{\mathbf C} }$
with isomorphisms of categories:
:$I: C / \mathbf C \to \paren {G \downarrow \operatorname{id}_{\mathbf C} }$ defined by:
{{DefineFunctor
|ob = for each object $f$ in $C / \mathbf C$:
:$I f = \tuple {*, \operatorname {cod} f, f}$
|mor = ::for each morphism $h : f \to f'$ in $C / \mathbf C$:
:$I h = \tuple {\operatorname{id}_*, h}$
}}
::<nowiki>$\begin{xy}
<6em,2em> ="ID",
<11em,2em> ="IC",
"ID";"IC" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{I},
<-3em,0em>*+{D} = "D",
<3em,0em>*+{D'} = "D2",
<0em,4em>*+{C} = "C",
"D";"D2" **@{-} ?>*@{>}  ?*!/^1em/{h},
"C";"D" **@{-} ?>*@{>} ?*!/^.6em/{f},
"C";"D2" **@{-} ?>*@{>} ?<>(.6)*!/_1em/{f'},
<15em,4em>*+{G* = C} = "GE",
<27em,4em>*+{G* = C} = "GE2",
<15em,0em>*+{\operatorname{id}_{\mathbf C} D = D} = "FD",
<27em,0em>*+{\operatorname{id}_{\mathbf C} D' = D'} = "FD2",
"GE";"GE2" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{G \operatorname{id}_* = \operatorname{id}_C},
"FD";"FD2" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{\operatorname{id}_{\mathbf C} h = h},
"GE";"FD" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{f},
"GE2";"FD2" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{f'},
\end{xy}$</nowiki>
and:
:$J: \paren {G \downarrow \operatorname{id}_{\mathbf C} } \to C / \mathbf C$ defined by:
{{DefineFunctor
|ob = for each object $\tuple {*, D, f}$ in $\paren {G \downarrow \operatorname{id}_{\mathbf C} }$:
:$J \tuple {*, D, f} = f$
|mor = for each morphism $\tuple {\operatorname{id}_*, h:D \to D'}: \tuple {*, D, f} \to \tuple {*, D', f'}$ in $\paren {G \downarrow \operatorname{id}_{\mathbf C} }$:
:$J \tuple {\operatorname{id}_*, h} = h$
}}
::<nowiki>$\begin{xy}
<13em,2em> ="ID",
<18em,2em> ="IC",
"ID";"IC" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{J},
<-3em,4em>*+{G* = C} = "GE",
<9em,4em>*+{G* = C} = "GE2",
<-3em,0em>*+{\operatorname{id}_{\mathbf C} D = D} = "FD",
<9em,0em>*+{\operatorname{id}_{\mathbf C} D' = D'} = "FD2",
"GE";"GE2" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{G \operatorname{id}_* = \operatorname{id}_C},
"FD";"FD2" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{\operatorname{id}_{\mathbf C} h = h},
"GE";"FD" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{f},
"GE2";"FD2" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{f'},
<21em,0em>*+{D} = "D",
<27em,0em>*+{D'} = "D2",
<24em,4em>*+{C} = "C",
"D";"D2" **@{-} ?>*@{>}  ?*!/^1em/{h},
"C";"D" **@{-} ?>*@{>} ?*!/^.6em/{f},
"C";"D2" **@{-} ?>*@{>} ?<>(.6)*!/_1em/{f'},
\end{xy}$</nowiki>

Proof:
=== Lemma 1 ===
{{:Coslice Category is Isomorphic to Comma Category/Lemma 1}}{{qed|lemma}}
Theorem: Slice Category is Isomorphic to Comma Category

Let $\mathbf C$ be a category.
Let $C$ be an object of $\mathbf C$.
Let $\operatorname{id}_{\mathbf C}$ denote the identity functor on $\mathbf C$.
Let $\mathbf 1$ denote the category one.
Let $F: \mathbf 1\to \mathbf C$ be the functor defined by:
:$F* = C$
and
:$F \operatorname{id}_* = \operatorname{id}_C$
Let $\mathbf C / C$ denote the slice category $\mathbf C$ over $C$.
Let $\paren {\operatorname{id}_{\mathbf C} \downarrow F}$ denote the comma category $\operatorname{id}_{\mathbf C}$ over $F$.
Then:
:$\mathbf C / C \cong \paren {\operatorname{id}_{\mathbf C} \downarrow F}$
with isomorphisms of categories:
:$I: \mathbf C / C \to \paren {\operatorname{id}_{\mathbf C} \downarrow F}$ defined by:
{{DefineFunctor
|ob = for each object $g$ in $\mathbf C / C$:
:$I g = \tuple {\operatorname {dom} g,  *, g}$
|mor = for each morphism $k : g \to g'$ in $\mathbf C / C$:
:$I k = \tuple {k, \operatorname{id}_*}$ 
}}
::as per commutative diagrams:
::<nowiki>$\begin{xy}
<6em,2em> ="ID",
<10em,2em> ="IC",
"ID";"IC" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{I},
<-3em,4em>*+{E} = "E",
<3em,4em>*+{E'} = "E2",
<0em,0em>*+{C} = "C",
"E";"E2" **@{-} ?>*@{>} ?*!/_1em/{k},
"E";"C" **@{-} ?>*@{>} ?<>(.3)*!/^1em/{g},
"E2";"C" **@{-} ?>*@{>} ?<>(.3)*!/_1em/{g'},
<15em,4em>*+{\operatorname{id}_{\mathbf C} E = E} = "GE",
<27em,4em>*+{\operatorname{id}_{\mathbf C} E' = E'} = "GE2",
<15em,0em>*+{F * = C} = "FD",
<27em,0em>*+{F * = C} = "FD2",
"GE";"GE2" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{\operatorname{id}_{\mathbf C} k = k},
"FD";"FD2" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{F \operatorname{id}_* = \operatorname{id}_C},
"GE";"FD" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{g},
"GE2";"FD2" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{g'},
\end{xy}$</nowiki>
and:
:$J: \paren {\operatorname{id}_{\mathbf C} \downarrow F} \to \mathbf C / C$ defined by:
{{DefineFunctor
|ob = for each object $\tuple {E, *, g}$ in $\paren {\operatorname{id}_{\mathbf C} \downarrow F}$:
:$J \tuple {E, *, g} = g$
|mor = for each morphism $\tuple {k: E \to E', \operatorname{id}_*} : \tuple{E, *, g} \to \tuple{E', *, g'}$ in $\paren {\operatorname{id}_{\mathbf C} \downarrow F}$:
:$J \tuple {k, \operatorname{id}_*} = k$
}}
::as per commutative diagrams:
::<nowiki>$\begin{xy}
<14em,2em> ="ID",
<18em,2em> ="IC",
"ID";"IC" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{J},
<-3em,4em>*+{\operatorname{id}_{\mathbf C} E = E} = "GE",
<9em,4em>*+{\operatorname{id}_{\mathbf C} E' = E'} = "GE2",
<-3em,0em>*+{F * = C} = "FD",
<9em,0em>*+{F * = C} = "FD2",
"GE";"GE2" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{\operatorname{id}_{\mathbf C} k = k},
"FD";"FD2" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{F \operatorname{id}_* = \operatorname{id}_C},
"GE";"FD" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{g},
"GE2";"FD2" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{g'},
<21em,4em>*+{E} = "E",
<27em,4em>*+{E'} = "E2",
<24em,0em>*+{C} = "C",
"E";"E2" **@{-} ?>*@{>}  ?*!/_1em/{k},
"E";"C" **@{-} ?>*@{>} ?*!/^.6em/{g},
"E2";"C" **@{-} ?>*@{>} ?<>(.6)*!/_1em/{g'},
\end{xy}$</nowiki>

Proof:
=== Lemma 1 ===
{{:Slice Category is Isomorphic to Comma Category/Lemma 1}}{{qed|lemma}}
Theorem: Equivalence of Definitions of Universal Morphism from Object to Functor

Let $\mathbf C$ and $\mathbf D$ be metacategories.
Let $C$ be an object of $\mathbf C$.
Let $F: \mathbf D \to \mathbf C$ be a covariant functor.
Let the pair $\tuple{R, u}$ consist of an object $R$ of $\mathbf D$ and a morphism $u: C \to FR$ in $C$.
{{TFAE|def=Universal Morphism from Object to Functor|context=Category Theory}}
=== Definition 1 ===
{{:Definition:Universal Morphism from Object to Functor/Definition 1}}
=== Definition 2 ===
{{:Definition:Universal Morphism from Object to Functor/Definition 2}}

Proof:
The result follows immediately from:
* Definition:Initial Object
* Definition:Functor Under Object Comma Category
{{qed}}