Homotopy Type Theory decidable set > history (Rev #4, changes)

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

Contents

Definition

A decidable set is a decidable setoid (T,()():T×T𝟚)(T, (-)\equiv(-): T \times T \to \mathbb{2}) where the canonical dependent functions

a:T,b:Tidtoequiv(a,b):(a=b)((ab)=1)a:T, b:T \vdash idtoequiv(a, b):(a = b) \to ((a \equiv b) = 1)

are equivalences.

See also

Revision on June 18, 2022 at 21:52:50 by Anonymous?. See the history of this page for a list of all contributions to it.