Eilenberg-MacLane spaces in homotopy type theory. - Daniel R. Licata; Eric Finster (CSL-LICS, 2014)

A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory. - Kuen-Bang Hou (Favonia); Eric Finster; Daniel R. Licata; Peter LeFanu Lumsdaine (LICS, 2016)

A type-theoretical definition of weak ω-categories. - Eric Finster; Samuel Mimram (LICS, 2017)

A Type Theory for Strictly Unital ∞-Categories. - Eric Finster; David Reutter; Jamie Vicary (CoRR, 2020)

Types Are Internal ∞-Groupoids. - Eric Finster; Antoine Allioux; Matthieu Sozeau (LICS, 2021)

Globular weak ω-categories as models of a type theory. - Thibaut Benjamin; Eric Finster; Samuel Mimram (CoRR, 2021)

A Type Theory for Strictly Associative Infinity Categories. - Eric Finster; Alex Rice; Jamie Vicary (CoRR, 2021)

A Cartesian Bicategory of Polynomial Functors in Homotopy Type Theory. - Eric Finster; Samuel Mimram; Maxime Lucas; Thomas Seiller (MFPS, 2021)

A Type Theory for Strictly Unital ∞-Categories. - Eric Finster; David Reutter; Jamie Vicary; Alex Rice (LICS, 2022)

Strictly Associative and Unital $ infty$-Categories as a Generalized Algebraic Theory. - Eric Finster; Alex Rice; Jamie Vicary (CoRR, 2023)

A Syntax for Strictly Associative and Unital ∞-Categories. - Eric Finster; Alex Rice; Jamie Vicary (LICS, 2024)