Mastodon Feed
Boosted by cstanhope@social.coop ("Your weary 'net denizen"):
carloangiuli@mathstodon.xyz ("Carlo Angiuli") wrote:
@danielgratzer 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.