Free Applicative Functors. - Paolo Capriotti; Ambrus Kaposi (MSFP, 2014)

Functions out of Higher Truncations. - Paolo Capriotti; Nicolai Kraus; Andrea Vezzosi (CSL, 2015)

Non-Wellfounded Trees in Homotopy Type Theory. - Benedikt Ahrens; Paolo Capriotti; Régis Spadotti (TLCA, 2015)

Extending Homotopy Type Theory with Strict Equality. - Thorsten Altenkirch; Paolo Capriotti; Nicolai Kraus (CSL, 2016)

Quotient inductive-inductive types. - Thorsten Altenkirch; Paolo Capriotti; Gabe Dijkstra; Fredrik Nordvall Forsberg (CoRR, 2016)

Two-Level Type Theory and Applications. - Danil Annenkov; Paolo Capriotti; Nicolai Kraus (CoRR, 2017)

Models of Type Theory with Strict Equality. - Paolo Capriotti (CoRR, 2017)

Models of type theory with strict equality. - Paolo Capriotti (2017)

Quotient Inductive-Inductive Types. - Thorsten Altenkirch; Paolo Capriotti; Gabe Dijkstra; Nicolai Kraus; Fredrik Nordvall Forsberg (FoSSaCS, 2018)

Univalent higher categories via complete Semi-Segal types. - Paolo Capriotti; Nicolai Kraus (Proc. ACM Program. Lang., 2018)

Higher Lenses. - Paolo Capriotti; Nils Anders Danielsson; Andrea Vezzosi (LICS, 2021)

Two-level type theory and applications. - Danil Annenkov; Paolo Capriotti; Nicolai Kraus; Christian Sattler (Math. Struct. Comput. Sci., 2023)

Two-level type theory and applications - ERRATUM. - Danil Annenkov; Paolo Capriotti; Nicolai Kraus; Christian Sattler (Math. Struct. Comput. Sci., 2024)