Homotopy Type Theory decidable universal quantifier > history (Rev #2, changes)

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

Contents

Definition

Given a typeTTdecidable setoid , adecidable universal quantifierTT , is a functionx.()(x):(T𝟚)𝟚\forall x.(-)(x):(T \to \mathbb{2}) \to \mathbb{2}decidable universal quantifier on TT is a function x.()(x):(T𝟚)𝟚\forall x.(-)(x):(T \to \mathbb{2}) \to \mathbb{2} with a term

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

See also

Revision on April 28, 2022 at 04:04:29 by Anonymous?. See the history of this page for a list of all contributions to it.