nLab
anabicategory

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 :B(y,z)×B(x,y)B(x,z)\circ: B(y,z) \times B(x,y) \to B(x,z) with anafunctors (and therefore the associators and unitors with ananatural transformations).

Zoran Škoda: I understand that there is a version of CatCat 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 CatCat is more naturally an anabicategory rather than any stricter notion.

Mike: Is that only because of the non-canonicity of pullbacks in SetSet? If our version of SetSet 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.)

Explicit definition

An anabicategory 𝒞\mathcal{C} consists of a set 𝒞 0\mathcal{C}_0 of objects, a set 𝒞 1\mathcal{C}_1 of 1-cells, which are relations 𝒞 0×𝒞 0\mathcal{C}_0 \times \mathcal{C}_0, and a set 𝒞 2\mathcal{C}_2 of 2-cells, which are relations 𝒞 1×𝒞 1\mathcal{C}_1 \times \mathcal{C}_1. (Note that only 𝒞 2\mathcal{C}_2 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 RR if we have R(x,y)R(x, y) yy is said to be a value of RR at xx. Some pairs x,yx, y with R(x,y)R(x, y) are also said to be specified values; generally if RR has some value at xx, 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 𝒞 1×𝒞 0\mathcal{C}_1 \times \mathcal{C}_0 and 𝒞 2×𝒞 1\mathcal{C}_2 \times \mathcal{C}_1, and every 1- or 2- cell ff has some specified value for its source and target.
  2. There are 2-source and 2-target relations 𝒞 2×𝒞 0\mathcal{C}_2 \times \mathcal{C}_0, and every 2- cell ff has some specified value for its 2-source and 2-target.
  3. There are identity relations Id:𝒞 0×𝒞 1Id:\mathcal{C}_0 \times \mathcal{C}_1 and 𝒞 1×𝒞 2\mathcal{C}_1 \times \mathcal{C}_2, and every object or 1-cell has some specified value for its identity.
  4. There is a composition relation :(𝒞 1×𝒞 1)×𝒞 1\circ:(\mathcal{C}_1 \times \mathcal{C}_1) \times \mathcal{C}_1; whenever f 1f_1 and f 2f_2 are such that some specified target of f 1f_1 is also a specified source of f 2f_2, there is some specified value of the composite of f 1f_1 and f 2f_2.
  5. There is a 1-composition relation 1:(𝒞 2×𝒞 2)×𝒞 2\circ_1:(\mathcal{C}_2 \times \mathcal{C}_2) \times \mathcal{C}_2; whenever f 1f_1 and f 2f_2 are such that some specified 2-target at f 1f_1 is also a specified 2-source at f 2f_2, there is some specified value of the 1-composite of f 1f_1 and f 2f_2.
  6. There is a 2-composition relation 2:(𝒞 2×𝒞 2)×𝒞 2\circ_2:(\mathcal{C}_2 \times \mathcal{C}_2) \times \mathcal{C}_2; whenever f 1f_1 and f 2f_2 are such that some specified target at f 1f_1 is also a specified source at f 2f_2, there is some specified value of the 2-composite of f 1f_1 and f 2f_2.

The relations satisfy the following conditions:

  1. For any 2-cell ff, and any values xx and yy of its source and target (respectively), the set of targets of xx, of targets of yy, and of 2-targets of ff are all equal (as subsets of 𝒞 1\mathcal{C}_1), and likewise for sources/2-sources. If xx or yy 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.
  2. Any source of an identity xx is also a target of xx, and vice versa. (However, we do not require the sets of specified values to match.) For any specified identity yy of xx, xx should be a specified source and target of yy.
  3. If hh is composition of fgf \circ g, the set of targets of ff is equal to the set of targets of hh, and the set of sources of gg is equal to the set of sources of hh. If hh is a specified composition, any specified target of ff is a specified target of hh, and any specified source of gg is a specified source of hh. (In general the converses may fail.) Moreover, if the composition fgf \circ g has any value, the set of targets of gg is equal to the set of sources of ff.
  4. If hh is a value of the 2-composition f 2gf \circ_2 g, the set of targets of ff is equal to the set of targets of hh, and the set of sources of gg is equal to the set of sources of hh. If hh is a specified value of the 2-composition, any specified target of ff is a specified target of hh, and any specified source of gg is a specified source of hh. Moreover, if the 2-composition f 2gf \circ_2 g has any value, the set of targets of gg is equal to the set of sources of ff.
  5. If hh is a value of the 1-composition f 1gf \circ_1 g, each source of hh is a composition of some source of ff and some source of gg, and each such composition is a source of hh. For any specified sources of ff and gg, each specified value of their composition is a specified source of hh. The same results hold with source replaced by target. Moreover, if the 1-composition f 1gf \circ_1 g has any value, the set of 2-targets of gg is equal to the set of 2-sources of ff.

There are also conditions defining equivalence relations on 𝒞 0\mathcal{C}_0 and 𝒞 1\mathcal{C}_1. (The equivalence relation for 𝒞 2\mathcal{C}_2 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 𝒞 1×𝒞 2\mathcal{C}_1\times \mathcal{C}_2 and the 1- and 2- composition relations (𝒞 2×𝒞 2)×𝒞 2(\mathcal{C}_2 \times \mathcal{C}_2) \times \mathcal{C}_2 are functional: any two values of the identity on some 1-cell xx, or any two values of one of the compositions on some 2-cells ff and gg, must be equal (as elements of 𝒞 2\mathcal{C}_2.)

  • A 2-cell ff is said to be an isomorphism (between any of its sources and any of its targets) if there are some 2-cell gg and 1-cell xx such that the 2-composition of ff and gg is the identity on xx. We say that gg is an inverse of ff.
  • Two 1-cells ff and gg are isomorphic if there is a 2-cell isomorphism hh with ff as a source and gg as a target (or equivalently, vice versa). This is the chosen equivalence relation for 𝒞 1\mathcal{C}_1.
  • A 1-cell ff is said to be an equivalence (between any of its sources and any of its targets) if there are some 1-cell gg and object xx such that some composition of ff and gg in either direction is isomorphic to an identity on xx.
  • Two objects xx and yy are equivalent if there is a 1-cell equivalence gg with xx as a source and yy as a target (or equivalently, vice versa). This is the chosen equivalence relation for 𝒞 0\mathcal{C}_0.

Finally there are coherence relations:

  1. Let ff be an identity 2-cell (in other words, a value of the identity relation for some 1-cell), and gg be any 2-cell. Then, if there is a 2-composition f 2gf \circ_2 g or g 2fg \circ_2 f, any such value is equal to gg. 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.
  2. Let ff and gg be identity 2-cells on, say, xx and yy respectively, and suppose that f 1gf \circ_1 g exists. Then it is an identity 2-cell on any value of xyx \circ y. Equivalently: the 1-composition of isomorphisms is an isomorphism.
  3. Let ff be an identity 1-cell, and let gg be any 1-cell. Then, if there is a composition fgf \circ g or gfg \circ f, any such value is isomorphic to gg. 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.
  4. Let ff, gg, and hh be 2-cells. If F=f 2gF = f \circ_2 g, and G=g 2hG = g \circ_2 h, then F 2h=f 2GF \circ_2 h = f \circ_2 G. (The latter values exist because the set of targets of GG and gg are equal, as are the set of sources of gg and FF.)
  5. Let ff, gg, and hh be 2-cells. If F=f 1gF = f \circ_1 g, and G=g 1hG = g \circ_1 h, then F 1h=f 1GF \circ_1 h = f \circ_1 G. (The latter values exist because the set of 2-targets of GG and gg are equal, as are the set of 2-sources of gg and FF.) It follows that composition of 1-cells is also associative, up to isomorphism.
  6. Let f 1f_1, f 2f_2, g 1g_1, and g 2g_2 be 2-cells. If F=f 1 1f 2F = f_1 \circ_1 f_2, G=g 1 1g 2G = g_1 \circ_1 g_2, H 1=f 1 2g 1H_1 = f_1 \circ_2 g_1, and H 2=f 2 2g 2H_2 = f_2 \circ_2 g_2, then F 1G=H 1 2H 2F \circ_1 G = H_1 \circ_2 H_2. (It follows from the preceding relations that these compositions exist.)

So every anabicategory is “anaskeletal” (every equivalence is an identity), and “anastrict:” its associators and unitors are also identities.

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).

Reference

  • Michael Makkai; Avoiding the axiom of choice in general category theory; section 3 (which is part 4 here).
Revised on December 12, 2013 09:39:51 by Ben Standeven? (76.215.118.137)