(**************************************************************************)
include "formal_topology/categories.ma".
-
+(*
inductive bool : Type[0] := true : bool | false : bool.
lemma BOOL : objs1 SET.
interpretation "o-algebra overlap" 'overlap a b = (fun21 ??? (oa_overlap ?) a b).
notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (\emsp) \nbsp term 90 p)"
-non associative with precedence 50 for @{ 'oa_meet $p }.
+non associative with precedence 55 for @{ 'oa_meet $p }.
notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∧) \below (ident i ∈ I) break term 90 p)"
-non associative with precedence 50 for @{ 'oa_meet_mk (λ${ident i}:$I.$p) }.
+non associative with precedence 55 for @{ 'oa_meet_mk (λ${ident i}:$I.$p) }.
-notation > "hovbox(∧ f)" non associative with precedence 60
+notation > "hovbox(∧ f)" non associative with precedence 65
for @{ 'oa_meet $f }.
interpretation "o-algebra meet" 'oa_meet f =
(fun12 ?? (oa_meet ??) f).
(fun12 ?? (oa_meet ??) (mk_unary_morphism1 ?? f ?)).
notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (\emsp) \nbsp term 90 p)"
-non associative with precedence 50 for @{ 'oa_join $p }.
+non associative with precedence 55 for @{ 'oa_join $p }.
notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (ident i ∈ I) break term 90 p)"
-non associative with precedence 50 for @{ 'oa_join_mk (λ${ident i}:$I.$p) }.
+non associative with precedence 55 for @{ 'oa_join_mk (λ${ident i}:$I.$p) }.
-notation > "hovbox(∨ f)" non associative with precedence 60
+notation > "hovbox(∨ f)" non associative with precedence 65
for @{ 'oa_join $f }.
interpretation "o-algebra join" 'oa_join f =
(fun12 ?? (oa_join ??) f).
notation < "hovbox(a ∨ b)" left associative with precedence 49
for @{ 'oa_join_mk (λ${ident i}:$_.match $i with [ true ⇒ $a | false ⇒ $b ]) }.
-notation > "hovbox(∨ f)" non associative with precedence 59
+notation > "hovbox(∨ f)" non associative with precedence 64
for @{ 'oa_join $f }.
notation > "hovbox(a ∨ b)" left associative with precedence 49
for @{ 'oa_join (mk_unary_morphism BOOL ? (λx__:bool.match x__ with [ true ⇒ $a | false ⇒ $b ]) (IF_THEN_ELSE_p ? $a $b)) }.
lemma oa_overlap_sym': ∀o:OA.∀U,V:o. (U >< V) = (V >< U).
intros; split; intro; apply oa_overlap_sym; assumption.
qed.
+*)