# 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.