Author: nLab edit announcer Format: MarkdownItexstarting page on univalent types in simplicial type theory, i.e. Rezk types without the Segal condition
Anonymouse
<a href="https://ncatlab.org/nlab/revision/univalent+type/1">v1</a>, <a href="https://ncatlab.org/nlab/show/univalent+type">current</a>
starting page on univalent types in simplicial type theory, i.e. Rezk types without the Segal condition
Author: P Format: MarkdownItexthese are actually called "Rezk complete types" in the simplicial type theory literature. Added references for Rezk complete types and a definition involving the free isomorphism.
<a href="https://ncatlab.org/nlab/revision/diff/Rezk+complete+type/5">diff</a>, <a href="https://ncatlab.org/nlab/revision/Rezk+complete+type/5">v5</a>, <a href="https://ncatlab.org/nlab/show/Rezk+complete+type">current</a>
these are actually called “Rezk complete types” in the simplicial type theory literature. Added references for Rezk complete types and a definition involving the free isomorphism.