A double groupoid is, equivalently,
an n-fold groupoid for .
Let be a (2,1)-topos, hence a (2,1)-category whose objects may be thought of as groupoids equipped with some geometric structure (stacks). Then a double groupoid with that geometric structure is a groupoid object in an (2,1)-category in , hence a simplicial object
which satisfies the groupoidal Segal conditions.
In the literature, the following special cases of def. 1 are often taken to be the default notion of “double groupoid”.
A special case of example 1, in turn, are bare double groupoids in the image of the embedding , where is the 1-category of groupoids (suppressing the 2-morphisms given by natural isomorphisms). A groupoid object in is equivalently a pair of groupoids and equipped with functors , and that satisfy the usual axioms of a small category groupoid without any non-trivial natural isomorphisms weakening them. This is called a strict double groupoid.
If one writes out the structure functors
of a double groupoid themselves in components, one obtains a square diagram of the form
(where now we are notationally suppressing the degeneracy maps/identity assigning maps, for readability). In this form double groupoid are presented in traditional literature.
More generally, one can consider double groupoids in an arbitrary (∞,1)-topos , to be a 3-coskeletal groupoid object in an (∞,1)-category consisting degreewise of 1-truncated objects. The realization map
restricted to such double groupoids is a presentation of 2-truncated objects in .
Double Lie groupoids are discussed (usually for the strict case) in
Kirill Mackenzie, General theory of Lie groupoids and Lie algebroids Cambridge Univ. Press, Cambridge (2005)
Some homotopical aspects of double groupoids and their relationship to homotopy 2-types are explored in