Envelope fully faithful

Proof. Consider two \(\Ll \)-cocartesian fibrations \(p\colon E \to S\) and \(p'\colon E' \to S\). We must show that the induced diagram

is a pullback square, where the horizontal maps are given by applying \(E_{\Rr }\). By the universal property of \(E_{\Rr }(p)\), we may identify this square with the square

where now the horizontal maps are given by postcomposition with \(i_{p'}\colon E' \to E_{\Rr }(p')\) and \(i\colon S \to \Ar _{\Rr }(S)\). But this is a simple consequence of the fact that the left square in the diagram

is a pullback square by the pasting law, and that a functor into \(E'\) preserves \(\Ll \)-cocartesian morphisms if and only if its composite with \(i_{p'}\) does. □