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.
Initial stub to record some references. Wanted by type theoretic model category
Is this talk also related?
Suggestions for better names:
Even cubical model category might do. Although it could be confused with the model structure on cubical sets.
I think by analogy to “simplicial model category”, the term “cubical model category” would be assumed to mean a model category enriched over cubical sets.
What about “univalent model category”? That’s reasonably short and hints at the key ingredient (and a raison-d’être). Otherwise, “univalence-induced” might do, but it is a cumbersome. I’ll ask Thierry and Christian for their opinions.
Re #5, yes, that’s very relevant, and I realized that the current assumptions on this page (type-theoretic model structure) are not general enough. In particular, once we have fibrant dependent products and fibrant univalent universes, then we should get a model structure worthy of the name. But then we might get a bit closer to type-theoretic model category, which AFAICS doen’t discuss univalent universes at the moment.
“univalent model category” seems a bit greedy since there could be other models of univalence in the future. What about something silly like “cubivalent model category”?
In fact there are already other models of univalence, such as Voevodsky’s very first model of simplicial sets and diagrams of such. So “univalent model category” won’t cut it.
Thanks. I’d like to change the name of this page now to something less conflicty and confusing, before the term starts to get used too much. I suggest “cubical-type model category” for now, does anyone have a better suggestion?
I think “cubical-type model category” is a reasonable improvement.
1 to 15 of 15