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

Definition

Given a type $T$ , a decidable universal quantifier is a function $\forall x.(-)(x):(T \to \mathbb{2}) \to \mathbb{2}$ with a term

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