equal
deleted
inserted
replaced
21 refl_def "refl A r == r <= Sigma A (%x.A) & (ALL x: A. (x,x) : r)" |
21 refl_def "refl A r == r <= Sigma A (%x.A) & (ALL x: A. (x,x) : r)" |
22 sym_def "sym(r) == ALL x y. (x,y): r --> (y,x): r" |
22 sym_def "sym(r) == ALL x y. (x,y): r --> (y,x): r" |
23 equiv_def "equiv A r == refl A r & sym(r) & trans(r)" |
23 equiv_def "equiv A r == refl A r & sym(r) & trans(r)" |
24 quotient_def "A/r == UN x:A. {r^^{x}}" |
24 quotient_def "A/r == UN x:A. {r^^{x}}" |
25 congruent_def "congruent r b == ALL y z. (y,z):r --> b(y)=b(z)" |
25 congruent_def "congruent r b == ALL y z. (y,z):r --> b(y)=b(z)" |
26 congruent2_def "congruent2 r b == ALL y1 z1 y2 z2. \ |
26 congruent2_def "congruent2 r b == ALL y1 z1 y2 z2. |
27 \ (y1,z1):r --> (y2,z2):r --> b y1 y2 = b z1 z2" |
27 (y1,z1):r --> (y2,z2):r --> b y1 y2 = b z1 z2" |
28 end |
28 end |