Timeline for type theory that does not treat the terms of $\mathrm{Prop}$ as types
Current License: CC BY-SA 3.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 18, 2015 at 12:14 | comment | added | Myshkin | @PeterLeFanuLumsdaine Thanks, I hadn't considered it that way. I've reverted the edit. | |
| Oct 18, 2015 at 12:13 | history | rollback | Myshkin |
Rollback to Revision 1
|
|
| Oct 18, 2015 at 12:08 | comment | added | Peter LeFanu Lumsdaine |
@Myshkin: re your edit, the use of code formatting instead of $\LaTeX$ in this answer may have been a deliberate preference. Since type theories are often used as programming languages (e.g. Coq, Agda), some people like to borrow the syntax of such languages when discussing type theory. The $\LaTeX$ is fine too, but in future, I would suggest not “correcting” code formatting in type theory like one does in other contexts.
|
|
| Oct 18, 2015 at 12:02 | history | edited | Myshkin | CC BY-SA 3.0 |
+latex (same notation as the OP used)
|
| Sep 17, 2015 at 23:05 | history | answered | gallais | CC BY-SA 3.0 |