Lemma 1.4.8 (Unitality). For every morphism \(f\colon x \to y\) in an \(\infty \)-category \(C\), there are natural isomorphisms \[ \id _y \circ f \cong f \cong f \circ \id _x \] in \(\Ar (C)\). Moreover, these isomorphisms are natural in \(f\), in the sense that they form natural isomorphisms of functors \(\Ar (C) \to \Ar (C)\).
Proof. For a fixed morphism \(f\), the isomorphisms are an immediate consequence of Exercise 1.2.15, using the degenerate commutative triangles \(s_1^*(f) := f \circ s_1\) and \(s_0^*(f) := f \circ s_0\). For the naturality of the relation \(f \circ \id _x \cong f\) we have to show that the composite \[ \Ar (C) \iso \Ar (C) \times _{s,C,\id } C \xrightarrow {1 \times p_{[1]}^*} \Ar (C) \times _{s,C,t} \Ar (C) \xrightarrow {- \circ -} \Ar (C) \] is isomorphic to the identity functor. This follows from the following commutative diagram:
A similar discussion applies to the relation \(f \cong \id _y \circ f\). □
Generated from the authoritative LaTeX source.