In this talk, we will outline an Agda implementation of a higher-dimensional piece of the homotopy hypothesis, which provides a general correspondence between groupoids and homotopy types. The groupoids we look at are monoidal groupoids where every element has the structure of an adjoint equivalence, called coherent $2$-groups. The correspondence for such groupoids takes the form of a biequivalence between the $\left(2,1\right)$-category of coherent $2$-groups and the $\left(2,1\right)$-category of pointed connected (homotopy) $2$-types. We build this biequivalence in homotopy type theory (HoTT) and use Agda to verify the construction (see https://github.com/PHart3/2-groups-agda). Thanks to the univalence axiom, we also obtain a verified identity between the two $\left(2,1\right)$-categories in question.

This biequivalence has been suggested at a few places in the literature. Inside HoTT, Buchholtz, van Doorn, and Rijke (2018) propose it as a $2$-dimensional generalization of the equivalence they construct between $\mathbf{Grp}$ and pointed connected $1$-types. It also was suggested in the classical setting by Baez and Lauda (2004).

Indeed, the biequivalence we construct generalizes the $1$-dimensional equivalence. It consists of two broad steps. First, we construct the classifying space of a coherent $2$-group $G$ as a higher inductive type by generalizing the first Eilenberg-MacLane space of a group. This defines a function from the type of coherent $2$-groups to the type of pointed connected $2$-types. Second, we equip this function with the structure of a pseudofunctor and prove that it forms a biequivalence with the loop space pseudofunctor, which takes a pointed connected $2$-type to its fundamental $2$-group.

Each step is purely algebraic, and all our proofs are constructive. Notably, combined with recent work by Owen Milner (unpublished), our biequivalence computes the Sinh invariant of a coherent $2$-group within a constructive system, whereas the traditional method relies on the axiom of choice. Our formalization, however, involves several huge computations, and we will discuss our experience managing its memory requirements and its arduous type-checking.