Theorem: Coslice Category is Isomorphic to Identity Functor Under 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 $C / \mathbf C$ denote the coslice category $\mathbf C$ under $C$.
Let $\paren {C \downarrow \operatorname{id}_{\mathbf C}}$ denote the comma category $\operatorname{id}_{\mathbf C}$ under $C$.
Then:
:$C / \mathbf C \cong \paren {C \downarrow \operatorname{id}_{\mathbf C} }$
with isomorphisms of categories:
:$I: C / \mathbf C \to \paren {C \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 = 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'},
<21em,4em>*+{C} = "C",
<15em,0em>*+{\operatorname{id}_{\mathbf C} D = D} = "FD",
<27em,0em>*+{\operatorname{id}_{\mathbf C} D' = D'} = "FD2",
"FD";"FD2" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{\operatorname{id}_{\mathbf C} h = h},
"C";"FD" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{f},
"C";"FD2" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{f'},
\end{xy}$</nowiki>
and:
:$J: \paren {C \downarrow \operatorname{id}_{\mathbf C} } \to C / \mathbf C$ defined by:
{{DefineFunctor
|ob = for each object $\tuple {D, f}$ in $\paren {C \downarrow \operatorname{id}_{\mathbf C} }$:
:$J \tuple {D, f} = f$
|mor = for each morphism $h: \tuple {D, f} \to \tuple {D', f'}$ in $\paren {C \downarrow \operatorname{id}_{\mathbf C} }$:
:$J h = h$
}}
::<nowiki>$\begin{xy}
<13em,2em> ="ID",
<18em,2em> ="IC",
"ID";"IC" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{J},
<3em,4em>*+{C} = "C",
<-3em,0em>*+{\operatorname{id}_{\mathbf C} D = D} = "FD",
<9em,0em>*+{\operatorname{id}_{\mathbf C} D' = D'} = "FD2",
"FD";"FD2" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{\operatorname{id}_{\mathbf C} h = h},
"C";"FD" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{f},
"C";"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:
Let $G: \mathbf 1\to \mathbf C$ be the functor defined by:
:$G* = C$
and:
:$G \operatorname{id}_* = \operatorname{id}_C$
From Coslice Category is Isomorphic to Comma Category:
:$C / \mathbf C \cong \paren {G \downarrow \operatorname{id}_{\mathbf C} }$
with isomorphisms of categories:
:$I_1: C / \mathbf C \to \paren {G \downarrow \operatorname{id}_{\mathbf C} }$ defined by:
{{DefineFunctor
|ob = for each object $f$ in $C / \mathbf C$:
:$I_1 f = \tuple {*, \operatorname {cod} f, f}$
|mor = for each morphism $h: f \to f'$ in $C / \mathbf C$:
:$I_1 h = \tuple {\operatorname{id}_*, h}$
}}
and:
:$J_1: \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_1 \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_1 \tuple {\operatorname{id}_*, h} = h$
}}
From Functor Under Object Comma Category is Isomorphic to Comma Category:
:$\paren {C \downarrow \operatorname{id}_{\mathbf C} } \cong \paren {G \downarrow \operatorname{id}_{\mathbf C} }$
with isomorphisms of categories:
:$I_2: \paren {C \downarrow \operatorname{id}_{\mathbf C} } \to \paren {G \downarrow \operatorname{id}_{\mathbf C} }$ defined by:
{{DefineFunctor
|ob = for each object $\tuple {D, f}$ in $\paren {C \downarrow \operatorname{id}_{\mathbf C} }$:
:$I_2 \tuple {D, f} = \tuple {*, D, f}$
|mor = for each morphism $h: \tuple {D, f} \to \tuple {D', f'}$ in $\paren {C \downarrow \operatorname{id}_{\mathbf C} }$:
:$I_2 h = \tuple {\operatorname{id}_*, h}$
}}
and:
:$J_2: \paren {G \downarrow \operatorname{id}_{\mathbf C} } \to \paren {C \downarrow \operatorname{id}_{\mathbf C} }$ defined by:
{{DefineFunctor
|ob = for each object $\tuple {*, D, f}$ in $\paren {G \downarrow \operatorname{id}_{\mathbf C} }$:
:$J_2 \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 \operatorname{id}_{\mathbf C} }$:
:$J_2 \tuple {\operatorname{id}_*, h} = h$
}}