Timeline for $\infty$-categorical interpretation of type theory
Current License: CC BY-SA 3.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 20, 2013 at 9:14 | vote | accept | Simon Henry | ||
| Jul 20, 2013 at 9:14 | vote | accept | Simon Henry | ||
| Jul 20, 2013 at 9:14 | |||||
| Jul 20, 2013 at 9:13 | comment | added | Simon Henry | Thank you ! Your answer suggest that the obstruction is only at the level of the relation between object classifier and univalent universe. Does this mean that it is indeed clear that Martin-löf type theory is exactly the internal logic of a locally cartesian closed $(\infty,1)$ -category ? | |
| Jul 19, 2013 at 9:57 | history | answered | Urs Schreiber | CC BY-SA 3.0 |