-nrecord unary_morphism1 (A,B: setoid1) : Type[1] ≝
- { fun11:1> A → B;
- prop11: ∀a,a'. eq1 ? a a' → eq1 ? (fun11 a) (fun11 a')
- }.
-
+nrecord unary_morphism1 (A,B: setoid1) : Type[1] ≝ {
+ fun11:1> A → B;
+ prop11: ∀a,a'. eq1 ? a a' → eq1 ? (fun11 a) (fun11 a')
+}.
+
+notation > "B ⇒_1 C" right associative with precedence 72 for @{'umorph1 $B $C}.
+notation "hvbox(B break ⇒\sub 1 C)" right associative with precedence 72 for @{'umorph1 $B $C}.
+interpretation "unary morphism 1" 'umorph1 A B = (unary_morphism1 A B).
+
+notation "┼_1 c" with precedence 89 for @{'prop1_x1 $c }.