left and right euclidean;
Here we consider the case , although we allow and to be of the form ; see (n,r)-category.
Let be a 2-congruence in a 2-category . * is a (2,1)-congruence if it is an internal groupoid, i.e. there is a map providing “inverses”. * It is a (1,2)-congruence if is ff. * It is a 1-congruence if it is both a (2,1)-congruence and a (1,2)-congruence. * it is a (0,1)-congruence if is an equivalence.
Note that in a 1-category,
Of course, a (0,1)-congruence in any 2-category is completely determined by any object .
Let be a morphism in . If is -truncated for , then is an -congruence. This means that:
The forward directions are fairly obvious; it is the converses which take work. Suppose first that is a (2,1)-congruence, and let be any 2-cell. Pulling back the eso along and gives and ; let be the pullback . Since is regular, is eso. By definition of kernels, the 2-cell corresponds to a map . But is a (2,1)-congruence, so composing this map with the “inverse” map gives another map , and thereby another 2-cell which is inverse to . Finally, since is eso, precomposing with it reflects invertibility, so must also be invertible. Thus is groupoidal.
Now suppose that is a (1,2)-congruence, and let be two parallel 2-cells. With notation as in the previous paragraph, the 2-cells and correspond to morphisms which become isomorphic in . But since is a (1,2)-congruence, this implies that the two maps are isomorphic, and hence . And since is eso, precomposing with it is faithful, so ; thus is posetal.
The discrete case follows by combining the posetal and groupoidal cases, so it remains to show that if is a (0,1)-congruence then is subterminal. We know it is discrete, so it suffices to show that given two we have a 2-cell . Continuing with the same notation, and letting be the induced maps with and , we have , and therefore the 2-cell defining the fork gives us a 2-cell and therefore . Now is the quotient of its kernel, so for this 2-cell to induce a 2-cell it suffices for it to be an action 2-cell for the actions of on and ; but this is automatic since we know to be posetal. Thus we have a 2-cell as desired, so is subterminal.