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

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

Contents

Definition

A decidable set $(T, (-)\equiv(-): T \times T \to \mathbb{2})$ has decidable subsets if the function type $T \to \mathbb{2}$ is a decidable set.

Examples

• All finite types are decidable sets and have decidable subsets.

See also

• booleans
• decidable set