An anabicategory is a particular notion of weak 2-category appropriate in the absence of the axiom of choice (including in many internal contexts). It is derived from the notion of bicategory by replacing the composition functor?s with anafunctors (and therefore the associators and unitors with ananatural transformations).
Zoran Škoda: I understand that there is a version of using anafunctors, but it is not clear to me what are the axioms for a variant of 2-category which this example belongs to. I do not understand what you mean by replacing hom-functor with anafunctor in that definition: I mean which definition of bicategory is phrased in terms of hom-functors; standard definition talks associators and so on…Please be more explicit.
Mike: Is this version clearer?
Toby: Or look at the complete definition in the reference that I just added.
If Cat is defined as consisting of (small) categories, anafunctors, and ananatural transformations (as is most appropriate in the absence of choice), then is more naturally an anabicategory rather than any stricter notion.
Mike: Is that only because of the non-canonicity of pullbacks in ? If our version of has canonical chosen pullbacks, do we get an ordinary bicategory?
Toby: H'm … as I recall, you get an ordinary bicategory using canonical pullbacks and general anafunctors, but if you move to saturated anafunctors, then you still only get an anabicategory. I should check this and then rewrite (here and at Cat) to say it correctly. (Of course, if you really use anafunctors, then you should only want an anabicategory.)