@danielgratzer@mathstodon.xyz and I have just released a new version of _Principles of Dependent Type Theory_! This one is a significant milestone: all planned content has been drafted; we do not expect any new sections at this point. Main changes: - Added Appendix B on generalized algebraic theories! This resolves some unfinished business from earlier in the book, by proving the "initiality theorem" for ETT/ITT. - Added a draft of Section 4.4 on observational type theory. - Removed "solutions to selected exercises", and converted the most important handful of exercises into lemmas with proofs. - Various improvements to Chapter 6 (categorical semantics). - Expanded Section 3.6 on undecidability of equality in ETT, including a series of exercises establishing the undecidability of equality in TT with judgmental Nat-eta. https://www.carloangiuli.com/papers/type-theory-book.pdf