Timeline for What kind of category is generated by Cubical type theory?
Current License: CC BY-SA 4.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 30, 2018 at 13:35 | history | edited | Simon Henry | CC BY-SA 4.0 |
added 3 characters in body
|
| May 30, 2018 at 13:34 | comment | added | Simon Henry | Well... maybe by "I'm not making any claim", I mostly meant "I think it is a terminology question and I don't care that much about this terminology". but of course you are absolutely right (and I've edited). | |
| May 30, 2018 at 13:28 | history | edited | Simon Henry | CC BY-SA 4.0 |
added 105 characters in body
|
| May 29, 2018 at 21:42 | comment | added | Mike Shulman | Well, you wrote "when one says ... it is a statement that compare a 'homotopy category'..." which seems to be making a claim that the informal statement always does refer to the homotopy-category-level version. | |
| May 29, 2018 at 20:56 | comment | added | Simon Henry | Of course, I entierely agree with you that an equivalence of $(\infty,1)$-category is preferable if you can get it. but the equivalence of homotopy categories already give you most of what you want. Regarding what statement between the equivalence of $(\infty,1)$-category and the equivalence of homotopy category is the closest to the informal claim that "some kind of type theory is the internal language of some kind of categories" I guess that's more of a philosophical question on which I'm not making any claim. | |
| May 29, 2018 at 17:57 | comment | added | Mike Shulman | The latter, for instance, is what Kapulkin and Szumilo obtain in the merely left-exact case in arxiv.org/abs/1709.09519, presenting these $(\infty,1)$-categories by fibration categories. | |
| May 29, 2018 at 17:56 | comment | added | Mike Shulman | I'm having trouble parsing the paragraph starting "Like, when one says". Are you saying that the internal language conjecture asserts an equivalence between the homotopy category of the category of contextual categories and the homotopy category of the category of lccc $(\infty,1)$-categories? If so, I suppose that's one way to state it, although I think most people would prefer an equivalence between the $(\infty,1)$-category of contextual categories and the $(\infty,1)$-category of lccc $(\infty,1)$-categories. | |
| May 29, 2018 at 16:03 | history | edited | Simon Henry | CC BY-SA 4.0 |
deleted 4 characters in body
|
| May 29, 2018 at 15:48 | history | answered | Simon Henry | CC BY-SA 4.0 |