We will discuss the core type theory from the HoTT Book. Our discussion will be based on Appendix A.2. It will be helpful to have looked at Chapter 1 as well.

Daniel Son will lead the session.