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



Given a decidable setoid TT, a decidable existential quantifier on TT 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) \equiv 0) \times \left(\left(\prod_{t:T} P(t) = 0\right) \to \emptyset \right) \to (\exists x.P(x) \equiv 1)

See also

Revision on June 15, 2022 at 22:47:35 by Anonymous?. See the history of this page for a list of all contributions to it.