Homotopy Type Theory Seminar

John Dykes, Department of Pure Mathematics, University of Waterloo

"Homotopy Type Theory and Univalent Foundations: Lecture 2"

Continuing from where we left off last week, we review function types. In discussing dependent pair and function types, we introduce the lambda calculus. We see the analogues of some standard set-theoretic constructions (products and coproducts, booleans, natural numbers) in the context of type theory. Using the analogy between propositions and types, we demonstrate how the axiom of choice can be (naively) rewritten as a type-theoretic statement. Time permitting, we  explain how the concepts of recursion and induction come alive in the type theory setting.

MC 5413