Timeline for Propositional vs Definitional extentionality in type theory
Current License: CC BY-SA 3.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Nov 28, 2017 at 22:22 | comment | added | Simon Henry | Ok, nice. I'll wait to see your thesis then. My version (arxiv.org/abs/1609.04622) is more categorical: it is a "weak model structure" on the category of "category with cofibrations together with a class of equivalences" ("pre-brown categories" in some sense) a bit like the work of Karol Szumilo but in practice a lot more similar to the one constructed by Peter and Chris. But I don't get a semi-model structure: it is "semi" on both side. But my motivation were very different: I was actually interested in constructing and comparing the model structures that these objects generates... | |
| Nov 28, 2017 at 22:13 | vote | accept | Simon Henry | ||
| Nov 28, 2017 at 19:47 | comment | added | Valery Isaev | Yes, Peter, Chris, and I (independently) work on similar questions with the same motivation, but with different approaches. I also have a construction of almost the same model structure (the difference is that it is a full model structure, but the type theory is slightly unusual, it's closer to the cubical TT). | |
| Nov 28, 2017 at 19:20 | comment | added | Simon Henry | That reference sound perfect, I'll look at it immediately. also What you are working sound interesting ! I assume you are familiar with it, but just in case: do you know the recent work (arxiv.org/abs/1610.00037) of Peter Lumsdaine and Chris Kapulkin which do something which sound a little bit like what you say. I also defined a very similar weak model structure in my own work essentially simultaneously, but we had different motivation and the one of Peter and Chris is a lot closer to syntaxe and type theory. | |
| Nov 28, 2017 at 19:05 | history | answered | Valery Isaev | CC BY-SA 3.0 |