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.)
An anabicategory consists of a set of objects, a set of 1-cells, which are relations , and a set of 2-cells, which are relations . (Note that only needs a defined equality relation, so the other two sets only need to be presets.) On these sets are defined several relations; for each relation if we have is said to be a value of at . Some pairs with are also said to be specified values; generally if has some value at , at least one such value will be specified. We omit the word “value” when it is clear from context. 1. There are source and target relations and , and every 1- or 2- cell has some specified value for its source and target. 1. There are 2-source and 2-target relations , and every 2- cell has some specified value for its 2-source and 2-target. 1. There are identity relations and , and every object or 1-cell has some specified value for its identity. 1. There is a composition relation ; whenever and are such that some specified target of is also a specified source of , there is some specified value of the composite of and . 1. There is a 1-composition relation ; whenever and are such that some specified 2-target at is also a specified 2-source at , there is some specified value of the 1-composite of and . 1. There is a 2-composition relation ; whenever and are such that some specified target at is also a specified source at , there is some specified value of the 2-composite of and .
The relations satisfy the following conditions: 1. For any 2-cell , and any values and of its source and target (respectively), the set of targets of , of targets of , and of 2-targets of are all equal (as subsets of ), and likewise for sources/2-sources. If or is a specified value of either relation, each specified value of its source is a specified value of the 2-source, and likewise for targets/2-targets. 1. Any source of an identity is also a target of , and vice versa. (However, we do not require the sets of specified values to match.) For any specified identity of , should be a specified source and target of . 1. If is composition of , the set of targets of is equal to the set of targets of , and the set of sources of is equal to the set of sources of . If is a specified composition, any specified target of is a specified target of , and any specified source of is a specified source of . (In general the converses may fail.) Moreover, if the composition has any value, the set of targets of is equal to the set of sources of . 1. If is a value of the 2-composition , the set of targets of is equal to the set of targets of , and the set of sources of is equal to the set of sources of . If is a specified value of the 2-composition, any specified target of is a specified target of , and any specified source of is a specified source of . Moreover, if the 2-composition has any value, the set of targets of is equal to the set of sources of . 1. If is a value of the 1-composition , each source of is a composition of some source of and some source of , and each such composition is a source of . For any specified sources of and , each specified value of their composition is a specified source of . The same results hold with source replaced by target. Moreover, if the 1-composition has any value, the set of 2-targets of is equal to the set of 2-sources of .
There are also conditions defining equivalence relations on and . (The equivalence relation for is simply equality.) All the relations defined above are required to be invariant under the appropriate equivalence relations (note, however, that their specified values do not need to be invariant). So in particular, the identity relation and the 1- and 2- composition relations are functional: any two values of the identity on some 1-cell , or any two values of one of the compositions on some 2-cells and , must be equal (as elements of .) * A 2-cell is said to be an isomorphism (between any of its sources and any of its targets) if there are some 2-cell and 1-cell such that the 2-composition of and is the identity on . We say that is an inverse of . * Two 1-cells and are isomorphic if there is a 2-cell isomorphism with as a source and as a target (or equivalently, vice versa). This is the chosen equivalence relation for . * A 1-cell is said to be an equivalence (between any of its sources and any of its targets) if there are some 1-cell and object such that some composition of and in either direction is isomorphic to an identity on . * Two objects and are equivalent if there is a 1-cell equivalence with as a source and as a target (or equivalently, vice versa). This is the chosen equivalence relation for .
Finally there are coherence relations: 1. Let be an identity 2-cell (in other words, a value of the identity relation for some 1-cell), and be any 2-cell. Then, if there is a 2-composition or , any such value is equal to . It follows (by considering their 2-composition) that identities on isomorphic 1-cells are equal, and that when two 1-cells are isomorphic, this fact will be witnessed by the identity on either object. 1. Let and be identity 2-cells on, say, and respectively, and suppose that exists. Then it is an identity 2-cell on any value of . Equivalently: the 1-composition of isomorphisms is an isomorphism. 1. Let be an identity 1-cell, and let be any 1-cell. Then, if there is a composition or , any such value is isomorphic to . It follows (by considering their composition) that identities on equivalent objects are isomorphic, and that when two objects are equivalent, this fact will be witnessed by the identity on either object. 1. Let , , and be 2-cells. If , and , then . (The latter values exist because the set of targets of and are equal, as are the set of sources of and .) 1. Let , , and be 2-cells. If , and , then . (The latter values exist because the set of 2-targets of and are equal, as are the set of 2-sources of and .) It follows that composition of 1-cells is also associative, up to isomorphism. 1. Let , , , and be 2-cells. If , , , and , then . (It follows from the preceding relations that these compositions exist.)
Every bicategory can be made into an anabicategory; we simply make the source, target, identity, and composition maps into relations with the original functions as specified values, then define the full values by isomorphism and equivalence. This will satisfy the coherence relations because the original bicategory satisfied the bicategory coherence relations.
On the other hand, we can also assume that every value of the defining relations is specified; then the anabicategory is said to be saturated. Any such anabicategory is clearly anaequivalent to a strict 2-category (just map each object or 1-cell to its equivalence class, and vice versa). For there to be a weak equivalence between the anabicategory and the 2-category, however, we would need the Axiom of Choice? (to pick out a single element of each equivalence class to serve as its image).