The notion of final $(\infty,1)$-functor (also called a cofinal $(\infty,1)$-functor) is the generalization of the notion of final functor from category theory to (∞,1)-category-theory.
An (∞,1)-functor $p : K' \to K$ is final precisely if precomposition with $p$ preserves colimits:
if $p$ is final then for for $F : K \to C$ any (∞,1)-functor we have
when either of these colimits exist.
(final morphism of simplicial set)
A morphism $p : S \to T$ of simplicial sets is final if for every right fibration $X \to T$ the induced morphism of simplicial sets
is a homotopy equivalence.
So in the overcategory $sSet/T$ a final morphism is an object such that morphisms out of it into any right fibration are the same as morphisms out of the terminal object into that right fibration.
This definition is originally due to Andre Joyal. It appears as HTT, def 4.1.1.1.
This is equivalent to the following definition, in terms of the model structure for right fibrations:
The morphism $p : S \to T$ is final precisely if the terminal morphism $(p \to *) = \left( \array{ S &&\to&& T \\ & {}_{\mathllap{}}\searrow && \swarrow_{=} \\ && T } \right)$ in the overcategory $sSet_T$ is a weak equivalence in the model structure for right fibrations on $sSet_T$.
This is HTT, prop. 4.1.2.5.
If $T$ is a Kan complex then $p : S \to T$ is final precisely if it is a weak equivalence in the standard model structure on simplicial sets.
This is HTT, cor. 4.1.2.6.
(preservation of undercategories and colimits)
A morphism $p : K' \to K$ of simplicial sets is final precisely if for every quasicategory $C$
and equivalently precisely if
… and for every $F : K \to C$ the morphism
of under quasi-categories induced by composition with $p$ is an equivalence of (∞,1)-categories.
This is HTT, prop. 4.1.1.8.
The following result is the $(\infty,1)$-categorical analog of what is known as Quillen’s Theorem A.
(recognition theorem for final $(\infty,1)$-functors)
A morphism $p : K \to C$ of simplicial sets with $C$ a quasi-category is final precisely if for each object $c \in C$ the comma-object $c/p := c/C \times_C K$ is weakly contractible.
More explicitly, the comma object in question here is the pullback
where $c/C$ is the under quasi-category under $c$.
This is due to Andre Joyal. A proof appears as HTT, prop. 4.1.3.1.
The following says that up to equivalence, the cofinal maps of simplicial sets are the right anodyne morphisms
A map of simplicial sets is cofinal precisely if it factors as a right anodyne map followed by a trivial fibration.
This is (Lurie, cor. 4.1.1.12).
The inclusion $\ast \to \mathcal{C}$ of a terminal object is final.
By theorem 1 the inclusion of the point is final precisely if for all $c \in \mathcal{C}$, the (∞,1)-categorical hom-space $\mathcal{C}(c,\ast)$ is contractible. This is the definition of $\ast$ being terminal.
For $K \in$ sSet a simplicial set, write $\Delta_{/K}$ for its category of elements, called here the category of simplices of the simplicial set:
an object of $\Delta_{/K}$ is a morphism of simplicial sets of the form $\Delta^n \to K$ for some $n \in \mathbb{N}$ (hence an $n$-simplex of $K$) and a morphism is a commuting diagram
Moreover, write
for the full subcategory on the non-degenerate simplices.
The category $\Delta_{/K}^{nd}$ is also known as the barycentric subdivision of $K$.
The inclusion
is a cofinal morphism of quasi-categories.
This appears as (Lurie, variant 4.2.3.15).
For every simplicial set $K$ there exists a cofinal map
This is (Lurie, prop. 4.2.3.14).
final $(\infty,1)$-functor
Section 4.1 of
Section 6 of