+
+(******************* compatible equivalence relations **********************)
+
+nrecord compatible_equivalence_relation (A: setoid) : Type[1] ≝
+ { rel:> equivalence_relation A;
+ compatibility: ∀x,x':A. x=x' → rel x x'
+ }.
+
+ndefinition quotient: ∀A. compatible_equivalence_relation A → setoid.
+ #A; #R; @ A R;
+nqed.
+
+(******************* first omomorphism theorem for sets **********************)
+
+ndefinition eqrel_of_morphism:
+ ∀A,B. unary_morphism A B → compatible_equivalence_relation A.
+ #A; #B; #f; @
+ [ @ [ napply (λx,y. f x = f y) ] /2/;
+##| #x; #x'; #H; nwhd; alias symbol "prop1" = "prop1".
+napply (.= (†H)); // ]
+nqed.
+
+ndefinition canonical_proj: ∀A,R. unary_morphism A (quotient A R).
+ #A; #R; @
+ [ napply (λx.x) | #a; #a'; #H; napply (compatibility … R … H) ]
+nqed.
+
+ndefinition quotiented_mor:
+ ∀A,B.∀f:unary_morphism A B.
+ unary_morphism (quotient … (eqrel_of_morphism … f)) B.
+ #A; #B; #f; @ [ napply f ] //.
+nqed.
+
+nlemma first_omomorphism_theorem_functions1:
+ ∀A,B.∀f: unary_morphism A B.
+ ∀x. f x = quotiented_mor … (canonical_proj … (eqrel_of_morphism … f) x).
+//. nqed.
+
+alias symbol "eq" = "setoid eq".
+ndefinition surjective ≝
+ λA,B.λS: ext_powerclass A.λT: ext_powerclass B.λf:unary_morphism A B.
+ ∀y. y ∈ T → ∃x. x ∈ S ∧ f x = y.
+
+ndefinition injective ≝
+ λA,B.λS: ext_powerclass A.λf:unary_morphism A B.
+ ∀x,x'. x ∈ S → x' ∈ S → f x = f x' → x = x'.
+
+nlemma first_omomorphism_theorem_functions2:
+ ∀A,B.∀f: unary_morphism A B.
+ surjective … (Full_set ?) (Full_set ?) (canonical_proj ? (eqrel_of_morphism … f)).
+/3/. nqed.
+
+nlemma first_omomorphism_theorem_functions3:
+ ∀A,B.∀f: unary_morphism A B.
+ injective … (Full_set ?) (quotiented_mor … f).
+ #A; #B; #f; nwhd; #x; #x'; #Hx; #Hx'; #K; nassumption.
+nqed.
+
+nrecord isomorphism (A, B : setoid) (S: ext_powerclass A) (T: ext_powerclass B) : Type[0] ≝
+ { iso_f:> unary_morphism A B;
+ f_closed: ∀x. x ∈ S → iso_f x ∈ T;
+ f_sur: surjective … S T iso_f;
+ f_inj: injective … S iso_f
+ }.
+
+nlemma subseteq_intersection_l: ∀A.∀U,V,W:Ω^A.U ⊆ W ∨ V ⊆ W → U ∩ V ⊆ W.
+#A; #U; #V; #W; *; #H; #x; *; /2/.
+nqed.
+
+nlemma subseteq_union_l: ∀A.∀U,V,W:Ω^A.U ⊆ W → V ⊆ W → U ∪ V ⊆ W.
+#A; #U; #V; #W; #H; #H1; #x; *; /2/.
+nqed.
+
+nlemma subseteq_intersection_r: ∀A.∀U,V,W:Ω^A.W ⊆ U → W ⊆ V → W ⊆ U ∩ V.
+/3/. nqed.
+
+(*
+nrecord isomorphism (A, B : setoid) (S: qpowerclass A) (T: qpowerclass B) : CProp[0] ≝
+ { iso_f:> unary_morphism A B;
+ f_closed: ∀x. x ∈ pc A S → fun1 ?? iso_f x ∈ pc B T}.
+
+
+ncheck (λA:?.
+ λB:?.
+ λS:?.
+ λT:?.
+ λxxx:isomorphism A B S T.
+ match xxx
+ return λxxx:isomorphism A B S T.
+ ∀x: carr A.
+ ∀x_72: mem (carr A) (pc A S) x.
+ mem (carr B) (pc B T) (fun1 A B ((λ_.?) A B S T xxx) x)
+ with [ mk_isomorphism _ yyy ⇒ yyy ] ).
+
+ ;
+ }.