interpretation "setoid2 symmetry" 'invert r = (sym2 ???? r).
interpretation "setoid1 symmetry" 'invert r = (sym1 ???? r).
interpretation "setoid symmetry" 'invert r = (sym ???? r).
interpretation "setoid2 symmetry" 'invert r = (sym2 ???? r).
interpretation "setoid1 symmetry" 'invert r = (sym1 ???? r).
interpretation "setoid symmetry" 'invert r = (sym ???? r).
interpretation "trans3" 'trans r = (trans3 ????? r).
interpretation "trans2" 'trans r = (trans2 ????? r).
interpretation "trans1" 'trans r = (trans1 ????? r).
interpretation "trans3" 'trans r = (trans3 ????? r).
interpretation "trans2" 'trans r = (trans2 ????? r).
interpretation "trans1" 'trans r = (trans1 ????? r).
∀o1,o2,o3.∀f1:arrows2 ? o1 o2.∀f2:arrows2 ? o2 o3.
map_arrows2 ?? (f2 ∘ f1) = map_arrows2 ?? f2 ∘ map_arrows2 ?? f1}.
∀o1,o2,o3.∀f1:arrows2 ? o1 o2.∀f2:arrows2 ? o2 o3.
map_arrows2 ?? (f2 ∘ f1) = map_arrows2 ?? f2 ∘ map_arrows2 ?? f1}.
-notation > "F⎽⇒ x" left associative with precedence 60 for @{'map_arrows2 $F $x}.
-notation "F\sub⇒ x" left associative with precedence 60 for @{'map_arrows2 $F $x}.
+notation > "F⎽⇒ x" left associative with precedence 65 for @{'map_arrows2 $F $x}.
+notation "F\sub⇒ x" left associative with precedence 65 for @{'map_arrows2 $F $x}.
interpretation "map_arrows2" 'map_arrows2 F x = (fun12 ?? (map_arrows2 ?? F ??) x).
definition functor2_setoid: category2 → category2 → setoid3.
interpretation "map_arrows2" 'map_arrows2 F x = (fun12 ?? (map_arrows2 ?? F ??) x).
definition functor2_setoid: category2 → category2 → setoid3.