Google Scholar

Coslice Colimits in Homotopy Type Theory

We present a fully mechanized derivation of (graph-indexed) 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.

A 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.

On Left Adjoints Preserving 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 mild sufficient condition for
left adjoints to preserve such colimits and present useful examples of left adjoints
satisfying it. These results are fully formalized.