Proof.Let be the coCartesian fibration associated with the functor (which is also Cartesian, since has a right adjoint).
We can assume that we have a commutative diagram
such that ,
and
is a coCartesian edge of for every
(combine T.5.2.1.1 and T.5.2.1.3). It is clear from T.1.2.9.2 that
for any pair of -categories with objects
and there is a canonical isomorphism
Hence, we get an induced commutative diagram
The functor is a Cartesian and coCartesian fibration by the
duals of T.2.4.3.1(1) and T.2.4.3.2(1). Moreover, an edge in
is (co)Cartesian if and only if its projection to is
(co)Cartesian by the duals of T.2.4.3.1(2) and T.2.4.3.2(2), which
shows that the functor is associated with . It follows
that has a right adjoint .
Assuming that is fully faithful, we will show that is
fully faithful by showing that the counit of the adjunction
is an equivalence. For every object, the counit map is an edge of
. Since the projection
is conservative, it is enough to show that the counit map of
is mapped to the counit map of . Indeed, for an object
,
we choose a Cartesian edge and a coCartesian
edge , and combine
them into a commutative diagram of the form:
where and .
Since is coCartesian, there exists a lift
that gives an edge
that is isomorphic to the counit map of the adjunction
at in the homotopy category . We can similarly construct
the counit map for an object of . The assertion
now follows from the above characterization of (co)Cartesian edges
in .
∎