Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
added to the references-section of the stub type-theoretic model category pointers to André Joyal’s slides on “typoses” (he is currently speaking about that again at CRM in Barcelona).
(maybe that entry should be renamed to “categorical semantics for homotopy type theory” or the like, but I won’t further play with it for the time being).
I am also pointing to Mike’s article and to his course notes. I will maybe ask André later, but I am a bit confused about (was already in Halifax) how he presents his typoses, without mentioning of at least very similar categorical semantics that has been discussed before. Maybe I am missing some sociological subtleties here.
Link type-theoretic model cateory is a typo.
I have edited the stub entry type-theoretic model category a bit: added some actual content to the Idea-section and moved what used to be there into the (mostly empty) Definition-section.
Mainly I added more specific pointers to where Mike defines this. In particular previously the entry seemed to point ot the wrong article.
I also made some slight corresponding edits at locally cartesian closed (infinity,1)-category and at relation between type theory and category theory, just editorial edits, trying to bring out the point more clearly (which seems to still not have penetrated too far into the community…)
Once again I hit the weird bug that the rendered page wasn’t updated after this edit until I made another trivial edit.
The connection with (algebraic?) model structures on constructive cubical models is missing. I don’t have the time to chase references now, but maybe someone knows this by heard.
I don’t know that connection. What I know of the constructive cubical models has a rather different flavor; but I’m certainly not up to date on all the most recent cubical developments.
Christian spoke about this in Bonn for example video. I don’t know whether there is a write up. There was a discussion on the HoTT list after, IIRC.
I was thinking of this discussion that the cartesian cubical model is an elementary oo-topos, but not equivalent to oo-groupoids.
Make a reference to type theoretic model structure, itself TDB.
Why have you removed the hyphen from ’type-theoretic’? This is requesting that a new page be set up.
David, I don’t think I removed the hyphen anywhere? For now I changed the name of type-theoretic model structure and made sure both pages had redirects for the non-hyphen versions.
I meant the link you have in #11. That was wanting a new page, but now you’ve put in the redirect it’s fine.
Or did I get mixed up with type-theoretic model category/type-theoretic model structure? Anyway, there’s now consistent naming.
Re #10 I don’t think that has anything to do with the model-category-theoretic conditions, does it?
What is going to be at type-theoretic model structure? It seems a terrible idea if a “type-theoretic model category” is not the same as a category equipped with a “type-theoretic model structure”.
Re #16 yes, that problem did cross my mind :)
It’s going to be about Christian’s model structures built using gluing. We used to call these “Sattler model structures” but Christian objected, so for moment they go by type-theoretic model structure. But as you point out, that’s not ideal. I don’t know a good solution, though.
Is that the kind of “gluing” coming from the “glue types” used for cubical univalence, not the standard term Artin gluing that’s also been used to build models of type theory? (-:O Maybe if we finally find a good name for those “glue types” that doesn’t conflict with established terminology, it would give us a good name for these model structures. Or vice versa.
1 to 20 of 20