Author: nLab edit announcer Format: MarkdownItexAdded a section on the axiom of fullness in dependent type theory
Anonymouse
<a href="https://ncatlab.org/nlab/revision/diff/subset+collection/7">diff</a>, <a href="https://ncatlab.org/nlab/revision/subset+collection/7">v7</a>, <a href="https://ncatlab.org/nlab/show/subset+collection">current</a>
Added a section on the axiom of fullness in dependent type theory
Author: nLab edit announcer Format: MarkdownItexAdded the fact that, given function sets, fullness is equivalent to having sets of inhabited subsets in the set theory.
Anonymouse
<a href="https://ncatlab.org/nlab/revision/diff/subset+collection/8">diff</a>, <a href="https://ncatlab.org/nlab/revision/subset+collection/8">v8</a>, <a href="https://ncatlab.org/nlab/show/subset+collection">current</a>
Added the fact that, given function sets, fullness is equivalent to having sets of inhabited subsets in the set theory.