include "o-algebra.ma".
include "o-saturations.ma".
-record Obasic_topology: Type2 ≝
- { Ocarrbt:> OA;
- oA: Ocarrbt ⇒ Ocarrbt;
- oJ: Ocarrbt ⇒ Ocarrbt;
- oA_is_saturation: is_o_saturation ? oA;
- oJ_is_reduction: is_o_reduction ? oJ;
- Ocompatibility: ∀U,V. (oA U >< oJ V) = (U >< oJ V)
+record Obasic_topology: Type2 ≝ {
+ Ocarrbt:> OA;
+ oA: Ocarrbt ⇒_2 Ocarrbt; oJ: Ocarrbt ⇒_2 Ocarrbt;
+ oA_is_saturation: is_o_saturation ? oA; oJ_is_reduction: is_o_reduction ? oJ;
+ Ocompatibility: ∀U,V. (oA U >< oJ V) =_1 (U >< oJ V)
}.
-record Ocontinuous_relation (S,T: Obasic_topology) : Type2 ≝
- { Ocont_rel:> arrows2 OA S T;
- (* reduces uses eq1, saturated uses eq!!! *)
- Oreduced: ∀U. U = oJ ? U → Ocont_rel U = oJ ? (Ocont_rel U);
- Osaturated: ∀U. U = oA ? U → Ocont_rel⎻* U = oA ? (Ocont_rel⎻* U)
+record Ocontinuous_relation (S,T: Obasic_topology) : Type2 ≝ {
+ Ocont_rel:> arrows2 OA S T;
+ Oreduced: ∀U:S. U = oJ ? U → Ocont_rel U =_1 oJ ? (Ocont_rel U);
+ Osaturated: ∀U:S. U = oA ? U → Ocont_rel⎻* U =_1 oA ? (Ocont_rel⎻* U)
}.
definition Ocontinuous_relation_setoid: Obasic_topology → Obasic_topology → setoid2.
change in e1 with (b⎻* ∘ oA o2 = b'⎻* ∘ oA o2);
apply (.= e‡#);
intro x;
- change with (eq1 ? (b⎻* (a'⎻* (oA o1 x))) (b'⎻*(a'⎻* (oA o1 x))));
+ change with (b⎻* (a'⎻* (oA o1 x)) =_1 b'⎻*(a'⎻* (oA o1 x)));
apply (.= †(Osaturated o1 o2 a' (oA o1 x) ?)); [
apply ((o_saturation_idempotent ?? (oA_is_saturation o1) x)^-1);]
apply (.= (e1 (a'⎻* (oA o1 x))));
- change with (eq1 ? (b'⎻* (oA o2 (a'⎻* (oA o1 x)))) (b'⎻*(a'⎻* (oA o1 x))));
+ change with (b'⎻* (oA o2 (a'⎻* (oA o1 x))) =_1 b'⎻*(a'⎻* (oA o1 x)));
apply (.= †(Osaturated o1 o2 a' (oA o1 x):?)^-1); [
apply ((o_saturation_idempotent ?? (oA_is_saturation o1) x)^-1);]
apply rule #;]