Homotopy Type Theory excluded middle > history (changes)

Showing changes from revision #1 to #2: Added | Removed | Changed


< excluded middle

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

PP and the type of functions PP \to \emptyset.

Ptypep: a:P b:Pa= Pbq:P+P\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: P:𝒰( a:𝒯 𝒰(P) b:𝒯 𝒰(P)a= 𝒯 𝒰(P)b)(𝒯 𝒰(P)+𝒯 𝒰(P))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

Last revised on June 14, 2022 at 00:37:39. See the history of this page for a list of all contributions to it.