+ intros; split; intro; unfold minus_star_image; simplify; intros;
+ [ cut (ext ?? a a1 ⊆ A ? X); [2: intros 2; apply (H1 a2); cases f1; assumption;]
+ lapply (if ?? (A_is_saturation ???) Hcut); clear Hcut;
+ cut (A ? (ext ?? a' a1) ⊆ A ? X); [2: apply (. (H ?)‡#); assumption]
+ lapply (fi ?? (A_is_saturation ???) Hcut);
+ apply (Hletin1 x); change with (x ∈ ext ?? a' a1); split; simplify;
+ [ apply I | assumption ]
+ | cut (ext ?? a' a1 ⊆ A ? X); [2: intros 2; apply (H1 a2); cases f1; assumption;]
+ lapply (if ?? (A_is_saturation ???) Hcut); clear Hcut;
+ cut (A ? (ext ?? a a1) ⊆ A ? X); [2: apply (. (H ?)\sup -1‡#); assumption]
+ lapply (fi ?? (A_is_saturation ???) Hcut);
+ apply (Hletin1 x); change with (x ∈ ext ?? a a1); split; simplify;
+ [ apply I | assumption ]]
+qed.*)
+
+lemma continuous_relation_eq_inv':
+ ∀o1,o2.∀a,a': continuous_relation_setoid o1 o2.
+ (∀X.a⎻* (A o1 X) = a'⎻* (A o1 X)) → a=a'.
+ intros 6;
+ cut (∀a,a': continuous_relation_setoid o1 o2.
+ (∀X.a⎻* (A o1 X) = a'⎻* (A o1 X)) →
+ ∀V:o2. A ? (ext ?? a' V) ⊆ A ? (ext ?? a V));
+ [2: clear b f a' a; intros;
+ lapply depth=0 (λV.saturation_expansive ??? (extS ?? a V)); [2: apply A_is_saturation;|skip]
+ (* fundamental adjunction here! to be taken out *)
+ cut (∀V:Ω^o2.V ⊆ a⎻* (A ? (extS ?? a V)));
+ [2: intro; intros 2; unfold minus_star_image; simplify; intros;
+ apply (Hletin V1 x); whd; split; [ exact I | exists; [apply a1] split; assumption]]
+ clear Hletin;
+ cut (∀V:Ω^o2.V ⊆ a'⎻* (A ? (extS ?? a V)));
+ [2: intro; apply (. #‡(f ?)^-1); apply Hcut] clear f Hcut;
+ (* second half of the fundamental adjunction here! to be taken out too *)
+ intro; lapply (Hcut1 {(V)}); clear Hcut1;
+ unfold minus_star_image in Hletin; unfold singleton in Hletin; simplify in Hletin;
+ whd in Hletin; whd in Hletin:(?→?→%); simplify in Hletin;
+ apply (if ?? (A_is_saturation ???));
+ intros 2 (x H); lapply (Hletin V ? x ?);
+ [ apply refl | unfold foo; apply H; ]
+ change with (x ∈ A ? (ext ?? a V));
+ apply (. #‡(†(extS_singleton ????)^-1));
+ assumption;]
+ split; apply Hcut; [2: assumption | intro; apply sym1; apply f]
+qed.
+
+definition continuous_relation_comp:
+ ∀o1,o2,o3.
+ continuous_relation_setoid o1 o2 →
+ continuous_relation_setoid o2 o3 →
+ continuous_relation_setoid o1 o3.
+ intros (o1 o2 o3 r s); constructor 1;
+ [ alias symbol "compose" (instance 1) = "category1 composition".
+apply (s ∘ r)
+ | intros;
+ apply sym1;
+ (*change in ⊢ (? ? ? (? ? ? ? %) ?) with (image_coercion ?? (s ∘ r) U);*)
+ apply (.= †(image_comp ??????));
+ apply (.= (reduced ?? s (image_coercion ?? r U) ?)^-1);
+ [ apply (.= (reduced ?????)); [ assumption | apply refl1 ]
+ | change in ⊢ (? ? ? % ?) with ((image_coercion ?? s ∘ image_coercion ?? r) U);
+ apply (.= (image_comp ??????)^-1);
+ apply refl1]
+ | intros;
+ apply sym1;
+ apply (.= †(minus_star_image_comp ??? s r ?));
+ apply (.= (saturated ?? s ((r)⎻* U) ?)^-1);
+ [ apply (.= (saturated ?????)); [ assumption | apply refl1 ]
+ | change in ⊢ (? ? ? % ?) with ((s⎻* ∘ r⎻* ) U);
+ apply (.= (minus_star_image_comp ??????)^-1);
+ apply refl1]]
+qed.
+