Craig Stuntz
Carlo AngiuliNew 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 🤫
Naïm Camille Favier@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"
daniel 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.
theHigherGeometer@carloangiuli The link to the draft seems to be broken for me
@highergeometer Huh, it works for me and there shouldn't be any permissions issues...? What if you go to my website and click on the link there? https://carloangiuli.com
Namdak Tönpa@carloangiuli one of the most not boring academic pages 👍
@carloangiuli I can't even open your website's home page!
@highergeometer That's very odd, and the first time anybody has said that to me! If you have multiple ISPs (e.g., home, cellular, work) have you tried more than one of them?
I would be happy to email you the PDF if you like... The book is also available on https://www.danielgratzer.com but @danielgratzer hasn't updated his copy to the latest draft yet. :)
@carloangiuli works on a different device, now. Weird.
edit; and now it works on the original machine in the browser I was trying before. A transient issue, it seems. Thanks for your patience!
Jean Abou Samra (new account)@carloangiuli @danielgratzer Yesterday there was a BSc student writing a thesis on combinatory logic who was asking me where he could find a readable definition of GATs. I think he'll be interested in your appendix when it's ready 🙂