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.
I am working on prettifying the entry contractible type and noticed that where in Categorical semantics it says “Let … with sufficient structure…” we really eventually need to point to an entry that discusses this sufficient structure in detail.
In lack of a better idea, I named that entry presentation of homotopy type theory. Feel free to make better suggestions.
ah, we should just call it categorical semantics of homotopy type theory, right?
Okay, good point. That’s more specific. I changed the page name. Maybe I have time later today to add content.
Dang, I thought that the cache bug had been fixed.
1 to 5 of 5