Topology Seminar
Speaker: Thomas Jan Mikhail
Title: Type Theory for the Working Mathematician (part 2)
Date: 3/5/2024
Time: 12:00
Abstract: In this talk we pick up where we left off last time (12/04/2024) and begin by first sketching out the relationship between type theories and logic, known as the Curry-Howard correspondence. In the remainder of the talk we will go through some applications, exemplifying the utility of type theory as a tool for proving statements in categories. Depending on the time these may include algebraic theories, topoi and homotopy type theory.