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

I am contributor of the Coq-HoTT Library.

Most recent project: Formalisation of 'Integers as Higher Inductive Types' (Altenkirch and Scoccola 2020)' in Rocq/Coq, repo (jww. Dan Christensen)