Homotopy Type Theory decidable subset > history (Rev #1)

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