Iosif Petrakis: From dependent type theory to dependent category theory
Time: Wed 2023-11-01 11.00 - 12.30
Location: Albano house 1, floor 3, Room U (Kovalevsky)
Participating: Iosif Petrakis (LMU Münich)
Abstract
We introduce categories with dependent arrows, in order to grasp type-dependency in categorical terms. As arrows are categorical generalisations of functions, dependent arrows are categorical generalisations of dependent functions in Martin-Löf Type Theory. We present results first in the theory of categories with dependent arrows and Sigma-objects, and second in the theory of (the introduced) dependent fibrations between them. In this way we generalise results in the theory of type-categories of Pitts, and the theory of fibrations between them, respectively. All introduced notions, examples, and shown results have their dual version.