As we continue our foray into the book, we begin to view types as spaces (or, “equivalently”, as omega groupoids). My goal for this section is to focus on the path induction rule and argue that it corresponds to the path-loop fibration.

More specifically, we can make an analogy between the path space over a space X and the type of all equivalences over a type A. The path space of X is homotopy equivalent to X, and I argue that path induction says “essentially the same thing” about the type of all equivalences over A. I aim to make this analogy as formal as possible, and then delve further into the material in chapter 2.

I would also like to go over some exercises. I’ve done a few, but if anyone wants to come up to the board and show off, then they are welcome!

In this talk we give a computationally motivated presentation of J-Calc. J-Calc is an extension of simply typed lambda calculus with justifications and justified modal types.

Initiating from textbook examples of modular programs, we will present the modal type theory of J-Calc as a type system corresponding to programming with modular definitions. More specifically, we will show how justified modality offers a logical reading to separate compilation in modular functional programming.