# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1680757475 -32400
# Node ID 437e48221ed5d0bb7cc08eee5b7864abd48020a8
# Parent  a496dbb74a5fcfb98eef0d2376b1a8b8c4035429
...

diff -r a496dbb74a5f -r 437e48221ed5 src/BAlgebra.agda
--- a/src/BAlgebra.agda	Thu Apr 06 11:50:41 2023 +0900
+++ b/src/BAlgebra.agda	Thu Apr 06 14:04:35 2023 +0900
@@ -168,19 +168,39 @@
 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))  ⟧ 
+  ; _+_ = λ x y → ⟦ hod x ∪ hod y , ba00 x y ⟧ ; _x_ = λ x y → ⟦ hod x ∩ hod y , (λ lt → x⊆P x (proj1 lt))  ⟧ 
    ; isBooleanAlgebra = record {
-       +-assoc = λ {a} {b} {c} → ==→o≡ record { eq→ = ? ; eq← = ?  }
+       +-assoc = λ {a} {b} {c} → ==→o≡ record { eq→ = ba01 a b c ; eq← = ba02 a b c  }
      ; 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  }
+     ; +-aab = λ {a} {b} → ==→o≡ record { eq→ = ba03 a b ; 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 = ? } }
-
+     ; a+0 = λ {a} → ==→o≡ record { eq→ = ba04 (hod a) ; eq← = case1 }
+     ; ax1 = λ {a} → ==→o≡ record { eq→ = proj1 ; eq← = λ ax → ⟪ ax , x⊆P a ax ⟫ }
+     ; a+-a1 = λ {a} → ==→o≡ record { eq→ = ? ; eq← = ? }
+     ; ax-a0 =  λ {a} → ==→o≡ record { eq→ = ? ; eq← = λ lt → ⊥-elim (¬x<0 lt) }
+       } } where
+     ba00 : (x y : PowerP P ) →  (hod x ∪ hod y) ⊆ P
+     ba00 x y (case1 px) = x⊆P x px
+     ba00 x y (case2 py) = x⊆P y py
+     ba01 : (a b c : PowerP P) → {x : Ordinal} → odef (hod a) x ∨ odef (hod b ∪ hod c) x →
+            odef (hod a ∪ hod b) x ∨ odef (hod c) x
+     ba01 a b c {x} (case1 ax) = case1 (case1 ax)
+     ba01 a b c {x} (case2 (case1 bx)) = case1 (case2 bx)
+     ba01 a b c {x} (case2 (case2 cx)) = case2 cx
+     ba02 : (a b c : PowerP P) → {x : Ordinal} → odef (hod a ∪ hod b) x ∨ odef (hod c) x
+         → odef (hod a) x ∨ odef (hod b ∪ hod c) x 
+     ba02 a b c {x} (case1 (case1 ax)) = case1 ax
+     ba02 a b c {x} (case1 (case2 bx)) = case2 (case1 bx)
+     ba02 a b c {x} (case2 cx) = case2 (case2 cx)
+     ba03 : (a b : PowerP P) → {x : Ordinal} →
+            odef (hod a) x ∨ odef (hod a ∩ hod b) x → OD.def (od (hod a)) x
+     ba03 a b (case1 ax) = ax
+     ba03 a b (case2 ab) = proj1 ab
+     ba04 : (a : HOD) →  {x : Ordinal} → odef a x ∨ odef od∅ x → odef a x
+     ba04 a (case1 ax) = ax
+     ba04 a (case2 x) = ⊥-elim (¬x<0 x)