# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1594770150 -32400
# Node ID 2a8a51375e49ac0064e7dc9e345f189621dc4177
# Parent  5e22b23ee3fd8710e29c639741235daae4919632
...

diff -r 5e22b23ee3fd -r 2a8a51375e49 BAlgbra.agda
--- a/BAlgbra.agda	Tue Jul 14 15:02:59 2020 +0900
+++ b/BAlgbra.agda	Wed Jul 15 08:42:30 2020 +0900
@@ -25,9 +25,9 @@
 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)) }
+--_∩_ : ( 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)) }
 
 _∪_ : ( A B : HOD  ) → HOD
 A ∪ B = record { od = record { def = λ x → odef A x ∨ odef B x } ;
diff -r 5e22b23ee3fd -r 2a8a51375e49 LEMC.agda
--- a/LEMC.agda	Tue Jul 14 15:02:59 2020 +0900
+++ b/LEMC.agda	Wed Jul 15 08:42:30 2020 +0900
@@ -52,6 +52,9 @@
        choice-func = λ A {X} not A∋X → a-choice (choice-func X not );
        choice = λ A {X} A∋X not → is-in (choice-func X not)
      } where
+         --
+         -- the axiom choice from LEM and OD ordering
+         --
          choice-func :  (X : HOD ) → ¬ ( X =h= od∅ ) → choiced X
          choice-func  X not = have_to_find where
                  ψ : ( ox : Ordinal ) → Set (suc n)
@@ -88,6 +91,12 @@
                             eq→ = λ {x} lt → ⊥-elim  (nn x (odef→o< lt) lt) 
                           ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
                         }
+
+         --
+         --  axiom regurality from ε-induction (using axiom of choice above)
+         --
+         --  from https://math.stackexchange.com/questions/2973777/is-it-possible-to-prove-regularity-with-transfinite-induction-only
+         --
          record Minimal (x : HOD)  : Set (suc n) where
            field
                min : HOD
@@ -95,9 +104,6 @@
                min-empty :  (y : HOD ) → ¬ ( min ∋ y) ∧ (x ∋ y)
          open Minimal
          open _∧_
-         --
-         --  from https://math.stackexchange.com/questions/2973777/is-it-possible-to-prove-regularity-with-transfinite-induction-only
-         --
          induction : {x : HOD} → ({y : HOD} → x ∋ y → (u : HOD ) → (u∋x : u ∋ y) → Minimal u )
               →  (u : HOD ) → (u∋x : u ∋ x) → Minimal u 
          induction {x} prev u u∋x with p∨¬p ((y : HOD) → ¬ (x ∋ y) ∧ (u ∋ y))
diff -r 5e22b23ee3fd -r 2a8a51375e49 OD.agda
--- a/OD.agda	Tue Jul 14 15:02:59 2020 +0900
+++ b/OD.agda	Wed Jul 15 08:42:30 2020 +0900
@@ -249,10 +249,9 @@
 in-codomain : (X : HOD  ) → ( ψ : HOD  → HOD  ) → OD 
 in-codomain  X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧  ( x ≡ od→ord (ψ (ord→od y )))))  }
 
-ZFSubset : (A x : HOD  ) → HOD 
-ZFSubset A x =  record { od = record { def = λ y → odef A y ∧  odef x y } ; odmax = omin (odmax A) (odmax x) ; <odmax = lemma }  where --   roughly x = A → Set 
-     lemma : {y : Ordinal} → def (od A) y ∧ def (od x) y → y o< omin (odmax A) (odmax x)
-     lemma {y} and = min1 (<odmax A (proj1 and)) (<odmax x (proj2 and))
+_∩_ : ( 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))}
 
 record _⊆_ ( A B : HOD   ) : Set (suc n) where
   field 
@@ -281,7 +280,7 @@
     lemma1 : osuc (od→ord y) o< od→ord (x , x)
     lemma1 = subst (λ k → osuc (od→ord y) o< k ) (sym (peq {x})) (osucc c ) 
 
-subset-lemma : {A x : HOD  } → ( {y : HOD } →  x ∋ y → ZFSubset A x ∋  y ) ⇔  ( x ⊆ A  )
+subset-lemma : {A x : HOD  } → ( {y : HOD } →  x ∋ y → (A ∩ x ) ∋  y ) ⇔  ( x ⊆ A  )
 subset-lemma  {A} {x} = record {
       proj1 = λ lt  → record { incl = λ x∋z → proj1 (lt x∋z)  }
     ; proj2 = λ x⊆A lt → record { proj1 = incl x⊆A lt ; proj2 = lt } 
@@ -337,9 +336,6 @@
           rmax = sup-o X (λ y X∋y → od→ord (ψ (ord→od y)))
           rmax< :  {y : Ordinal} → (y o< rmax) ∧ def (in-codomain X ψ) y → y o< rmax
           rmax< lt = proj1 lt
-    _∩_ : ( A B : ZFSet  ) → ZFSet
-    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))}
     Union : HOD  → HOD   
     Union U = record { od = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((odef U u) ∧ (odef (ord→od u) x)))  }
        ; odmax = osuc (od→ord U) ; <odmax = umax< } where
@@ -360,7 +356,7 @@
     A ∈ B = B ∋ A
 
     OPwr :  (A :  HOD ) → HOD 
-    OPwr  A = Ord ( sup-o (Ord (osuc (od→ord A))) ( λ x A∋x → od→ord ( ZFSubset A (ord→od x)) ) )   
+    OPwr  A = Ord ( sup-o (Ord (osuc (od→ord A))) ( λ x A∋x → od→ord ( A ∩ (ord→od x)) ) )   
 
     Power : HOD  → HOD 
     Power A = Replace (OPwr (Ord (od→ord A))) ( λ x → A ∩ x )
@@ -495,7 +491,7 @@
          ---
          ---    First consider ordinals in HOD
          ---
-         --- ZFSubset A x =  record { def = λ y → odef A y ∧  odef x y }                   subset of A
+         --- A ∩ x =  record { def = λ y → odef A y ∧  odef x y }                   subset of A
          --
          --
          ∩-≡ :  { a b : HOD  } → ({x : HOD  } → (a ∋ x → b ∋ x)) → a =h= ( b ∩ a )
@@ -505,24 +501,24 @@
             eq← = λ {x} x<a∩b → proj2 x<a∩b }
          -- 
          -- Transitive Set case
-         -- we have t ∋ x → Ord a ∋ x means t is a subset of Ord a, that is ZFSubset (Ord a) t =h= t
-         -- OPwr (Ord a) is a sup of ZFSubset (Ord a) t, so OPwr (Ord a) ∋ t
-         -- OPwr  A = Ord ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )   
+         -- we have t ∋ x → Ord a ∋ x means t is a subset of Ord a, that is (Ord a) ∩ t =h= t
+         -- OPwr (Ord a) is a sup of (Ord a) ∩ t, so OPwr (Ord a) ∋ t
+         -- OPwr  A = Ord ( sup-o ( λ x → od→ord ( A ∩ (ord→od x )) ) )   
          -- 
          ord-power← : (a : Ordinal ) (t : HOD) → ({x : HOD} → (t ∋ x → (Ord a) ∋ x)) → OPwr (Ord a) ∋ t
          ord-power← a t t→A  = odef-subst  {_} {_} {OPwr (Ord a)} {od→ord t}
                  lemma refl (lemma1 lemma-eq )where
-              lemma-eq :  ZFSubset (Ord a) t =h= t
+              lemma-eq :  ((Ord a) ∩ t) =h= t
               eq→ lemma-eq {z} w = proj2 w 
               eq← lemma-eq {z} w = record { proj2 = w  ;
                  proj1 = odef-subst  {_} {_} {(Ord a)} {z}
                     ( t→A (odef-subst  {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso  }
               lemma1 :  {a : Ordinal } { t : HOD }
-                 → (eq : ZFSubset (Ord a) t =h= t)  → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t
-              lemma1  {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq ))
+                 → (eq : ((Ord a) ∩ t) =h= t)  → od→ord ((Ord a) ∩ (ord→od (od→ord t))) ≡ od→ord t
+              lemma1  {a} {t} eq = subst (λ k → od→ord ((Ord a) ∩ k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (==→o≡ eq ))
               lemma2 : (od→ord t) o< (osuc (od→ord (Ord a)))
               lemma2 = ⊆→o≤  {t} {Ord a} (λ {x} x<t → subst (λ k → def (od (Ord a)) k) diso (t→A (subst (λ k → def (od t) k) (sym diso) x<t))) 
-              lemma :  od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (Ord (osuc (od→ord (Ord a)))) (λ x lt → od→ord (ZFSubset (Ord a) (ord→od x)))
+              lemma :  od→ord ((Ord a) ∩ (ord→od (od→ord t)) ) o< sup-o (Ord (osuc (od→ord (Ord a)))) (λ x lt → od→ord ((Ord a) ∩ (ord→od x)))
               lemma = sup-o< _ lemma2
 
          -- 
@@ -561,20 +557,20 @@
                     t
                  ∎
               sup1 : Ordinal
-              sup1 =  sup-o (Ord (osuc (od→ord (Ord (od→ord A))))) (λ x A∋x → od→ord (ZFSubset (Ord (od→ord A)) (ord→od x)))
+              sup1 =  sup-o (Ord (osuc (od→ord (Ord (od→ord A))))) (λ x A∋x → od→ord ((Ord (od→ord A)) ∩ (ord→od x)))
               lemma9 : def (od (Ord (Ordinals.osuc O (od→ord (Ord (od→ord A)))))) (od→ord (Ord (od→ord A)))
               lemma9 = <-osuc 
-              lemmab : od→ord (ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A) )))) o< sup1
+              lemmab : od→ord ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A) )))) o< sup1
               lemmab = sup-o< (Ord (osuc (od→ord (Ord (od→ord A))))) lemma9 
               lemmad : Ord (osuc (od→ord A)) ∋ t
               lemmad = ⊆→o≤ (λ {x} lt → subst (λ k → def (od A) k ) diso (t→A (subst (λ k → def (od t) k ) (sym diso) lt))) 
-              lemmac : ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A) ))) =h= Ord (od→ord A)
+              lemmac : ((Ord (od→ord A)) ∩  (ord→od (od→ord (Ord (od→ord A) )))) =h= Ord (od→ord A)
               lemmac = record { eq→ = lemmaf ; eq← = lemmag } where
-                 lemmaf : {x : Ordinal} → def (od (ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A)))))) x → def (od (Ord (od→ord A))) x
+                 lemmaf : {x : Ordinal} → def (od ((Ord (od→ord A)) ∩  (ord→od (od→ord (Ord (od→ord A)))))) x → def (od (Ord (od→ord A))) x
                  lemmaf {x} lt = proj1 lt
-                 lemmag :  {x : Ordinal} → def (od (Ord (od→ord A))) x → def (od (ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A)))))) x
+                 lemmag :  {x : Ordinal} → def (od (Ord (od→ord A))) x → def (od ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A)))))) x
                  lemmag {x} lt = record { proj1 = lt ; proj2 = subst (λ k → def (od k) x) (sym oiso) lt } 
-              lemmae : od→ord (ZFSubset (Ord (od→ord A)) (ord→od (od→ord (Ord (od→ord A))))) ≡ od→ord (Ord (od→ord A))
+              lemmae : od→ord ((Ord (od→ord A)) ∩ (ord→od (od→ord (Ord (od→ord A))))) ≡ od→ord (Ord (od→ord A))
               lemmae = cong (λ k → od→ord k ) ( ==→o≡ lemmac)
               lemma7 : def (od (OPwr (Ord (od→ord A)))) (od→ord t)
               lemma7 with osuc-≡< lemmad
diff -r 5e22b23ee3fd -r 2a8a51375e49 OPair.agda
--- a/OPair.agda	Tue Jul 14 15:02:59 2020 +0900
+++ b/OPair.agda	Wed Jul 15 08:42:30 2020 +0900
@@ -136,3 +136,18 @@
 p-pi2 :  { x y : HOD } → (p : def ZFProduct (od→ord  < x , y >) ) →  π2 p ≡ y
 p-pi2 {x} {y} p = proj2 ( prod-eq ( ord→== (op-iso p)))
 
+
+_⊗_  : (A B : HOD) → HOD
+A ⊗ B  = record { od = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkAB p ) } ;
+        odmax = pmax; <odmax = <pmax } where
+    checkAB : { p : Ordinal } → def ZFProduct p → Set n
+    checkAB (pair x y) = odef A x ∧ odef B y
+    pmax : Ordinal
+    pmax = omax (odmax A)  (odmax B)
+    <pmax : {y : Ordinal} → def ZFProduct y ∧ ({x : Ordinal} (p : def ZFProduct x) → checkAB p) → y o< omax (odmax A)  (odmax B)
+    <pmax {y} = TransFinite {λ y → def ZFProduct y ∧ ({x : Ordinal} (p : def ZFProduct x) → checkAB p) → y o< omax (odmax A)  (odmax B)} ind y where
+        ind : (x : Ordinal)
+            → ((y₁ : Ordinal) → y₁ o< x → def ZFProduct y₁ ∧ ({x₁ : Ordinal} (p : def ZFProduct x₁) → checkAB p) → y₁ o< (omax (odmax A) (odmax B)))
+            → def ZFProduct x ∧ ({x₁ : Ordinal} (p : def ZFProduct x₁) → checkAB p) → x o< (omax (HOD.odmax A) (HOD.odmax B))
+        ind = {!!}
+