-interpretation "prop1" 'prop1 c = (prop1 _____ c).
-interpretation "prop11" 'prop1 c = (prop11 _____ c).
-interpretation "prop12" 'prop1 c = (prop12 _____ c).
-interpretation "prop13" 'prop1 c = (prop13 _____ c).
-interpretation "prop2" 'prop2 l r = (prop2 ________ l r).
-interpretation "prop21" 'prop2 l r = (prop21 ________ l r).
-interpretation "prop22" 'prop2 l r = (prop22 ________ l r).
-interpretation "prop23" 'prop2 l r = (prop23 ________ l r).
-interpretation "refl" 'refl = (refl ___).
-interpretation "refl1" 'refl = (refl1 ___).
-interpretation "refl2" 'refl = (refl2 ___).
-interpretation "refl3" 'refl = (refl3 ___).
-
-definition unary_morphism2_of_unary_morphism1: ∀S,T.unary_morphism1 S T → unary_morphism2 S T.
+interpretation "prop1" 'prop1 c = (prop1 ????? c).
+interpretation "prop11" 'prop1 c = (prop11 ????? c).
+interpretation "prop12" 'prop1 c = (prop12 ????? c).
+interpretation "prop13" 'prop1 c = (prop13 ????? c).
+interpretation "prop2" 'prop2 l r = (prop2 ???????? l r).
+interpretation "prop21" 'prop2 l r = (prop21 ???????? l r).
+interpretation "prop22" 'prop2 l r = (prop22 ???????? l r).
+interpretation "prop23" 'prop2 l r = (prop23 ???????? l r).
+interpretation "refl" 'refl = (refl ???).
+interpretation "refl1" 'refl = (refl1 ???).
+interpretation "refl2" 'refl = (refl2 ???).
+interpretation "refl3" 'refl = (refl3 ???).
+
+notation > "A × term 74 B ⇒ term 19 C" non associative with precedence 72 for @{'binary_morphism0 $A $B $C}.
+notation > "A × term 74 B ⇒_1 term 19 C" non associative with precedence 72 for @{'binary_morphism1 $A $B $C}.
+notation > "A × term 74 B ⇒_2 term 19 C" non associative with precedence 72 for @{'binary_morphism2 $A $B $C}.
+notation > "A × term 74 B ⇒_3 term 19 C" non associative with precedence 72 for @{'binary_morphism3 $A $B $C}.
+notation > "B ⇒_1 C" right associative with precedence 72 for @{'arrows1_SET $B $C}.
+notation > "B ⇒_1. C" right associative with precedence 72 for @{'arrows1_SETlow $B $C}.
+notation > "B ⇒_2 C" right associative with precedence 72 for @{'arrows2_SET1 $B $C}.
+notation > "B ⇒_2. C" right associative with precedence 72 for @{'arrows2_SET1low $B $C}.
+
+notation "A × term 74 B ⇒ term 19 C" non associative with precedence 72 for @{'binary_morphism0 $A $B $C}.
+notation "A × term 74 B ⇒\sub 1 term 19 C" non associative with precedence 72 for @{'binary_morphism1 $A $B $C}.
+notation "A × term 74 B ⇒\sub 2 term 19 C" non associative with precedence 72 for @{'binary_morphism2 $A $B $C}.
+notation "A × term 74 B ⇒\sub 3 term 19 C" non associative with precedence 72 for @{'binary_morphism3 $A $B $C}.
+notation "B ⇒\sub 1 C" right associative with precedence 72 for @{'arrows1_SET $B $C}.
+notation "B ⇒\sub 2 C" right associative with precedence 72 for @{'arrows2_SET1 $B $C}.
+notation "B ⇒\sub 1. C" right associative with precedence 72 for @{'arrows1_SETlow $B $C}.
+notation "B ⇒\sub 2. C" right associative with precedence 72 for @{'arrows2_SET1low $B $C}.
+
+interpretation "'binary_morphism0" 'binary_morphism0 A B C = (binary_morphism A B C).
+interpretation "'arrows2_SET1 low" 'arrows2_SET1 A B = (unary_morphism2 A B).
+interpretation "'arrows2_SET1low" 'arrows2_SET1low A B = (unary_morphism2 A B).
+interpretation "'binary_morphism1" 'binary_morphism1 A B C = (binary_morphism1 A B C).
+interpretation "'binary_morphism2" 'binary_morphism2 A B C = (binary_morphism2 A B C).
+interpretation "'binary_morphism3" 'binary_morphism3 A B C = (binary_morphism3 A B C).
+interpretation "'arrows1_SET low" 'arrows1_SET A B = (unary_morphism1 A B).
+interpretation "'arrows1_SETlow" 'arrows1_SETlow A B = (unary_morphism1 A B).
+
+
+definition unary_morphism2_of_unary_morphism1:
+ ∀S,T:setoid1.unary_morphism1 S T → unary_morphism2 (setoid2_of_setoid1 S) T.