Author: Ali Caglayan Format: MarkdownItexmoved types here from type theory page.
<a href="https://ncatlab.org/homotopytypetheory/revision/diff/empty/4">diff</a>, <a href="https://ncatlab.org/homotopytypetheory/revision/empty/4">v4</a>, <a href="https://ncatlab.org/homotopytypetheory/show/empty">current</a>