Homotopy Type Theory decidable preordered type > history (changes)

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

Contents

Definition

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

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

See also

Last revised on June 18, 2022 at 21:50:39. See the history of this page for a list of all contributions to it.