Coslice Colimits in Homotopy Type Theory

We present a fully mechanized derivation of colimits in coslices of a type universe
from ordinary colimits along with a formal proof that the forgetful functor creates
colimits over trees. We also present applications to factorization systems, higher
group theory, and generalized cohomology theory.

Mechanized Study of Coherent 2-groups

We present a fully mechanized biequivalence between the (2,1)-category of
coherent 2-groups and that of pointed connected 2-types along with an induced
identity between them via univalence.

Left Adjoints and Colimits in Homotopy Type Theory

We examine the relation between left adjoints and graph-indexed colimits in the
setting of wild categories. We establish a relatively modest sufficient condition
for left adjoints to preserve such colimits and present useful examples of left
adjoints satisfying it. These results are fully formalized.