Logic & Lambdas: Context Extension

Description

In this video, we discuss the deductive rules governing arrow types: the application rule, the lambda abstraction rule, and the β & η rules.

Formalization links:

• The formalization I’m developing for this video series

HoTT textbooks:

• The HoTT Book (2013)—the original statement of HoTT
• Introduction to Homotopy Type Theory, by Egbert Rijke (to be released)