Theorem: Morphism 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 C^\to$ denote the morphism category on $\mathbf C$.
Let $\paren{\operatorname{id}_{\mathbf C} \downarrow \operatorname{id}_{\mathbf C}}$ denote the comma category $\operatorname{id}_{\mathbf C}$ over $\operatorname{id}_{\mathbf C}$.
Then:
:$\mathbf C^\to \cong \paren{\operatorname{id}_{\mathbf C} \downarrow \operatorname{id}_{\mathbf C} }$
with isomorphisms of categories:
:$I: \mathbf C^\to \to \paren{\operatorname{id}_{\mathbf C} \downarrow \operatorname{id}_{\mathbf C} }$ defined by:
{{DefineFunctor
|ob = for each object $f$ in $\mathbf C^\to$:
:$I f = \tuple{\operatorname {dom} f,  \operatorname {cod} f, f}$
|mor = for each morphism $\tuple{h_1, h_2}: f \to f'$ in $\mathbf C^\to$:
:$I \tuple {h_1, h_2} = \tuple {h_1, h_2}$ 
}}
::<nowiki>$\begin{xy}
<6em,2em> ="ID",
<11em,2em> ="IC",
"ID";"IC" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{I},
<-3em,0em>*+{D} = "D",
<3em,0em>*+{D'} = "D2",
<-3em,4em>*+{C} = "C",
<3em,4em>*+{C'} = "C2",
"C";"C2" **@{-} ?>*@{>}  ?*!/^1em/{g},
"D";"D2" **@{-} ?>*@{>}  ?*!/^1em/{h},
"C";"D" **@{-} ?>*@{>} ?*!/^.6em/{f},
"C2";"D2" **@{-} ?>*@{>} ?<>(.6)*!/_1em/{f'},
<15em,4em>*+{\operatorname{id}_{\mathbf C} C = C} = "C",
<27em,4em>*+{\operatorname{id}_{\mathbf C} C' = C'} = "C2",
<15em,0em>*+{\operatorname{id}_{\mathbf C} D = D} = "D",
<27em,0em>*+{\operatorname{id}_{\mathbf C} D' = D'} = "D2",
"C";"C2" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{\operatorname{id}_{\mathbf C} g = g},
"D";"D2" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{\operatorname{id}_{\mathbf C} h = h},
"C";"D" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{f},
"C2";"D2" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{f'},
\end{xy}$</nowiki>
and:
:$J: \paren{\operatorname{id}_{\mathbf C} \downarrow \operatorname{id}_{\mathbf C} } \to \mathbf C^\to$ defined by:
{{DefineFunctor
|ob = for each object $\tuple{E, D, f}$ in $\paren{\operatorname{id}_{\mathbf C} \downarrow \operatorname{id}_{\mathbf C } }$:
:$J \tuple {E, D, f} = f$
|mor = for each morphism $\tuple{h:E \to E', h_2:D \to D'}: \tuple{E, D, f} \to \tuple{E', D', f'}$ in $\paren {\operatorname{id}_{\mathbf C} \downarrow \operatorname{id}_{\mathbf C} }$:
:$J \tuple {h_1, h_2} = \tuple {h_1, h_2}$
}}
::<nowiki>$\begin{xy}
<13em,2em> ="ID",
<18em,2em> ="IC",
"ID";"IC" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{J},
<-3em,4em>*+{\operatorname{id}_{\mathbf C} C = C} = "C",
<9em,4em>*+{\operatorname{id}_{\mathbf C} C' = C'} = "C2",
<-3em,0em>*+{\operatorname{id}_{\mathbf C} D = D} = "D",
<9em,0em>*+{\operatorname{id}_{\mathbf C} D' = D'} = "D2",
"C";"C2" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{\operatorname{id}_{\mathbf C} g = g},
"D";"D2" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{\operatorname{id}_{\mathbf C} h = h},
"C";"D" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{f},
"C2";"D2" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{f'},
<21em,0em>*+{D} = "D",
<27em,0em>*+{D'} = "D2",
<21em,4em>*+{C} = "C",
<27em,4em>*+{C} = "C2",
"C";"C2" **@{-} ?>*@{>}  ?*!/_1em/{g},
"D";"D2" **@{-} ?>*@{>}  ?*!/^1em/{h},
"C";"D" **@{-} ?>*@{>} ?*!/^.6em/{f},
"C2";"D2" **@{-} ?>*@{>} ?<>(.6)*!/_1em/{f'},
\end{xy}$</nowiki>

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