include "formal_topology/basic_pairs_to_o-basic_pairs.ma".
include "formal_topology/apply_functor.ma".
-
+(*
definition rOBP ≝ Apply (category2_of_category1 BP) OBP BP_to_OBP.
include "formal_topology/o-basic_pairs_to_o-basic_topologies.ma".
| intros; apply (#‡e); ]
qed.
-notation < "F x" left associative with precedence 60 for @{'map_arrows $F $x}.
+notation < "F x" left associative with precedence 65 for @{'map_arrows $F $x}.
interpretation "map arrows 2" 'map_arrows F x = (fun12 ? ? (map_arrows2 ? ? F ? ?) x).
definition preserve_sup : ∀S,T.∀ f:Ω^S ⇒_1 Ω^T. CProp[1].
*)
-*)
\ No newline at end of file
+*)
+*)