definition A : ∀b:OBP. unary_morphism1 (Oform b) (Oform b).
intros; constructor 1;
- [ apply (λx.□_b (Ext⎽b x));
+ [ apply (λx.□⎽b (Ext⎽b x));
| intros; apply (†(†e));]
qed.
}.
interpretation "o-concrete space downarrow" 'downarrow x =
- (fun11 __ (Odownarrow _) x).
+ (fun11 ?? (Odownarrow ?) x).
definition Obinary_downarrow :
∀C:Oconcrete_space.binary_morphism1 (Oform C) (Oform C) (Oform C).
apply ((†e)‡(†e1));]
qed.
-interpretation "concrete_space binary ↓" 'fintersects a b = (fun21 _ _ _ (Obinary_downarrow _) a b).
+interpretation "concrete_space binary ↓" 'fintersects a b = (fun21 ? ? ? (Obinary_downarrow ?) a b).
record Oconvergent_relation_pair (CS1,CS2: Oconcrete_space) : Type2 ≝
{ Orp:> arrows2 ? CS1 CS2;