include "basic_pairs.ma".
-(* full_subset e' una coercion che non mette piu' *)
+(* carr1 e' necessario perche' ci sega via la coercion per gli oggetti di REL!
+ (confondendola con la coercion per gli oggetti di SET *)
record concrete_space : Type1 ≝
{ bp:> BP;
- converges: ∀a: concr bp.∀U,V: form bp. a ⊩ U → a ⊩ V → a ⊩ (U ↓ V);
- all_covered: ∀x: concr bp. x ⊩ full_subset (form bp)
+ converges: ∀a: carr1 (concr bp).∀U,V: carr1 (form bp). a ⊩ U → a ⊩ V → a ⊩ (U ↓ V);
+ all_covered: ∀x: carr1 (concr bp). x ⊩ form bp
}.
record convergent_relation_pair (CS1,CS2: concrete_space) : Type1 ≝