Homotopy Type Theory decidable existential quantifier > history (Rev #1)

Contents

Definition

Given a type TT, a decidable existential quantifier is a function x.()(x):(T𝟚)𝟚\exists x.(-)(x):(T \to \mathbb{2}) \to \mathbb{2} with a term

p: P:T𝟚( t:TP(t)=0)(x.P(x)=0)×(( t:TP(t)=0))(x.P(x)=1)p:\prod_{P:T \to \mathbb{2}} \left(\prod_{t:T} P(t) = 0\right) \to (\exists x.P(x) = 0) \times \left(\left(\prod_{t:T} P(t) = 0\right) \to \emptyset \right) \to (\exists x.P(x) = 1)

See also

Revision on April 27, 2022 at 16:19:47 by Anonymous?. See the history of this page for a list of all contributions to it.