+
+definition OR : carr3 (arrows3 CAT2 OBP BTop).
+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)));
+ 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 (.= #‡†(Ocommute:?)^-1);
+ apply (.= #‡e1);
+ change in ⊢ (? ? ? (? ? ? ? ? ? %) ?) with (⊩\sub T ∘ a'\sub\c)⎻*;
+ apply (.= #‡†(Ocommute:?));
+ change in ⊢ (? ? ? (? ? ? ? ? ? %) ?) with (a'\sub\f⎻* ∘ (⊩\sub S)⎻* );
+ apply (.= (comp_assoc2 ? ???? ?? a'\sub\f⎻* )^-1);
+ apply refl2;]
+| intros 2 (o a); apply rule #;
+| intros 6; apply refl1;]
+qed.
+
+(*
+axiom DDD : False.
+
+definition sigma_equivalence_relation2:
+ ∀C2:CAT2.∀Q.∀X,Y:exT22 ? (λy:C2.Q y).∀P.
+ equivalence_relation2 (exT22 ? (λf:arrows2 C2 (\fst X) (\fst Y).P f)).
+intros; constructor 1;
+ [ intros(F G); apply (\fst F =_2 \fst G);
+ | intro; apply refl2;
+ | intros 3; apply sym2; assumption;
+ | intros 5; apply (trans2 ?? ??? x1 x2);]
+qed.
+
+definition Apply : ∀C1,C2: CAT2.arrows3 CAT2 C1 C2 → CAT2.
+intros (C1 C2 F);
+constructor 1;
+[ apply (exT22 ? (λx:C2.exT22 ? (λy:C1.map_objs2 ?? F y =_\ID x)));
+| intros (X Y); constructor 1;
+ [ apply (exT22 ? (λf:arrows2 C2 (\fst X) (\fst Y).
+ exT22 ? (λg:arrows2 C1 (\fst (\snd X)) (\fst (\snd Y)).
+ ? (map_arrows2 ?? F ?? g) = f)));
+ intro; apply hide; clear g f; cases X in c; cases Y; cases x; cases x1; clear X Y x x1;
+ simplify; cases H; cases H1; intros; assumption;
+ | apply sigma_equivalence_relation2;]
+| intro o; constructor 1;
+ [ apply (id2 C2 (\fst o))
+ | exists[apply (id2 C1 (\fst (\snd o)))]
+ cases o; cases x; cases H; unfold hide; simplify;
+ apply (respects_id2 ?? F);]
+| intros (o1 o2 o3); constructor 1;
+ [ intros (f g); whd in f g; constructor 1;
+ [ apply (comp2 C2 (\fst o1) (\fst o2) (\fst o3) (\fst f) (\fst g));
+ | exists[apply (comp2 C1 (\fst (\snd o1)) (\fst (\snd o2)) (\fst (\snd o3)) (\fst (\snd f)) (\fst (\snd g)))]
+ cases o1; cases x; cases H;
+