I have added to this entry missing cross-link to HoTT, by appending a half-sentence to the third paragraph (here).
]]>Added some material that was at boundary (type theory)
]]>Fixed arXiv link in previous edit (s/abs:/abs\//) and pasted doi link from the arXiv page
a distinct Anonymous
]]>adding reference
Anonymous
]]>edited first paragraph to explain that cubical type theories are not necessarily homotopy type theories, and added in a reference to the XTT paper as an example of a cubical type theory which is not a homotopy type theory.
Anonymous
]]>cubical type theory is certainly not a “homotopy type theory in which univalence is not just an axiom but a theorem”. There exist extensional cubical type theories such as XTT where UIP is a theorem, not an axiom.
]]>Added my thesis to the normalization links
]]>Thanks. I hadn’t seen we have appropriate other entries, such as normal form.
]]>I don’t think there is ambiguity in disambiguation. Made a start here: normalization.
]]>Ah, ’normalization’ is a redirect for normal variety. This is misleading the link at sequent calculus too.
What do people reckon is the best way to disambiguate?
]]>Added reference
Added some references to ABCFHL cartesian cubical type theory.
]]>Updated dead link. from http://www.cs.cmu.edu/~amoertbe/papers/cubicalagda.pdf to https://staff.math.su.se/anders.mortberg/papers/cubicalagda.pdf
Lasse Letager Hansen
]]>Fixed location of previous edit.
]]>Added reference to Bentzen’s “Naive cubical type theory”.
]]>update references
Evan Cavallo
]]>added pointer to
Ref to: Homotopy canonicity for cubical type theory
]]>@spitters This new one is still not equivalent to simplicial sets right?
]]>Adding Cavallo/Mortberg
]]>Recording the fact that Cartesian cubical sets are not equivalent to simplicial sets.
]]>hyperlinked author names, and added arxiv:
to before the arXiv identifiers
Added reference to “Parametric Cubical Type Theory” paper.
]]>Adding references for HITs, canonicity.
]]>