Maximilian Petrowitsch

Preprints

Elementary ∞-Toposes from Type Theory, arxiv: 2512.18891 (jww. Daniël Apol)

Talks

Elementary ∞-Toposes from Type Theory

Category Theory 2026 (International Congress of Mathematicians), Johns Hopkins University, Baltimore, July 16, 2026

3rd Workshop on Syntax and Semantics of Type Theory, Faculty of Mathematics and Physics, Ljubljana, June 4, 2026

Workshop on Homotopy Type Theory / Univalent Foundations 2026, Aarhus University, Aarhus, June 2, 2026

32nd Foundational Methods in Computer Science Workshop, University of Ottawa, Ottawa, June 20, 2025

Canadian Mathematical Society Summer Meeting, Session: Category Theory: Structures and Applications, Université Laval, Quebec City, June 8, 2025

The Yoneda Lemma as a Principle of Structuralist Mathematics

Reserach Seminar, Lugano, November 21, 2025

Nominalism and Infinite Cardinality

ic.SoAP, Geneva, June 12, 2021

EENPS, Belgrade, May 1, 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)