Maximilian Petrowitsch

Publications

Elementary ∞-Toposes from Type Theory [arxiv] (jww. Daniël Apol)

Formalisation

Rocq/Coq

I am contributor of the Coq-HoTT Library.

Integers as Higher Inductive Type [PR, code] (jww. Dan Christensen)

Biinvertible maps [PR, code] (jww. Dan Christensen)

Talks

Elementary ∞-Toposes from Type Theory
Contributed:

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

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

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

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

Invited:

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

The Yoneda Lemma as a Principle of Structuralist Mathematics

Research Seminar, Lugano, 21 November 2025

Nominalism and Infinite Cardinality

ic.SoAP, Geneva, 12 June 2021

EENPS, Belgrade, 1 May 2021