MAXIMILIAN PETROWITSCH

My main research interests are logic and the foundations of mathematics at the intersection of philosophy, pure mathematics, and theoretical computer science. I am particularly interested in categorical logic in a higher categorical setting. Roughly speaking, categorical logic generalizes the conventional conception of models of a theory as a structured set to models of a theory in arbitrary categories. The theories whose interpretation and semantics are given by categorical logic are in the most general setting some kind of type theory. Categorical logic thereby allows interpreting so-called proof-relevant environments, where proofs are considered to be themselves mathematical objects subject to reasoning. Conventionally, in Boolean or Heyting valued models, entailments between propositions can hold at maximum ‘in one way’. Models valued in categories allow admitting distinct parallel arrows between the objects to account for a semantic interpretation of distinct proofs of one statement from another. Categorical logic thereby combines constructivist, structuralist, and computational approaches to the foundations of mathematics.
   
 Developments in recent years, particularly the Univalent Foundations program and homotopy type theory, lead to such interpretations in higher categories. The concept of a higher category originates from homotopical algebra, which it allows making precise the notion of paths (or homotopies) between paths in a space from an algebraic viewpoint. In the setting of higher categories, one has in addition a potentially infinite tower of arrows between arrows on a lower level, allowing to interpret higher equivalences between terms and equivalences between proofs of equivalences up to infinity. In these so-called univalent type theories, it is possible to identify isomorphic or in some sense weakly equivalent objects. As a practical application, this interpretation has been increasingly used in recent years for formalizations of mathematical proofs in proof assistants which are based on constructive type theories such as Coq or Agda.
   
 Regarding my PhD project, I am in particularly interested in equivalences of models of different type theories in a higher categorical setting. I am also in general interested in studying and understanding the formal aspects and properties of the semantics for such theories such coherence, soundness and completeness, canonicity and decidability, in short, the ‘model theory’ of higher categorical logic.