alias symbol "eq" = "setoid1 eq".
(* Qui, per fare le cose per bene, ci serve la nozione di funtore categorico *)
-definition o_basic_topology_of_o_basic_pair: OBP → BTop.
+definition o_basic_topology_of_o_basic_pair: OBP → OBTop.
intro t;
constructor 1;
[ apply (Oform t);
definition o_continuous_relation_of_o_relation_pair:
∀BP1,BP2.arrows2 OBP BP1 BP2 →
- arrows2 BTop (o_basic_topology_of_o_basic_pair BP1) (o_basic_topology_of_o_basic_pair BP2).
+ arrows2 OBTop (o_basic_topology_of_o_basic_pair BP1) (o_basic_topology_of_o_basic_pair BP2).
intros (BP1 BP2 t);
constructor 1;
[ apply (t \sub \f);
qed.
-definition OR : carr3 (arrows3 CAT2 OBP BTop).
+definition OR : carr3 (arrows3 CAT2 OBP OBTop).
constructor 1;
[ apply o_basic_topology_of_o_basic_pair;
| intros; constructor 1;
[ apply o_continuous_relation_of_o_relation_pair;
| apply hide;
intros; whd; unfold o_continuous_relation_of_o_relation_pair; simplify;;
- change with ((a \sub \f ⎻* ∘ A (o_basic_topology_of_o_basic_pair S)) =
- (a' \sub \f ⎻*∘A (o_basic_topology_of_o_basic_pair S)));
+ change with ((a \sub \f ⎻* ∘ oA (o_basic_topology_of_o_basic_pair S)) =
+ (a' \sub \f ⎻*∘ oA (o_basic_topology_of_o_basic_pair S)));
whd in e; cases e; clear e e2 e3 e4;
change in ⊢ (? ? ? (? ? ? ? ? % ?) ?) with ((⊩\sub S)⎻* ∘ (⊩\sub S)⎻);
apply (.= (comp_assoc2 ? ???? ?? a\sub\f⎻* ));
change in ⊢ (? ? ? (? ? ? ? ? ? %) ?) with (a'\sub\f⎻* ∘ (⊩\sub S)⎻* );
apply (.= (comp_assoc2 ? ???? ?? a'\sub\f⎻* )^-1);
apply refl2;]
-| intros 2 (o a); apply rule #;
+| intros 2 (o a); apply refl1;
| intros 6; apply refl1;]
qed.