include "datatypes/pairs.ma".
alias symbol "eq" = "setoid eq".
-
alias symbol "eq" = "setoid1 eq".
alias symbol "eq" = "setoid eq".
-alias symbol "eq" = "setoid eq".
-alias symbol "eq" = "setoid1 eq".
-alias symbol "eq" = "setoid eq".
-alias symbol "eq" = "setoid1 eq".
nrecord partition (A: setoid) : Type[1] ≝
{ support: setoid;
- indexes: qpowerclass support;
- class: unary_morphism1 (setoid1_of_setoid support) (qpowerclass_setoid A);
+ indexes: ext_powerclass support;
+ class: unary_morphism1 (setoid1_of_setoid support) (ext_powerclass_setoid A);
inhabited: ∀i. i ∈ indexes → class i ≬ class i;
disjoint: ∀i,j. i ∈ indexes → j ∈ indexes → class i ≬ class j → i = j;
covers: big_union support ? indexes (λx.class x) = full_set A
nlapply (f_sur ???? (fi nindex) y ?)
[ alias symbol "refl" = "refl".
alias symbol "prop1" = "prop11".
+alias symbol "prop2" = "prop21 mem".
napply (. #‡(†?));##[##2: napply Hni2 |##1: ##skip | nassumption]##]
*; #nindex2; *; #Hni21; #Hni22;
nletin xxx ≝ (plus (big_plus (minus n nindex) (λi.λ_.s (S (plus i nindex)))) nindex2);
|##5: napply le_S_S_to_le; nassumption
|##*: nassumption]##]
##| #x; #x'; nnormalize in ⊢ (? → ? → %); #Hx; #Hx'; #E;
- ncut(∀i1,i2,i1',i2'. i1 ∈ Nat_ (S n) → i1' ∈ Nat_ (S n) → i2 ∈ pc ? (Nat_ (s i1)) → i2' ∈ pc ? (Nat_ (s i1')) → eq_rel (carr A) (eq A) (iso_f ???? (fi i1) i2) (iso_f ???? (fi i1') i2') → i1=i1' ∧ i2=i2');
+ ncut(∀i1,i2,i1',i2'. i1 ∈ Nat_ (S n) → i1' ∈ Nat_ (S n) → i2 ∈ Nat_ (s i1) → i2' ∈ Nat_ (s i1') → eq_rel (carr A) (eq A) (fi i1 i2) (fi i1' i2') → i1=i1' ∧ i2=i2');
##[ #i1; #i2; #i1'; #i2'; #Hi1; #Hi1'; #Hi2; #Hi2'; #E;
nlapply(disjoint … P (f i1) (f i1') ???)
[##2,3: napply f_closed; nassumption
|##1: @ (fi i1 i2); @;
- ##[ napply f_closed; nassumption ##| napply (. E‡#);
+ ##[ napply f_closed; nassumption ##| alias symbol "refl" = "refl1".
+napply (. E‡#);
nwhd; napply f_closed; nassumption]##]
#E'; ncut(i1 = i1'); ##[ napply (f_inj … E'); nassumption; ##]
#E''; nrewrite < E''; @;
[ napply (quotient ? R)
| napply Full_set
| napply mk_unary_morphism1
- [ #a; napply mk_qpowerclass
+ [ #a; napply mk_ext_powerclass
[ napply {x | R x a}
| #x; #x'; #H; nnormalize; napply mk_iff; #K; nelim daemon]
##| #a; #a'; #H; napply conj; #x; nnormalize; #K [ nelim daemon | nelim daemon]##]