Research

Coslice Colimits in Homotopy Type Theory

• Paper [CSL 2025] [errata]
• Technical report [arXiv] [local copy (more up-to-date)]
• Agda code [colimits-agda]

Mechanized study of coherent 2-groups

A fully mechanized biequivalence between coherent 2-groups and pointed connected 2-types along with an induced identity between them

• Agda code [2-groups-agda]
• Preprint [GitHub]