Homotopy Type Theory decidable preordered type > history (Rev #2)

Contents

Contents
Definition
See also

Definition

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

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

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

See also

category: not redirected to nlab yet

Revision on June 15, 2022 at 22:47:47 by Anonymous?. See the history of this page for a list of all contributions to it.