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;
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;