Topology seminar
Speaker: Jatin Atwal, IIT Bombay
Host: Rekha Santhanam
Title: An Introduction to Homotopy Type Theory
Time, day and date: 2:15:00 PM – 3:15:00 PM, Thursday, September 03
Venue: Room 215
Abstract: We'll give a brief overview of the subject. We'll start by looking at types, their structure, and the homotopy-theoretic properties they encode. We will talk about the two pillars of HoTT; Univalence axiom and Higher Inductive Types, and how these enable us to study homotopy theory from a synthetic viewpoint. If time permits, we'll look at the computational semantics of HoTT and how the theorems proved can be mechanically verified using proof assistants like Agda, Rocq, etc.
The talk does not assume any background, however some knowledge of homotopy theory would ease the flow of ideas.