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

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

Contents

Definition

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

Examples

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

See also

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