--- a/src/BAlgebra.agda	Mon Jan 16 22:43:09 2023 +0900
+++ b/src/BAlgebra.agda	Tue Jan 17 11:21:18 2023 +0900
@@ -33,26 +33,6 @@
 open _∨_
 open Bool
 
---_∩_ : ( A B : HOD  ) → HOD
---A ∩ B = record { od = record { def = λ x → odef A x ∧ odef B x } ;
---    odmax = omin (odmax A) (odmax B) ; <odmax = λ y → min1 (<odmax A (proj1 y)) (<odmax B (proj2 y)) }
-
-∩-comm : { A B : HOD } → (A ∩ B) ≡ (B ∩ A)
-∩-comm {A} {B} = ==→o≡ record { eq← = λ {x} lt → ⟪ proj2 lt , proj1 lt ⟫ ; eq→ =  λ {x} lt → ⟪ proj2 lt , proj1 lt ⟫ }
-
-_∪_ : ( A B : HOD  ) → HOD
-A ∪ B = record { od = record { def = λ x → odef A x ∨ odef B x } ;
-    odmax = omax (odmax A) (odmax B) ; <odmax = lemma } where
-      lemma :  {y : Ordinal} → odef A y ∨ odef B y → y o< omax (odmax A) (odmax B)
-      lemma {y} (case1 a) = ordtrans (<odmax A a) (omax-x _ _)
-      lemma {y} (case2 b) = ordtrans (<odmax B b) (omax-y _ _)
-
-_＼_ : ( A B : HOD  ) → HOD
-A ＼ B = record { od = record { def = λ x → odef A x ∧ ( ¬ ( odef B x ) ) }; odmax = odmax A ; <odmax = λ y → <odmax A (proj1 y) }
-
-¬∅∋ : {x : HOD} → ¬ ( od∅ ∋ x )
-¬∅∋ {x} = ¬x<0
-
 L＼L=0 : { L  : HOD  } → L ＼ L ≡ od∅ 
 L＼L=0 {L} = ==→o≡ ( record { eq→ = lem0 ; eq← =  lem1 } ) where
     lem0 : {x : Ordinal} → odef (L ＼ L) x → odef od∅ x