Intro to HoTT No. 5, Part 3
In this video, we conduct a formal development of product types in Agda, to complement our earlier informal developments (the product operation on homotopy spaces) and formalization in the HoTT deductive calculus. We use some function combinators to implement integer division in Agda and Haskell, running into some trouble with nontermination along the way.
