Author: maxsnew Format: MarkdownItexAdded a reference to Seely's 2-categorical analysis of eta expansion.
<a href="https://ncatlab.org/nlab/revision/diff/eta-conversion/10">diff</a>, <a href="https://ncatlab.org/nlab/revision/eta-conversion/10">v10</a>, <a href="https://ncatlab.org/nlab/show/eta-conversion">current</a>
Added a reference to Seely’s 2-categorical analysis of eta expansion.
Author: nLab edit announcer Format: MarkdownItexextensional type theory -> set-level type theory
identity types are extensional -> identity types are valued in propositions
Anonymous
<a href="https://ncatlab.org/nlab/revision/diff/eta-conversion/13">diff</a>, <a href="https://ncatlab.org/nlab/revision/eta-conversion/13">v13</a>, <a href="https://ncatlab.org/nlab/show/eta-conversion">current</a>
extensional type theory -> set-level type theory
identity types are extensional -> identity types are valued in propositions