Homotopy Type Theory decidable setoid > history (Rev #8, changes)

Showing changes from revision #7 to #8: Added | Removed | Changed

Contents

Definition

A decidable setoid is a type TT with a function ()():T×T𝟚(-) \equiv (-):T \times T \to \mathbb{2} and terms

r: a:A(aa)=1r: \prod_{a:A} (a \equiv a) = 1
s: a:A b:A((ab)(ba))=1s: \prod_{a:A} \prod_{b:A} ((a \equiv b) \implies (b \equiv a)) = 1
t: a:A b:A c:A((ab)(bc)(ac))=1t: \prod_{a:A} \prod_{b:A} \prod_{c:A} ((a \equiv b) \wedge (b \equiv c) \implies (a \equiv c)) = 1

A decidable set is a decidable setoid where the canonical dependent functions

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

are equivalences.

See also

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