homotopy hypothesis-theorem
delooping hypothesis-theorem
stabilization hypothesis-theorem
n-category = (n,n)-category
n-groupoid = (n,0)-category
category object in an (∞,1)-category, groupoid object
A double groupoid is, equivalently,
a double category in which all 1-morphisms and 2-morphisms are isomorphisms;
a groupoid object internal to the 1-category Grpd;
an n-fold groupoid for $n = 2$.
Equipped with the relevant extra stuff, structure, property one obtains notions of double topological groupoids, double Lie groupoids, etc.
Let $\mathbf{H}$ 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 $\mathbf{H}$, 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”.
The archetypical special case of def. 1 is that where $\mathbf{H} =$ Grpd is the (2,1)-category of bare (geometrically discrete) groupoids.
A special case of example 1, in turn, are bare double groupoids in the image of the embedding $Grpd_1^{\Delta^{op}} \to Grpd^{\Delta^{op}}$, where $Grpd_1$ is the 1-category of groupoids (suppressing the 2-morphisms given by natural isomorphisms). A groupoid object in $Grpd_{1}$ is equivalently a pair of groupoids $\mathcal{G}_1$ and $\mathcal{G}_0$ equipped with functors $s,t \colon \mathcal{G}_1 \to \mathcal{G}_0$, $i \colon \mathcal{G}_0 \to \mathcal{G}_1$ and $\circ \colon \mathcal{G}_1 \times_{\mathcal{G}_0} \mathcal{G}_1 \to \mathcal{G}_1$ 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 $\mathcal{G}_\bullet$ 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.
For $\mathbf{H} =$ SmoothGrpd, double groupoids in $\mathbf{H}$ which are in the inclusion of LieGrpd${\Delta}^{op} \to$ SmoothGrpd${}^{\Delta^{op}}$ are called double Lie groupoids.
More generally, one can consider double groupoids in an arbitrary (∞,1)-topos $\mathbf{H}$, 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 $\mathbf{H}$.
Double Lie groupoids are discussed (usually for the strict case) in
Ronnie Brown, Kirill Mackenzie, Determination of a double Lie groupoid by its core diagram. J. Pure Appl. Algebra 80 (1992), no. 3, 237–272
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