include "o-algebra.ma".
include "o-saturations.ma".
-record basic_topology: Type ≝
+record basic_topology: Type2 ≝
{ carrbt:> OA;
A: carrbt ⇒ carrbt;
J: carrbt ⇒ carrbt;
qed.
coercion hint.
-record continuous_relation (S,T: basic_topology) : Type ≝
+record continuous_relation (S,T: basic_topology) : Type2 ≝
{ cont_rel:> arrows2 OA S T;
(* reduces uses eq1, saturated uses eq!!! *)
reduced: ∀U. U = J ? U → cont_rel U = J ? (cont_rel U);