(* *)
(**************************************************************************)
-include "o-concrete_spaces.ma".
-
-definition btop_carr: BTop → Type ≝ λo:BTop. carr (carrbt o).
+include "o-basic_topologies.ma".
+definition btop_carr: BTop → Type ≝ λo:BTop. carr1 (oa_P (carrbt o)).
coercion btop_carr.
-definition btop_carr': BTop → setoid ≝ λo:BTop. carrbt o.
+(*
+definition btop_carr': BTop → setoid1 ≝ λo:BTop. carrbt o.
coercion btop_carr'.
qed.
interpretation "ffintersects" 'fintersects U V = (fun1 ___ (ffintersects _) U V).
+*)
record formal_topology: Type ≝
{ bt:> BTop;
- converges: ∀U,V: Ω \sup bt. A ? (U ↓ V) = A ? U ∩ A ? V
+ converges: ∀U,V: bt. A ? (U ↓ V) = (A ? U ∧ A ? V)
}.
+(*
definition bt': formal_topology → basic_topology ≝ λo:formal_topology.bt o.
coercion bt'.
qed.
interpretation "ffintersects'" 'fintersects U V = (fun1 ___ (ffintersects' _) U V).
-
+*)
record formal_map (S,T: formal_topology) : Type ≝
{ cr:> continuous_relation_setoid S T;
C1: ∀b,c. extS ?? cr (b ↓ c) = ext ?? cr b ↓ ext ?? cr c;