Homotopy Type Theory excluded middle > history (Rev #2, changes)

Showing changes from revision #1 to #2: Added | ~~Removed~~ | ~~Chan~~ged

~~Definition~~

~~Excluded middle says that there is a term of the sum of a proposition~~

~~$P$~~ ~~and the type of functions~~ ~~$P \to \emptyset$~~ .

~~$\frac{P\ \mathrm{type} \quad p:\prod_{a:P} \prod_{b:P} a =_P b}{q:P + P \to \emptyset}$~~
~~In universes~~
~~Excluded middle is said to hold in a universe $\mathcal{U}$ if the universe comes with a dependent function~~
$p:\prod_{P:\mathcal{U}} \left(\prod_{a:\mathcal{T}_\mathcal{U}(P)} \prod_{b:\mathcal{T}_\mathcal{U}(P)} a =_{\mathcal{T}_\mathcal{U}(P)} b\right) \to \left(\mathcal{T}_\mathcal{U}(P) + \mathcal{T}_\mathcal{U}(P) \to \emptyset\right)$
~~See also~~

limited principle of omniscience

double negation

Whitehead's principle

Revision on June 14, 2022 at 04:37:39 by Anonymous?. See the history of this page for a list of all contributions to it.