Homotopy Type Theory decidable setoid > history (Rev #4)

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