(* *)
(**************************************************************************)
+include "basics/core_notation/comprehension_2.ma".
include "formal_topology/categories.ma".
-
+(*
inductive bool : Type[0] := true : bool | false : bool.
lemma BOOL : objs1 SET.
constructor 1; [apply bool] constructor 1;
-[ intros (x y); apply (match x with [ true ⇒ match y with [ true ⇒ ⊤ | _ ⇒ ⊥] | false ⇒ match y with [ true ⇒ ⊥ | false ⇒ ⊤ ]]);
+[ intros (x y); apply (match x with [ true ⇒ match y with [ true ⇒ True | _ ⇒ False] | false ⇒ match y with [ true ⇒ False | false ⇒ True ]]);
| whd; simplify; intros; cases x; apply I;
| whd; simplify; intros 2; cases x; cases y; simplify; intros; assumption;
| whd; simplify; intros 3; cases x; cases y; cases z; simplify; intros;
lemma oa_overlap_sym': ∀o:OA.∀U,V:o. (U >< V) = (V >< U).
intros; split; intro; apply oa_overlap_sym; assumption.
qed.
+*)