This is another session of the PhD introduction series.

Chaitanya will do a 30 minutes talk. Given that the talk will not last as long as usual, we will also take advantage of the opportunity to discuss the organization of the seminar.

Abstract:

The talk will not be about my particular research problem. It will seek instead to give a gentle pictorial introduction to the inherent structure of dependent types and how this structure determines what dependent types and dependently-typed programs (or proofs) *mean*.

The focus will be on why this structure naturally leads to homotopy type theory and univalence. As a bonus, and if time permits, there will be some remarks on univalence and extensionality.