conservative (∞,1)-functor



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:ABf:A\to B is a surjection (i.e. b:B a:Af(a)=b\prod_{b:B} \exists_{a:A} f(a)=b, where \exists denotes the propositional truncation of \sum). Let P,Q:BTypeP,Q:B\to Type be dependent types with a fiberwise map g: b:BP(b)Q(b)g:\prod_{b:B} P(b) \to Q(b) which becomes a fiberwise equivalence upon restricting to AA, i.e. such that a:AIsEquiv(g(f(a)))\prod_{a:A} IsEquiv(g(f(a))). We must show that gg is itself a fiberwise equivalence.

Thus, let b:Bb:B; we must show IsEquiv(g(b))IsEquiv(g(b)). By assumption we have a:Af(a)=b\exists_{a:A} f(a)=b. But IsEquiv(g(b))IsEquiv(g(b)) is an h-proposition, so we may strip the truncation and obtain an a:Aa:A such that f(a)=bf(a)=b. Transporting along this equality, it suffices to show IsEquiv(g(f(a)))IsEquiv(g(f(a))), but this follows from the other assumption.

See also Lemma 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.