Library UniMath.Combinatorics.DecSet

Decidable sets.

Gianluca Amato, Marco Maggesi, Cosimo Perini Brogi 2019-2021

Require Import UniMath.Foundations.PartB.

Definition decSet: UU := ∑ (X: UU ), isdeceq X.

Definition make_decSet (X: UU) (i: isdeceq X): decSet := X ,, i.

Definition pr1decSet: decSet → UU := pr1.

Coercion pr1decSet : decSet >-> UU.

Definition decproperty (X: decSet) := pr2 X.