Research

Google Scholar

Classifying 2-Groups in Homotopy Type Theory

• Paper [LICS 2026] [local copy]
  with Owen Milner
• Agda code [source] [html]

On Left Adjoints Preserving Colimits in Homotopy Type Theory

• Paper [CSL 2026]
  received the Helena Rasiowa Award
• Invited extended version [arXiv]
  submitted to Logical Methods in Computer Science
• Agda code [source]

Coslice Colimits in Homotopy Type Theory

• Paper [CSL 2025] [errata]
  with Favonia
• Technical report (latest update: March 2026) [arXiv]
• Agda code [source]