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

Showing changes from revision #2 to #3: Added | ~~Removed~~ | ~~Chan~~ged

Contents

Contents
Definition
See also

Definition

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

r: \prod_{a:A} (a \equiv a) = 1

s: \prod_{a:A} \prod_{b:A} ((a \equiv b) \implies (b \equiv a)) = 1

t: \prod_{a:A} \prod_{b:A} \prod_{c:A} ((a \equiv b) \wedge (b \equiv c) \implies (a \equiv c)) = 1

See also

decidable preordered type

Revision on April 28, 2022 at 02:28:56 by Anonymous?. See the history of this page for a list of all contributions to it.