Maximilian Petrowitsch

Preprints

Elementary Infinity-Toposes from Type Theory, arxiv: 2512.18891

Talks

Elementary Infinity-Toposes from Type Theory, CMS Summer Meeting, Session: Category Theory: Structures and Applications, Université Laval, Quebec City, June 8, 2025

Elementary Infinity-Toposes from Type Theory, 32nd Foundational Methods in Computer Science Workshop, University of Ottawa, Ottawa, June 20, 2025

Nominalism and Infinite Cardinality, ic.SoAP/EENPS, Belgrade and Geneva/Lugano (Online), 2021

Formalisation projects

Integers as Higher Inductive Types, Formalisation of (Altenkirch and Scoccola 2020) in Coq, repo