Carlo Angiuli5d ago

New draft of Principles of Dependent Type Theory with @danielgratzer:
https://www.carloangiuli.com/papers/type-theory-book.pdf

This is a minor release with a lot of small improvements and typo fixes, and a sneak preview of a forthcoming appendix 🤫

Show threadNaïm Camille Favier5d ago

@carloangiuli @danielgratzer couple more things:

  • the proof of lemma 6.3.28 overflows
  • in the proof of lemma 6.3.28, "the condition naturality"
  • in the statement of lemma 6.3.29, i think "an assignment of X to Y" usually means Y ↦ X. might be worth reformulating this even if it's not really ambiguous
  • in slogan 6.3.31, â‹” should be ⋔ˢᵗ, and F should be F_Î¥
  • in §6.3.4.2, "The categorical encoding the intensional identity is consequently encoded as follows"
Show threaddaniel gratzer
@ncf @carloangiuli Thanks! Can you please send these over email---I can't keep track of issues raised here without handling them synchronously which isn't usually feasible.
Mar 19 at 4:18pmWeb
Show threadNaïm Camille Favier5d ago
@danielgratzer @carloangiuli sure