equivalences in/of $(\infty,1)$-categories
An (∞,1)-functor is conservative if its reflects equivalences in an (∞,1)-category. This means that on homotopy categories it is a conservative functor.
In an (∞,1)-topos, (∞,1)-pullback along an effective epimorphism is a conservative (∞,1)-functor between slice (∞,1)-categories.
We write in the conjectural internal logic of an (∞,1)-topos expressed as homotopy type theory, with slice (∞,1)-categories represented using dependent types. The reader is free to translate this manually into an (∞,1)-category-theoretic proof.
Thus, suppose $f:A\to B$ is a surjection (i.e. $\prod_{b:B} \exists_{a:A} f(a)=b$, where $\exists$ denotes the propositional truncation of $\sum$). Let $P,Q:B\to Type$ be dependent types with a fiberwise map $g:\prod_{b:B} P(b) \to Q(b)$ which becomes a fiberwise equivalence upon restricting to $A$, i.e. such that $\prod_{a:A} IsEquiv(g(f(a)))$. We must show that $g$ is itself a fiberwise equivalence.
Thus, let $b:B$; we must show $IsEquiv(g(b))$. By assumption we have $\exists_{a:A} f(a)=b$. But $IsEquiv(g(b))$ is an h-proposition, so we may strip the truncation and obtain an $a:A$ such that $f(a)=b$. Transporting along this equality, it suffices to show $IsEquiv(g(f(a)))$, but this follows from the other assumption.
See also Lemma 6.2.3.16 in Higher Topos Theory.
In the context of quasi-categories, def. 6.2.1 in
Last revised on February 13, 2017 at 17:38:53. See the history of this page for a list of all contributions to it.