Intro to HoTT No. 5, Part 2
In this video, we conduct a formal development of product types in the HoTT deductive calculus, formalizing our informal work from the previous video. This provides an occasion to refine our intuitions for what Beta and Eta Computation rules mean.
