update in binaries for λδ

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

diff --git a/helm/software/matita/nlibrary/sets/setoids.ma b/helm/software/matita/nlibrary/sets/setoids.ma
index f633470edacea39fb3b81081f0172fea903da06f..e40dad6f6d20e4e3a1f7624b6f28b5d6056a6ef3 100644 (file)
--- a/helm/software/matita/nlibrary/sets/setoids.ma
+++ b/helm/software/matita/nlibrary/sets/setoids.ma
@@ -21,7 +21,21 @@ nrecord setoid : Type[1] ≝ {
   eq0: equivalence_relation carr
 }.
 
+(* activate non uniform coercions on: Type → setoid *)
+unification hint 0 ≔ R : setoid;
+   MR ≟ carr R, 
+   lock ≟ mk_lock1 Type[0] MR setoid R 
+(* ---------------------------------------- *) ⊢ 
+   setoid ≡ force1 ? MR lock.
+
+notation < "[\setoid\ensp\of term 19 x]" non associative with precedence 90 for @{'mk_setoid $x}.
+interpretation "mk_setoid" 'mk_setoid x = (mk_setoid x ?).
+
 interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq0 t) x y).
+(* single = is for the abstract equality of setoids, == is for concrete 
+   equalities (that may be lifted to the setoid level when needed *)
+notation < "hvbox(a break mpadded width -50% (=)= b)" non associative with precedence 45 for @{ 'eq_low $a $b }.
+notation > "a == b" non associative with precedence 45 for @{ 'eq_low $a $b }.
 
 notation > "hvbox(a break =_0 b)" non associative with precedence 45
 for @{ eq_rel ? (eq0 ?) $a $b }.
@@ -73,7 +87,7 @@ nlemma unary_morph_eq: ∀A,B.∀f,g:A ⇒_0 B. (∀x. f x = g x) → f = g.
 nlemma mk_binary_morphism:
  ∀A,B,C: setoid. ∀f: A → B → C. (∀a,a',b,b'. a=a' → b=b' → f a b = f a' b') →
   A ⇒_0 (unary_morph_setoid B C).
- #A; #B; #C; #f; #H; @ [ #x; @ (f x) ] #a; #a'; #Ha [##2: napply unary_morph_eq; #y]
+ #A; #B; #C; #f; #H; @; ##[ #x; @ (f x) ] #a; #a'; #Ha [##2: napply unary_morph_eq; #y]
  /2/.
 nqed.
 
@@ -89,16 +103,19 @@ ndefinition comp_unary_morphisms:
 nqed.
 
 unification hint 0 ≔ o1,o2,o3:setoid,f:o2 ⇒_0 o3,g:o1 ⇒_0 o2;
-   R ≟ mk_unary_morphism ?? (composition … f g)
-        (prop1 ?? (comp_unary_morphisms o1 o2 o3 f g))
+   R ≟ mk_unary_morphism o1 o3 
+        (composition ??? (fun1 o2 o3 f) (fun1 o1 o2 g))
+        (prop1 o1 o3 (comp_unary_morphisms o1 o2 o3 f g))
  (* -------------------------------------------------------------------- *) ⊢
-                              fun1 ?? R ≡ (composition … f g).
+    fun1 o1 o3 R ≡ composition ??? (fun1 o2 o3 f) (fun1 o1 o2 g).
 
-ndefinition comp_binary_morphisms:
- ∀o1,o2,o3.
-  (unary_morph_setoid o2 o3) ⇒_0 
-   (unary_morph_setoid (unary_morph_setoid o1 o2) (unary_morph_setoid o1 o3)).
+ndefinition comp_binary_morphisms: 
+  ∀o1,o2,o3.(o2 ⇒_0 o3) ⇒_0 ((o1 ⇒_0 o2) ⇒_0 (o1 ⇒_0 o3)).
 #o1; #o2; #o3; napply mk_binary_morphism
- [ #f; #g; napply (comp_unary_morphisms … f g) (*CSC: why not ∘?*)
+ [ #f; #g; napply (comp_unary_morphisms ??? f g) 
+         (* CSC: why not ∘? 
+            GARES: because the coercion to FunClass is not triggered if there
+                   are no "extra" arguments. We could fix that in the refiner
+         *)
  | #a; #a'; #b; #b'; #ea; #eb; #x; #x'; #Hx; nnormalize; /3/ ]
 nqed.