Identity functor into the category of isomorphisms

Construction 1.4.24. The identity morphisms define a canonical functor \[ i\colon C \to \Iso (C). \] Indeed, restriction along \(p_{[1]}\colon [1] \to [0]\) gives a functor \[ p_{[1]}^*\colon C \to \Ar (C), \qquad x \mapsto \id _x, \] whose composites with the source and target functors \(s,t\colon \Ar (C) \to C\) are both isomorphic to \(\id _C\). The triple \((p_{[1]}^*,p_{[1]}^*,p_{[1]}^*)\) therefore lifts to a functor \[ C \to \Ar (C) \times _{t,C,s} \Ar (C) \times _{t,C,s} \Ar (C), \qquad x \mapsto (\id _x,\id _x,\id _x). \] By Lemma 1.4.8 there is a natural isomorphism \(\id _x \circ \id _x \cong \id _x\), so the composite of this functor with \((g,f,h) \mapsto (f \circ g, h \circ f)\) is naturally isomorphic to the composite of the diagonal \(\Delta \colon C \to C \times C\) with \((x,y) \mapsto (\id _y, \id _x)\). The universal property of the pullback defining \(\Iso (C)\) thus provides the desired functor \(i\), and it satisfies \(\pi _{\Iso } \circ i \cong p_{[1]}^*\).