...

diff --git a/helm/software/matita/library/datatypes/categories.ma b/helm/software/matita/library/datatypes/categories.ma
index 6dac9b044bb537175b1f4dc33708356563836fbc..3a8a6c759a2268e623a6fdb248d7602d70aadc8d 100644 (file)
--- a/helm/software/matita/library/datatypes/categories.ma
+++ b/helm/software/matita/library/datatypes/categories.ma
@@ -88,13 +88,6 @@ notation ".= r" with precedence 50 for @{'trans $r}.
 interpretation "trans1" 'trans r = (trans1 _____ r).
 interpretation "trans" 'trans r = (trans _____ r).
 
-(*
-record unary_morphism0 (A,B: setoid) : Type0 ≝
- { fun_0:1> A → B;
-   prop_0: ∀a,a'. eq ? a a' → eq ? (fun_0 a) (fun_0 a')
- }.
-*)
-
 record unary_morphism (A,B: setoid1) : Type0 ≝
  { fun_1:1> A → B;
    prop_1: ∀a,a'. eq1 ? a a' → eq1 ? (fun_1 a) (fun_1 a')
@@ -117,7 +110,6 @@ notation "† c" with precedence 90 for @{'prop1 $c }.
 notation "l ‡ r" with precedence 90 for @{'prop $l $r }.
 notation "#" with precedence 90 for @{'refl}.
 interpretation "prop_1" 'prop1 c = (prop_1 _____ c).
-(* interpretation "prop_0" 'prop1 c = (prop_0 _____ c). *)
 interpretation "prop1" 'prop l r = (prop1 ________ l r).
 interpretation "prop" 'prop l r = (prop ________ l r).
 interpretation "refl1" 'refl = (refl1 ___).

diff --git a/helm/software/matita/library/logic/cprop_connectives.ma b/helm/software/matita/library/logic/cprop_connectives.ma
index c0bbdda18f3212715b49e5c8412cb7523c81e2ce..facda284891ed948ba1ed1e650e69c405fdd6b84 100644 (file)
--- a/helm/software/matita/library/logic/cprop_connectives.ma
+++ b/helm/software/matita/library/logic/cprop_connectives.ma
@@ -62,9 +62,17 @@ record Iff (A,B:CProp) : CProp ≝
  { if: A → B;
    fi: B → A
  }.
-
+ 
+record Iff1 (A,B:CProp) : CProp ≝
+ { if1: A → B;
+   fi1: B → A
+ }.
+ 
 interpretation "logical iff" 'iff x y = (Iff x y).
 
+notation "hvbox(a break ⇔ b)" right associative with precedence 25 for @{'iff1 $a $b}.
+interpretation "logical iff type1" 'iff1 x y = (Iff1 x y).
+
 inductive exT (A:Type) (P:A→CProp) : CProp ≝
   ex_introT: ∀w:A. P w → exT A P.