nrecord partition (A: setoid) : Type[1] ≝
{ support: setoid;
indexes: qpowerclass support;
class: unary_morphism1 (setoid1_of_setoid support) (qpowerclass_setoid A);
inhabited: ∀i. i ∈ indexes → class i ≬ class i;
nrecord partition (A: setoid) : Type[1] ≝
{ support: setoid;
indexes: qpowerclass support;
class: unary_morphism1 (setoid1_of_setoid support) (qpowerclass_setoid A);
inhabited: ∀i. i ∈ indexes → class i ≬ class i;