equivalences in/of $(\infty,1)$-categories
equality (definitional?, propositional, computational, judgemental, extensional, intensional, decidable)
isomorphism, weak equivalence, homotopy equivalence, weak homotopy equivalence, equivalence in an (∞,1)-category
Examples.
An (∞,1)-functor between (∞,1)-categories is an equivalence in (∞,1)Cat precisely if it is an essentially surjective (∞,1)-functor and a full and faithful (∞,1)-functor.
When (∞,1)-categories are presented by quasi-categories, an equivalence between them is presented by a weak equivalence in the model structure for quasi-categories.
An (∞,1)-functor $f : C \to D$ is an equivalence in (∞,1)Cat if the following equivalent conditions hold
On the underlying simplicial sets it is a weak categorical equivalence in Joyal’s model structure for quasi-categories.
For every simplicial set $K$ the induced morphism $f_* : SSet(K,C) \to SSet(K,D)$ is a weak categorical equivalence.
For every simplicial set $K$ the induced morphism $f_* : Core(SSet(K,C)) \to Core(SSet(K,D))$ on the maximal Kan complexes is a equivalence of Kan complexes (a homotopy equivalence).
This is HTT, lemma 3.1.3.2.
equivalence of (∞,1)-categories, adjoint (∞,1)-functor