Author: nLab edit announcer Format: MarkdownItexlink went to a comment instead of the top of the blog post
Anonymous
<a href="https://ncatlab.org/nlab/revision/diff/interval+type/10">diff</a>, <a href="https://ncatlab.org/nlab/revision/interval+type/10">v10</a>, <a href="https://ncatlab.org/nlab/show/interval+type">current</a>
link went to a comment instead of the top of the blog post
Author: nLab edit announcer Format: MarkdownItexAdded reference
* Carlo Angiuli, _Univalence implies function extensionality_ ([blog](http://homotopytypetheory.org/2011/12/05/hott-in-prose/), [pdf](http://hottheory.files.wordpress.com/2011/12/hott2.pdf))
Section 4 is the relevant part of the article
Anonymous
<a href="https://ncatlab.org/nlab/revision/diff/interval+type/12">diff</a>, <a href="https://ncatlab.org/nlab/revision/interval+type/12">v12</a>, <a href="https://ncatlab.org/nlab/show/interval+type">current</a>
Added reference
Carlo Angiuli, Univalence implies function extensionality (blog, pdf)
Author: nLab edit announcer Format: MarkdownItexexpanded bullet point on function extensionality into its own section with a proof of function extensionality from the judgmental computation rules of the interval type.
Anonymous
<a href="https://ncatlab.org/nlab/revision/diff/interval+type/15">diff</a>, <a href="https://ncatlab.org/nlab/revision/interval+type/15">v15</a>, <a href="https://ncatlab.org/nlab/show/interval+type">current</a>
expanded bullet point on function extensionality into its own section with a proof of function extensionality from the judgmental computation rules of the interval type.