Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
It occurred to me that HoTT should have something to say about anafunctors, if only to say they’re already built in, or something like that. But I can’t see the two terms appearing together anywhere (no ’anafuntor’ in the HoTT book, no ’type’ in anafunctor) except in this blog post:
To work in category theory based on set theory and classical logic, while avoiding AC, one is therefore justified in “mixing and matching” functors and anafunctors as convenient, but discussing them all as if they were regular functors (except when defining a particular anafunctor). Such usage can be formalized by turning everything into an anafunctor, and translating functor operations and properties into corresponding operations and properties of anafunctors.
there is a better solution, which is to throw out set theory as a foundation of category theory and start over with homotopy type theory. In that case, thanks to a generalized notion of equality, regular functors act like anafunctors, and in particular AP holds.
This AP is
“Axiom of Protoequivalence”—that is, the statement that every fully faithful, essentially surjective functor (i.e. every protoequivalence) is an equivalance
I can’t see that the blogger got round to starting over with HoTT.
So my question is whether something useful could be added to anafunctor even if it’s only to say that HoTT renders it unnecessary, or whatever it does?
I can’t see that the blogger got round to starting over with HoTT.
It is discussed more in his PhD thesis: https://github.com/byorgey/thesis/raw/master/Yorgey-thesis-final-2014-11-17.pdf
Though surely there is more to say.
If you know what an anafunctor is, then on reading chapter 9 of the book carefully you may detect their ghostly presence. (-: The short answer is that anafunctors are unnecessary when using “saturated/univalent” categories in HoTT, because of their “functor comprehension principle”. An anafunctor is a span whose first leg is a surjective and fully faithful functor, but for saturated categories any such functor is an equivalence (in the strong sense of having an inverse), so any anafunctor is equivalent to a functor.
I extracted #3 in a new section, although perhaps it should come earlier. There are terms to explain there. Is the ’saturated’ the same as in saturated class of maps or saturated class of limits? There’s also ’saturated homotopical category’ at relative category. By the way, none of these last three pages mentions each other.
Saturated/univalent would be something like ’projective’. The functor pointing the wrong in an anafunctor is an acyclic fibration (in the canonical model structure), and having its codomain saturated guarantees a splitting.
No, no relation to other kinds of saturation. Also it’s not projectivity but more like injectivity; it’s not univalence of the domain of an anafunctor that makes it a functor but rather the codomain. See theorem 9.9.4 in the HoTT book: univalent categories are local with respect to weak equivalences.
I put in a reference to def 9.1.3, as the notes to chap. 9 suggest.
@Mike
Then I don’t understand what you mean by this sentence :
An anafunctor is a span whose first leg is a surjective and fully faithful functor, but for saturated categories any such functor is an equivalence (in the strong sense of having an inverse)
Since you haven’t referred to the codomain of the anafunctor here at all, merely the ’domain half’. Did you mean for ff and surjective on objects that saturated or saturated this becomes a legit equivalence?
Yes, I think C saturated suffices, but C and D both saturated certainly suffices. By “for saturated categories” I meant “if all categories in sight are saturated”.
1 to 9 of 9