Abstract

This thesis introduces displayed univalent reflexive graphs, a natural analogue of displayed categories, as a framework for uniformly internalizing composite mathematical structures in homotopy or cubical type theory. This framework is then used to formalize the definition of and equivalence of strict 2-groups and crossed modules. Lastly, foundations for the development of higher groups from the classifying space perspective in cubical type theory are laid. Most results are formalized in Cubical Agda.