Timeline for Nontrivial interpretation of dependent type theory in the category of chain complexes
Current License: CC BY-SA 4.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 27, 2020 at 0:56 | comment | added | Zhen Lin | I suppose if you omit $\Pi$ and $\Sigma$ and $0$ and $+$ you may have a model, yes. But that’s not a very expressive fragment of type theory. | |
| Aug 27, 2020 at 0:31 | comment | added | Yuta | By "Martin Löf type theory with identity types", I was thinking of the fragment without Π and Σ. Then by Thm 3.1. of arxiv.org/pdf/0709.0248.pdf, I think finitely completeness and weak factorization system is enough to model Martin Löf type theory with identity types. Or isn't the stability condition satisfied? | |
| Aug 26, 2020 at 22:11 | comment | added | Zhen Lin | That is incorrect, or at least very imprecise. You need a lot more than just a model structure to interpret dependent type theory. For instance you need a locally cartesian closed category, or something very close, to interpret $\Pi$-types. | |
| Aug 26, 2020 at 21:19 | comment | added | Yuta | Could you please make it precise? I think model categories can interpret Martin Löf type theory with identity types. (By "dependent type theory", I meant Martin Löf type theory with identity types.) Is my understanding correct? | |
| Aug 26, 2020 at 13:50 | review | Close votes | |||
| Sep 16, 2020 at 3:09 | |||||
| Aug 26, 2020 at 9:50 | comment | added | Zhen Lin | I think you have confused different usages of the word “model” here. | |
| Aug 26, 2020 at 9:42 | review | First posts | |||
| Aug 26, 2020 at 10:49 | |||||
| Aug 26, 2020 at 9:39 | history | asked | Yuta | CC BY-SA 4.0 |