Theorem: Slice Category is Isomorphic to Identity Functor Over Object 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 / C$ denote the slice category $\mathbf C$ over $C$.
Let $\paren {\operatorname{id}_{\mathbf C} \downarrow C}$ denote the comma category $\operatorname{id}_{\mathbf C}$ over $C$.
Then:
:$\mathbf C / C \cong \paren {\operatorname{id}_{\mathbf C} \downarrow C}$
with isomorphisms of categories:
:$I: \mathbf C / C \to \paren {\operatorname{id}_{\mathbf C} \downarrow C}$ 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 = k$
}}
::as per commutative diagrams:
::<nowiki>$\begin{xy}
<0em,8em>*+{\mathbf C / C} ="ID",
<21em,8em>*+{\paren {\operatorname{id}_{\mathbf C} \downarrow C} } ="IC",
<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",
<21em,0em>*+{C} = "C",
"GE";"GE2" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{\operatorname{id}_{\mathbf C} k = k},
"GE";"C" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{g},
"GE2";"C" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{g'},
\end{xy}$</nowiki>
and:
:$J: \paren {\operatorname{id}_{\mathbf C} \downarrow C} \to \mathbf C / C$ defined by:
{{DefineFunctor
|ob = for each object $\tuple {E, g}$ in $\paren {\operatorname{id}_{\mathbf C} \downarrow C}$:
:$J \tuple {E, g} = g$
|mor = for each morphism $k: \tuple {E, g} \to \tuple {E', g'}$ in $\paren {\operatorname{id}_{\mathbf C} \downarrow C}$:
:$J k = k$
}}
::<nowiki>$\begin{xy}
<3em,8em>*+{\paren {\operatorname{id}_{\mathbf C} \downarrow C} } ="GC",
<24em,8em>*+{\mathbf C / C} ="GF",
<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>*+{C} = "C",
"GE";"GE2" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{\operatorname{id}_{\mathbf C} k = k},
"GE";"C" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{g},
"GE2";"C" **@{-} ?>*@{>} ?<>(.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:
Let $F: \mathbf 1\to \mathbf C$ be the functor defined by:
:$F* = C$
and
:$F \operatorname{id}_* = \operatorname{id}_C$
From Slice Category is Isomorphic to Comma Category:
:$\mathbf C / C \cong \paren {\operatorname{id}_{\mathbf C} \downarrow F}$
with isomorphisms of categories:
:$I_1: \mathbf C / C \to \paren {\operatorname{id}_{\mathbf C} \downarrow F}$ defined by:
{{DefineFunctor
|ob = for each object $g$ in $\mathbf C / C$:
:$I_1 g = \tuple {\operatorname {dom} g,  *, g}$
|mor = for each morphism $k: g \to g'$ in $\mathbf C / C$:
:$I_1 k = \tuple {k, \operatorname{id}_*}$
}}
and:
:$J_1: \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_1 \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_1 \tuple {k, \operatorname{id}_*} = k$
}}
From Functor Over Object Comma Category is Isomorphic to Comma Category:
:$\paren {\operatorname{id}_{\mathbf C} \downarrow C} \cong \paren {\operatorname{id}_{\mathbf C} \downarrow F}$
with isomorphisms of categories:
:$I_2: \paren {\operatorname{id}_{\mathbf C} \downarrow C} \to \paren {\operatorname{id}_{\mathbf C} \downarrow F}$ defined by:
{{DefineFunctor
|ob = for each object $\tuple {E, g}$ in $\paren {C \downarrow F}$:
:$I_2 \tuple {E, g} = \tuple {E, *, g}$
|mor = for each morphism $k: \tuple {E, g} \to \tuple {E', g'}$ in $\paren{C \downarrow F}$:
:$I_2 k = \tuple {k, \operatorname{id}_*}$
}}
and:
:$J_2: \paren {\operatorname{id}_{\mathbf C} \downarrow F} \to \paren {\operatorname{id}_{\mathbf C} \downarrow C}$ defined by:
{{DefineFunctor
|ob = for each object $\tuple {E, *, g}$ in $\paren {\operatorname{id}_{\mathbf C} \downarrow F}$:
:$J_2 \tuple {E, *, g} = \tuple {E, 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_2 \tuple {k, \operatorname{id}_*} = k$
}}