Category of isomorphisms

Definition 1.4.21. Given an \(\infty \)-category \(C\), we define the \(\infty \)-category \(\Iso (C)\) via the following pullback diagram:

We define \(\pi _{\Iso }\colon \Iso (C) \to \Ar (C)\) to be the composite functor \[ \Iso (C) \to \Ar (C) \times _{t,C,s} \Ar (C) \times _{t,C,s} \Ar (C) \xrightarrow {\pr _2} \Ar (C). \] An object of \(\Iso (C)\) is a triple of morphisms \((g\colon y' \to x, f\colon x \to y, h\colon y \to x')\) together with isomorphisms \(f \circ g \cong \id _y\) and \(h \circ f \cong \id _x\). Its image under \(\pi _{\Iso }\) is the morphism \(f\).