Author: David_Corfield Format: MarkdownItexAdded the HoTT version of disjunction.
<a href="https://ncatlab.org/nlab/revision/diff/disjunction/10">diff</a>, <a href="https://ncatlab.org/nlab/revision/disjunction/10">v10</a>, <a href="https://ncatlab.org/nlab/show/disjunction">current</a>
Author: Urs Format: MarkdownItexadded pointer to today's
* Landon D. C. Elkind, Richard Zach, _The Genealogy of $\vee$_ ([arXiv:2012.06072](https://arxiv.org/abs/2012.06072))
<a href="https://ncatlab.org/nlab/revision/diff/disjunction/11">diff</a>, <a href="https://ncatlab.org/nlab/revision/disjunction/11">v11</a>, <a href="https://ncatlab.org/nlab/show/disjunction">current</a>
added pointer to today’s
Landon D. C. Elkind, Richard Zach, The Genealogy of (arXiv:2012.06072)
Author: Madeleine Birchfield Format: MarkdownItexMoved the inductive definition of disjunctions in dependent type theory to its own section regarding disjunctions in dependent type theory, and added material regarding the definition of disjunctions which uses the type of propositions.
<a href="https://ncatlab.org/nlab/revision/diff/disjunction/17">diff</a>, <a href="https://ncatlab.org/nlab/revision/disjunction/17">v17</a>, <a href="https://ncatlab.org/nlab/show/disjunction">current</a>
Moved the inductive definition of disjunctions in dependent type theory to its own section regarding disjunctions in dependent type theory, and added material regarding the definition of disjunctions which uses the type of propositions.