--- a/src/BAlgebra.agda	Thu Apr 06 09:16:52 2023 +0900
+++ b/src/BAlgebra.agda	Thu Apr 06 11:50:41 2023 +0900
@@ -1,3 +1,5 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+
 open import Level
 open import Ordinals
 module BAlgebra {n : Level } (O : Ordinals {n})   where
@@ -124,32 +126,61 @@
     lemma2 {x} lt | _ | case1 cp = case1 cp 
     lemma2 {x} lt | case2 cq | case2 cr = case2 ⟪ cq , cr ⟫ 
 
-record IsBooleanAlgebra ( L : Set n)
+record IsBooleanAlgebra {n : Level} ( L : Set n)
+       ( _==_ : L → L → Set n )
        ( b1 : L )
        ( b0 : L )
        ( -_ : L → L  )
        ( _+_ : L → L → L )
        ( _x_ : L → L → L ) : Set (suc n) where
    field
-       +-assoc : {a b c : L } → a + ( b + c ) ≡ (a + b) + c
-       x-assoc : {a b c : L } → a x ( b x c ) ≡ (a x b) x c
-       +-sym : {a b : L } → a + b ≡ b + a
-       -sym : {a b : L } → a x b  ≡ b x a
-       +-aab : {a b : L } → a + ( a x b ) ≡ a
-       x-aab : {a b : L } → a x ( a + b ) ≡ a
-       +-dist : {a b c : L } → a + ( b x c ) ≡ ( a x b ) + ( a x c )
-       x-dist : {a b c : L } → a x ( b + c ) ≡ ( a + b ) x ( a + c )
-       a+0 : {a : L } → a + b0 ≡ a
-       ax1 : {a : L } → a x b1 ≡ a
-       a+-a1 : {a : L } → a + ( - a ) ≡ b1
-       ax-a0 : {a : L } → a x ( - a ) ≡ b0
+       +-assoc : {a b c : L } → (a + ( b + c )) == ((a + b) + c)
+       x-assoc : {a b c : L } → (a x ( b x c )) == ((a x b) x c)
+       +-sym : {a b : L } → (a + b) == (b + a)
+       -sym : {a b : L } → (a x b)  == (b x a)
+       +-aab : {a b : L } → (a + ( a x b )) == a
+       x-aab : {a b : L } → (a x ( a + b )) == a
+       +-dist : {a b c : L } → (a + ( b x c )) == (( a + b ) x ( a + c ))
+       x-dist : {a b c : L } → (a x ( b + c )) == (( a x b ) + ( a x c ))
+       a+0 : {a : L } → (a + b0) == a
+       ax1 : {a : L } → (a x b1) == a
+       a+-a1 : {a : L } → (a + ( - a )) == b1
+       ax-a0 : {a : L } → (a x ( - a )) == b0
 
-record BooleanAlgebra ( L : Set n) : Set (suc n) where
+record BooleanAlgebra {n : Level} ( L : Set n) : Set (suc n) where
    field
+       _=b=_ : L → L → Set n 
        b1 : L
        b0 : L
        -_ : L → L 
        _+_ : L → L → L
        _x_ : L → L → L
-       isBooleanAlgebra : IsBooleanAlgebra L b1 b0 -_ _+_ _x_
-       
+       isBooleanAlgebra : IsBooleanAlgebra L _=b=_ b1 b0 -_ _+_ _x_
+
+record PowerP (P : HOD) : Set (suc n) where
+    constructor ⟦_,_⟧
+    field
+       hod : HOD
+       x⊆P : hod ⊆ P  
+
+open PowerP
+
+HODBA : (P : HOD) → BooleanAlgebra (PowerP P)
+HODBA P = record { _=b=_ = λ x y → hod x ≡ hod y ; b1 = ⟦ P , (λ x → x) ⟧   ; b0 = ⟦ od∅ , (λ x →  ⊥-elim (¬x<0 x)) ⟧ 
+  ; -_ = λ x → ⟦  P ＼ hod x , proj1 ⟧
+  ; _+_ = λ x y → ⟦ hod x ∪ hod y , ?  ⟧ ; _x_ = λ x y → ⟦ hod x ∩ hod y , (λ lt → x⊆P x (proj1 lt))  ⟧ 
+   ; isBooleanAlgebra = record {
+       +-assoc = λ {a} {b} {c} → ==→o≡ record { eq→ = ? ; eq← = ?  }
+     ; x-assoc = λ {a} {b} {c} → ==→o≡ record { eq→ = λ lt → ⟪ ⟪ proj1 lt  , proj1 (proj2 lt) ⟫ , proj2 (proj2 lt)  ⟫ 
+                                              ; eq← = λ lt → ⟪ proj1 (proj1 lt) , ⟪ proj2 (proj1 lt)  , proj2 lt ⟫ ⟫ } 
+     ; +-sym = ?
+     ; -sym = λ {a} {b} → ==→o≡ record { eq→ = λ lt → ⟪ proj2 lt , proj1 lt ⟫ ; eq← = λ lt → ⟪ proj2 lt , proj1 lt ⟫  }
+     ; +-aab = λ {a} {b} → ==→o≡ record { eq→ = ? ; eq← = case1  }
+     ; x-aab = λ {a} {b} → ==→o≡ record { eq→ = proj1 ; eq← = λ ax →  ⟪ ax , case1 ax ⟫ }
+     ; +-dist = dist-ord2
+     ; x-dist = dist-ord
+     ; a+0 = ?
+     ; ax1 = ?
+     ; a+-a1 = ?
+     ; ax-a0 = ? } }
+