Almost done (up to definition of category).

[helm.git] / helm / software / matita / nlibrary / sets / sets.ma

diff --git a/helm/software/matita/nlibrary/sets/sets.ma b/helm/software/matita/nlibrary/sets/sets.ma
index 0e2dd418d3c19ef4e00d02e02c8ed15c79175734..113654ad330de847908ae68b3fcf65faaf9c3033 100644 (file)
--- a/helm/software/matita/nlibrary/sets/sets.ma
+++ b/helm/software/matita/nlibrary/sets/sets.ma
@@ -323,6 +323,7 @@ nlemma first_omomorphism_theorem_functions1:
  #A; #B; #f; #x; napply refl;
 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.