-nrecord unary_morphism (A,B: setoid) : Type[0] ≝
- { fun1:1> A → B;
- prop1: ∀a,a'. a = a' → fun1 a = fun1 a'
- }.
+nrecord unary_morphism (A,B: setoid) : Type[0] ≝ {
+ fun1:1> A → B;
+ prop1: ∀a,a'. a = a' → fun1 a = fun1 a'
+}.
+
+notation > "B ⇒_0 C" right associative with precedence 72 for @{'umorph0 $B $C}.
+notation "hvbox(B break ⇒\sub 0 C)" right associative with precedence 72 for @{'umorph0 $B $C}.
+interpretation "unary morphism 0" 'umorph0 A B = (unary_morphism A B).