Author: nLab edit announcer Format: MarkdownItexAdded a section about families of sets in dependent type theory
Anonymous
<a href="https://ncatlab.org/nlab/revision/diff/family+of+sets/5">diff</a>, <a href="https://ncatlab.org/nlab/revision/family+of+sets/5">v5</a>, <a href="https://ncatlab.org/nlab/show/family+of+sets">current</a>
Added a section about families of sets in dependent type theory
Author: nLab edit announcer Format: MarkdownItexadded link to family of subsets
Anonymous
<a href="https://ncatlab.org/nlab/revision/diff/family+of+sets/7">diff</a>, <a href="https://ncatlab.org/nlab/revision/family+of+sets/7">v7</a>, <a href="https://ncatlab.org/nlab/show/family+of+sets">current</a>
Author: Urs Format: MarkdownItexIn the second sentence, it has a preimage denoted "$p^*(k)$", which doesn't seem to typecheck. The usual notation would be "$p^{-1}\big(\{k\}\big)$".
The third sentence is a "let..."-clause which is missing its "then..." punchline.
<a href="https://ncatlab.org/nlab/revision/diff/family+of+sets/8">diff</a>, <a href="https://ncatlab.org/nlab/revision/family+of+sets/8">v8</a>, <a href="https://ncatlab.org/nlab/show/family+of+sets">current</a>
In the second sentence, it has a preimage denoted “$p^*(k)$”, which doesn’t seem to typecheck. The usual notation would be “$p^{-1}\big(\{k\}\big)$”.
The third sentence is a “let…”-clause which is missing its “then…” punchline.