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.
have cross-linked with semi-simplicial object
If you have the energy to edit, please do.
Reorganization of the page: - clarify the difference between the “iterated dependent” (or “indexed”) presentation of semi-simplicial types - clarify the contributions of Voevodsky and myself in term of formalization - move historical contents not related to semi-simplicial types in a specific section - add more recent bibliography
Thanks. I see, I’ll step back, I see that we were cross-editing just now.
I have made the pointer to your and Voevodksy’s note an actual linked reference. Hope this works for you. But if your aim is visibility and claim of priority, its better to have an actual reference item than just in-line commentary.
the family/fibration equivalence looks so central that I feel that there should be a page about it.
Please feel invited to create a dedicated page!
But we should have at least some version of the statement scattered around in some form or other. Have you seen this here:
?
Even so, this might want to be on a stand-alone page, for ease of linking to it and for inviting expanding and referencing it.
Thanks! Looks good.
I made some more of the in-line references into anchored pointers to the list of references.
Also fixed this glitch:
Vladimir Voevodsky proposed Homotopy Type Theory (HTT),
to
Vladimir Voevodsky proposed Homotopy Type System (HTS)
but this does not seem any more specific to categorical semantics
Just to highlight that the paragraph at dependent type – Relation to families of elements does not consider any semantics at all, but stays entirely inside the type theory.
But if you feel like writing more about this issue, either there or elsewhere, it will be most welcome!
1 to 16 of 16