Freely adjoining R-cocartesian morphisms

Construction 17.2.2 (Freely adjoining \(\Rr \)-cocartesian morphisms). Using the notation \(\Ar _{\Rr }(S)\) from Lemma 17.1.9, for any \(p\colon E\to S\) we define \[ E_{\Rr }(p) \quad :=\quad E\times _{S,s}\Ar _{\Rr }(S)\xrightarrow {\;t\circ \pr _2\;}S. \] This construction defines an endofunctor \(E_{\Rr }\colon (\Cat _\infty )_{/S}\to (\Cat _\infty )_{/S}\).