Homotopy Type Theory double negation > history (Rev #3, changes)

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

Definition

< double negation

Double negation says that given a proposition

PP there is a function in the function type ((P))P((P \to \emptyset) \to \emptyset) \to P.

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 \to \emptyset) \to \emptyset) \to P}

In universes

Double negation 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) \to \emptyset) \to \emptyset) \to \mathcal{T}_\mathcal{U}(P)\right)

See also

  • sharp?, flat?, shape

  • unity of opposites?

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