# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1685747630 -32400
# Node ID ad9ed7c4a0b38ceab37cdd8ef8dc686982af40ce
# Parent  428227847d6242bcb27eb2402aabf766f4d56929
...

diff -r 428227847d62 -r ad9ed7c4a0b3 src/OD.agda
--- a/src/OD.agda	Fri Jun 02 12:12:29 2023 +0900
+++ b/src/OD.agda	Sat Jun 03 08:13:50 2023 +0900
@@ -108,12 +108,8 @@
 
 -- possible order restriction (required in the axiom of infinite )
 
-record ODAxiom-ho< : Set (suc n) where
- field
-  ho< : {x : HOD} → & x o< next (odmax x)
-
-postulate  odAxiom-ho< : ODAxiom-ho<
-open ODAxiom-ho< odAxiom-ho<
+-- postulate  odAxiom-ho< : ODAxiom-ho<
+-- open ODAxiom-ho< odAxiom-ho<
 
 -- odmax minimality
 --
@@ -451,7 +447,6 @@
 -- ｛_｝ : ZFSet → ZFSet
 -- ｛ x ｝ = ( x ,  x )     -- better to use (x , x) directly
 
-
 data infinite-d  : ( x : Ordinal  ) → Set n where
     iφ :  infinite-d o∅
     isuc : {x : Ordinal  } →   infinite-d  x  →
@@ -465,28 +460,21 @@
 --
 --  Since we have Ord (next o∅), we don't need this, but ZF axiom requires this and ho<
 
+infinite-od : OD
+infinite-od = record { def = λ x → infinite-d x } 
+
+record ODAxiom-ho< : Set (suc n) where
+ field
+    omega : Ordinal  
+    ho< : {x : Ordinal } → infinite-d x →  x o< next omega
+
+postulate
+    odaxion-ho< : ODAxiom-ho< 
+
+open ODAxiom-ho< odaxion-ho<
+
 infinite : HOD
-infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next o∅ ; <odmax = lemma }  where
-    u : (y : Ordinal ) → HOD
-    u y = Union (* y , (* y , * y))
-    --   next< : {x y z : Ordinal} → x o< next z  → y o< next x → y o< next z
-    lemma8 : {y : Ordinal} → & (* y , * y) o< next (odmax (* y , * y))
-    lemma8 = ho<
-    ---           (x,y) < next (omax x y) < next (osuc y) = next y
-    lemmaa : {x y : HOD} → & x o< & y → & (x , y) o< next (& y)
-    lemmaa {x} {y} x<y = subst (λ k → & (x , y) o< k ) (sym nexto≡) (subst (λ k → & (x , y) o< next k ) (sym (omax< _ _ x<y)) ho< )
-    lemma81 : {y : Ordinal} → & (* y , * y) o< next (& (* y))
-    lemma81 {y} = nexto=n (subst (λ k →  & (* y , * y) o< k ) (cong (λ k → next k) (omxx _)) lemma8)
-    lemma9 : {y : Ordinal} → & (* y , (* y , * y)) o< next (& (* y , * y))
-    lemma9 = lemmaa (c<→o< (case1 refl))
-    lemma71 : {y : Ordinal} → & (* y , (* y , * y)) o< next (& (* y))
-    lemma71 = next< lemma81 lemma9
-    lemma1 : {y : Ordinal} → & (u y) o< next (osuc (& (* y , (* y , * y))))
-    lemma1 = ho<
-    --- main recursion
-    lemma : {y : Ordinal} → infinite-d y → y o< next o∅
-    lemma {o∅} iφ = x<nx
-    lemma (isuc {y} x) = next< (lemma x) (next< (subst (λ k → & (* y , (* y , * y)) o< next k) &iso lemma71 ) (nexto=n lemma1))
+infinite = record { od = record { def = λ x → infinite-d x } ; odmax = next omega ; <odmax = ho<}  
 
 empty : (x : HOD  ) → ¬  (od∅ ∋ x)
 empty x = ¬x<0
diff -r 428227847d62 -r ad9ed7c4a0b3 src/ODUtil.agda
--- a/src/ODUtil.agda	Fri Jun 02 12:12:29 2023 +0900
+++ b/src/ODUtil.agda	Sat Jun 03 08:13:50 2023 +0900
@@ -23,7 +23,7 @@
 open OD O
 open OD.OD
 open ODAxiom odAxiom
-open ODAxiom-ho< odAxiom-ho<
+-- open ODAxiom-ho< odAxiom-ho<
 
 open HOD
 open _∧_
@@ -75,20 +75,20 @@
    lemma {z} (case1 refl) = case1 refl
    lemma {z} (case2 refl) = case1 refl
 
-pair-<xy : {x y : HOD} → {n : Ordinal}  → & x o< next n →  & y o< next n  → & (x , y) o< next n
-pair-<xy {x} {y} {o} x<nn y<nn with trio< (& x) (& y) | inspect (omax (& x)) (& y)
-... | tri< a ¬b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx y<nn)) ho<
-... | tri> ¬a ¬b c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx x<nn)) ho<
-... | tri≈ ¬a b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (omax≡ _ _ b) (subst (λ k → osuc k o< next o) b (osuc<nx x<nn))) ho<
+-- pair-<xy : {x y : HOD} → {n : Ordinal}  → & x o< next n →  & y o< next n  → & (x , y) o< next n
+-- pair-<xy {x} {y} {o} x<nn y<nn with trio< (& x) (& y) | inspect (omax (& x)) (& y)
+-- ... | tri< a ¬b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx y<nn)) ho<
+-- ... | tri> ¬a ¬b c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (sym eq1) (osuc<nx x<nn)) ho<
+-- ... | tri≈ ¬a b ¬c | record { eq = eq1 } = next< (subst (λ k → k o< next o ) (omax≡ _ _ b) (subst (λ k → osuc k o< next o) b (osuc<nx x<nn))) ho<
 
 --  another form of infinite
 -- pair-ord< :  {x : Ordinal } → Set n
-pair-ord< : {x : HOD } → ( {y : HOD } → & y o< next (odmax y) ) → & ( x , x ) o< next (& x)
-pair-ord< {x} ho< = subst (λ k → & (x , x) o< k ) lemmab0 lemmab1  where
-       lemmab0 : next (odmax (x , x)) ≡ next (& x)
-       lemmab0 = trans (cong (λ k → next k) (omxx _)) (sym nexto≡)
-       lemmab1 : & (x , x) o< next ( odmax (x , x))
-       lemmab1 = ho<
+-- pair-ord< : {x : HOD } → ( {y : HOD } → & y o< next (odmax y) ) → & ( x , x ) o< next (& x)
+-- pair-ord< {x} ho< = subst (λ k → & (x , x) o< k ) lemmab0 lemmab1  where
+--        lemmab0 : next (odmax (x , x)) ≡ next (& x)
+--        lemmab0 = trans (cong (λ k → next k) (omxx _)) (sym nexto≡)
+--        lemmab1 : & (x , x) o< next ( odmax (x , x))
+--        lemmab1 = ho<
 
 trans-⊆ :  { A B C : HOD} → A ⊆ B → B ⊆ C → A ⊆ C
 trans-⊆ A⊆B B⊆C ab = B⊆C (A⊆B ab)
@@ -115,8 +115,13 @@
     ; proj2 = λ x⊆A lt → ⟪ x⊆A lt , lt ⟫
    }
 
-ω<next-o∅ : {y : Ordinal} → infinite-d y → y o< next o∅
-ω<next-o∅ {y} lt = <odmax infinite lt
+--postulate
+--    odaxion-ho< : ODAxiom-ho< 
+--
+--open ODAxiom-ho< odaxion-ho<
+
+-- ω<next-o∅ : {y : Ordinal} → infinite-d y → y o< next omega
+-- ω<next-o∅ {y} lt = <odmax infinite lt
 
 nat→ω : Nat → HOD
 nat→ω Zero = od∅
diff -r 428227847d62 -r ad9ed7c4a0b3 src/OrdUtil.agda
--- a/src/OrdUtil.agda	Fri Jun 02 12:12:29 2023 +0900
+++ b/src/OrdUtil.agda	Sat Jun 03 08:13:50 2023 +0900
@@ -259,29 +259,29 @@
 nexto∅ {x} | tri≈ ¬a b ¬c = subst (λ k → k o< next x) (sym b) x<nx
 nexto∅ {x} | tri> ¬a ¬b c = ⊥-elim ( ¬x<0 c )
 
-next< : {x y z : Ordinal} → x o< next z  → y o< next x → y o< next z
-next< {x} {y} {z} x<nz y<nx with trio< y (next z)
-next< {x} {y} {z} x<nz y<nx | tri< a ¬b ¬c = a
-next< {x} {y} {z} x<nz y<nx | tri≈ ¬a b ¬c = ⊥-elim (¬nx<nx x<nz (subst (λ k → k o< next x) b y<nx)
-   (λ w nz=ow → o<¬≡ nz=ow (subst₂ (λ j k → j o< k ) (sym nz=ow) nz=ow (osuc<nx (subst (λ k → w o< k ) (sym nz=ow) <-osuc) ))))
-next< {x} {y} {z} x<nz y<nx | tri> ¬a ¬b c = ⊥-elim (¬nx<nx x<nz (ordtrans c y<nx )
-   (λ w nz=ow → o<¬≡ (sym nz=ow) (osuc<nx (subst (λ k → w o< k ) (sym nz=ow) <-osuc ))))
+-- next< : {x y z : Ordinal} → x o< next z  → y o< next x → y o< next z
+-- next< {x} {y} {z} x<nz y<nx with trio< y (next z)
+-- next< {x} {y} {z} x<nz y<nx | tri< a ¬b ¬c = a
+-- next< {x} {y} {z} x<nz y<nx | tri≈ ¬a b ¬c = ⊥-elim (¬nx<nx x<nz (subst (λ k → k o< next x) b y<nx)
+--    (λ w nz=ow → o<¬≡ nz=ow (subst₂ (λ j k → j o< k ) (sym nz=ow) nz=ow (osuc<nx (subst (λ k → w o< k ) (sym nz=ow) <-osuc) ))))
+-- next< {x} {y} {z} x<nz y<nx | tri> ¬a ¬b c = ⊥-elim (¬nx<nx x<nz (ordtrans c y<nx )
+--    (λ w nz=ow → o<¬≡ (sym nz=ow) (osuc<nx (subst (λ k → w o< k ) (sym nz=ow) <-osuc ))))
 
 osuc< : {x y : Ordinal} → osuc x ≡ y → x o< y
 osuc< {x} {y} refl = <-osuc
 
-nexto=n : {x y : Ordinal} → x o< next (osuc y)  → x o< next y
-nexto=n {x} {y} x<noy = next< (osuc<nx x<nx) x<noy
+-- nexto=n : {x y : Ordinal} → x o< next (osuc y)  → x o< next y
+-- nexto=n {x} {y} x<noy = next< (osuc<nx x<nx) x<noy
 
-nexto≡ : {x : Ordinal} → next x ≡ next (osuc x)
-nexto≡ {x} with trio< (next x) (next (osuc x) )
+-- nexto≡ : {x : Ordinal} → next x ≡ next (osuc x)
+-- nexto≡ {x} with trio< (next x) (next (osuc x) )
 --    next x o< next (osuc x ) ->  osuc x o< next x o< next (osuc x) -> next x ≡ osuc z -> z o o< next x -> osuc z o< next x -> next x o< next x
-nexto≡ {x} | tri< a ¬b ¬c = ⊥-elim (¬nx<nx (osuc<nx  x<nx ) a
-   (λ z eq → o<¬≡ (sym eq) (osuc<nx  (osuc< (sym eq)))))
-nexto≡ {x} | tri≈ ¬a b ¬c = b
+-- nexto≡ {x} | tri< a ¬b ¬c = ⊥-elim (¬nx<nx (osuc<nx  x<nx ) a
+--    (λ z eq → o<¬≡ (sym eq) (osuc<nx  (osuc< (sym eq)))))
+-- nexto≡ {x} | tri≈ ¬a b ¬c = b
 --    next (osuc x) o< next x ->  osuc x o< next (osuc x) o< next x -> next (osuc x) ≡ osuc z -> z o o< next (osuc x) ...
-nexto≡ {x} | tri> ¬a ¬b c = ⊥-elim (¬nx<nx (ordtrans <-osuc x<nx) c
-   (λ z eq → o<¬≡ (sym eq) (osuc<nx  (osuc< (sym eq)))))
+-- nexto≡ {x} | tri> ¬a ¬b c = ⊥-elim (¬nx<nx (ordtrans <-osuc x<nx) c
+--    (λ z eq → o<¬≡ (sym eq) (osuc<nx  (osuc< (sym eq)))))
 
 next-is-limit : {x y : Ordinal} → ¬ (next x ≡ osuc y)
 next-is-limit {x} {y} eq = o<¬≡ (sym eq) (osuc<nx y<nx) where
@@ -291,33 +291,33 @@
 omax<next : {x y : Ordinal} → x o< y → omax x y o< next y
 omax<next {x} {y} x<y = subst (λ k → k o< next y ) (omax< _ _ x<y ) (osuc<nx x<nx)
 
-x<ny→≡next : {x y : Ordinal} → x o< y → y o< next x → next x ≡ next y
-x<ny→≡next {x} {y} x<y y<nx with trio< (next x) (next y)
-x<ny→≡next {x} {y} x<y y<nx | tri< a ¬b ¬c =          -- x < y < next x <  next y ∧ next x = osuc z
-     ⊥-elim ( ¬nx<nx y<nx a (λ z eq →  o<¬≡ (sym eq) (osuc<nx (subst (λ k → z o< k ) (sym eq) <-osuc ))))
-x<ny→≡next {x} {y} x<y y<nx | tri≈ ¬a b ¬c = b
-x<ny→≡next {x} {y} x<y y<nx | tri> ¬a ¬b c =          -- x < y < next y < next x
-     ⊥-elim ( ¬nx<nx (ordtrans x<y x<nx) c (λ z eq →  o<¬≡ (sym eq) (osuc<nx (subst (λ k → z o< k ) (sym eq) <-osuc ))))
+-- x<ny→≡next : {x y : Ordinal} → x o< y → y o< next x → next x ≡ next y
+-- x<ny→≡next {x} {y} x<y y<nx with trio< (next x) (next y)
+-- x<ny→≡next {x} {y} x<y y<nx | tri< a ¬b ¬c =          -- x < y < next x <  next y ∧ next x = osuc z
+--      ⊥-elim ( ¬nx<nx y<nx a (λ z eq →  o<¬≡ (sym eq) (osuc<nx (subst (λ k → z o< k ) (sym eq) <-osuc ))))
+-- x<ny→≡next {x} {y} x<y y<nx | tri≈ ¬a b ¬c = b
+-- x<ny→≡next {x} {y} x<y y<nx | tri> ¬a ¬b c =          -- x < y < next y < next x
+--      ⊥-elim ( ¬nx<nx (ordtrans x<y x<nx) c (λ z eq →  o<¬≡ (sym eq) (osuc<nx (subst (λ k → z o< k ) (sym eq) <-osuc ))))
 
-≤next : {x y : Ordinal} → x o≤ y → next x o≤ next y
-≤next {x} {y} x≤y with trio< (next x) y
-≤next {x} {y} x≤y | tri< a ¬b ¬c = ordtrans a (ordtrans x<nx <-osuc )
-≤next {x} {y} x≤y | tri≈ ¬a refl ¬c = (ordtrans x<nx <-osuc )
-≤next {x} {y} x≤y | tri> ¬a ¬b c with osuc-≡< x≤y
-≤next {x} {y} x≤y | tri> ¬a ¬b c | case1 refl = o≤-refl -- x = y < next x
-≤next {x} {y} x≤y | tri> ¬a ¬b c | case2 x<y = o≤-refl0 (x<ny→≡next x<y c) -- x ≤ y < next x
+-- ≤next : {x y : Ordinal} → x o≤ y → next x o≤ next y
+-- ≤next {x} {y} x≤y with trio< (next x) y
+-- ≤next {x} {y} x≤y | tri< a ¬b ¬c = ordtrans a (ordtrans x<nx <-osuc )
+-- ≤next {x} {y} x≤y | tri≈ ¬a refl ¬c = (ordtrans x<nx <-osuc )
+-- ≤next {x} {y} x≤y | tri> ¬a ¬b c with osuc-≡< x≤y
+-- ≤next {x} {y} x≤y | tri> ¬a ¬b c | case1 refl = o≤-refl -- x = y < next x
+-- ≤next {x} {y} x≤y | tri> ¬a ¬b c | case2 x<y = o≤-refl0 (x<ny→≡next x<y c) -- x ≤ y < next x
 
-x<ny→≤next : {x y : Ordinal} → x o< next y → next x o≤ next y
-x<ny→≤next {x} {y} x<ny with trio< x y
-x<ny→≤next {x} {y} x<ny | tri< a ¬b ¬c =  ≤next (ordtrans a <-osuc )
-x<ny→≤next {x} {y} x<ny | tri≈ ¬a refl ¬c =  o≤-refl
-x<ny→≤next {x} {y} x<ny | tri> ¬a ¬b c = o≤-refl0 (sym ( x<ny→≡next c x<ny ))
+-- x<ny→≤next : {x y : Ordinal} → x o< next y → next x o≤ next y
+-- x<ny→≤next {x} {y} x<ny with trio< x y
+-- x<ny→≤next {x} {y} x<ny | tri< a ¬b ¬c =  ≤next (ordtrans a <-osuc )
+-- x<ny→≤next {x} {y} x<ny | tri≈ ¬a refl ¬c =  o≤-refl
+-- x<ny→≤next {x} {y} x<ny | tri> ¬a ¬b c = o≤-refl0 (sym ( x<ny→≡next c x<ny ))
 
-omax<nomax : {x y : Ordinal} → omax x y o< next (omax x y )
-omax<nomax {x} {y} with trio< x y
-omax<nomax {x} {y} | tri< a ¬b ¬c    = subst (λ k → osuc y o< k ) nexto≡ (osuc<nx x<nx )
-omax<nomax {x} {y} | tri≈ ¬a refl ¬c = subst (λ k → osuc x o< k ) nexto≡ (osuc<nx x<nx )
-omax<nomax {x} {y} | tri> ¬a ¬b c    = subst (λ k → osuc x o< k ) nexto≡ (osuc<nx x<nx )
+-- omax<nomax : {x y : Ordinal} → omax x y o< next (omax x y )
+-- omax<nomax {x} {y} with trio< x y
+-- omax<nomax {x} {y} | tri< a ¬b ¬c    = subst (λ k → osuc y o< k ) nexto≡ (osuc<nx x<nx )
+-- omax<nomax {x} {y} | tri≈ ¬a refl ¬c = subst (λ k → osuc x o< k ) nexto≡ (osuc<nx x<nx )
+-- omax<nomax {x} {y} | tri> ¬a ¬b c    = subst (λ k → osuc x o< k ) nexto≡ (osuc<nx x<nx )
 
 omax<nx : {x y z : Ordinal} → x o< next z → y o< next z → omax x y o< next z
 omax<nx {x} {y} {z} x<nz y<nz with trio< x y
@@ -325,11 +325,11 @@
 omax<nx {x} {y} {z} x<nz y<nz | tri≈ ¬a refl ¬c = osuc<nx y<nz
 omax<nx {x} {y} {z} x<nz y<nz | tri> ¬a ¬b c = osuc<nx x<nz
 
-nn<omax : {x nx ny : Ordinal} → x o< next nx → x o< next ny → x o< next (omax nx ny)
-nn<omax {x} {nx} {ny} xnx xny with trio< nx ny
-nn<omax {x} {nx} {ny} xnx xny | tri< a ¬b ¬c = subst (λ k → x o< k ) nexto≡ xny
-nn<omax {x} {nx} {ny} xnx xny | tri≈ ¬a refl ¬c = subst (λ k → x o< k ) nexto≡ xny
-nn<omax {x} {nx} {ny} xnx xny | tri> ¬a ¬b c = subst (λ k → x o< k ) nexto≡ xnx
+-- nn<omax : {x nx ny : Ordinal} → x o< next nx → x o< next ny → x o< next (omax nx ny)
+-- nn<omax {x} {nx} {ny} xnx xny with trio< nx ny
+-- nn<omax {x} {nx} {ny} xnx xny | tri< a ¬b ¬c = subst (λ k → x o< k ) nexto≡ xny
+-- nn<omax {x} {nx} {ny} xnx xny | tri≈ ¬a refl ¬c = subst (λ k → x o< k ) nexto≡ xny
+-- nn<omax {x} {nx} {ny} xnx xny | tri> ¬a ¬b c = subst (λ k → x o< k ) nexto≡ xnx
 
 record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
   field
diff -r 428227847d62 -r ad9ed7c4a0b3 src/Ordinals.agda
--- a/src/Ordinals.agda	Fri Jun 02 12:12:29 2023 +0900
+++ b/src/Ordinals.agda	Sat Jun 03 08:13:50 2023 +0900
@@ -34,7 +34,9 @@
    field
      x<nx :    { y : ord } → (y o< next y )
      osuc<nx : { x y : ord } → x o< next y → osuc x o< next y 
-     ¬nx<nx :  {x y : ord} → y o< x → x o< next y →  ¬ ((z : ord) → ¬ (x ≡ osuc z)) 
+     --
+     -- this means we have some non constructive previous, it looks bad
+     -- ¬nx<nx :  {x y : ord} → y o< x → x o< next y →  ¬ ((z : ord) → ¬ (x ≡ osuc z)) 
 
 record Ordinals {n : Level} : Set (suc (suc n)) where
    field
diff -r 428227847d62 -r ad9ed7c4a0b3 src/PFOD.agda
--- a/src/PFOD.agda	Fri Jun 02 12:12:29 2023 +0900
+++ b/src/PFOD.agda	Sat Jun 03 08:13:50 2023 +0900
@@ -22,7 +22,7 @@
 open OD O
 open OD.OD
 open ODAxiom odAxiom
-open ODAxiom-ho< odAxiom-ho<
+-- open ODAxiom-ho< odAxiom-ho<
 import OrdUtil
 import ODUtil
 open Ordinals.Ordinals  O
@@ -73,19 +73,19 @@
 HODω2 = record { od = record { def = λ x → Hω2r x } ; odmax = next o∅ ; <odmax = odmax0 } where
     P  : (i j : Nat) (x : Ordinal ) → HOD
     P  i j x = ((nat→ω i , nat→ω i) , (nat→ω i , nat→ω j)) , * x
-    nat1 : (i : Nat) (x : Ordinal) → & (nat→ω i) o< next x
-    nat1 i x =  next< nexto∅ ( <odmax infinite (ω∋nat→ω {i}))
+    -- nat1 : (i : Nat) (x : Ordinal) → & (nat→ω i) o< next x
+    -- nat1 i x =  next< nexto∅ ( <odmax infinite (ω∋nat→ω {i}))
     lemma1 : (i j : Nat) (x : Ordinal ) → osuc (& (P i j x)) o< next x
-    lemma1 i j x = osuc<nx (pair-<xy (pair-<xy (pair-<xy (nat1 i x) (nat1 i x) ) (pair-<xy (nat1 i x) (nat1 j x) ) )
-         (subst (λ k → k o< next x) (sym &iso) x<nx ))
+    lemma1 i j x = ? -- osuc<nx (pair-<xy (pair-<xy (pair-<xy (nat1 i x) (nat1 i x) ) (pair-<xy (nat1 i x) (nat1 j x) ) )
+    --      (subst (λ k → k o< next x) (sym &iso) x<nx ))
     lemma : (i j : Nat) (x : Ordinal ) → & (Union (P i j x)) o< next x
-    lemma i j x = next< (lemma1 i j x ) ho<
+    lemma i j x = ? -- next< (lemma1 i j x ) ho<
     odmax0 :  {y : Ordinal} → Hω2r y → y o< next o∅ 
     odmax0 {y} r with hω2 r
     ... | hφ = x<nx
-    ... | h0 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma i 0 x)
-    ... | h1 {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) (lemma i 1 x)
-    ... | he {i} {x} t = next< (odmax0 record { count = i ; hω2 = t }) x<nx
+    ... | h0 {i} {x} t = ? -- jnext< (odmax0 record { count = i ; hω2 = t }) (lemma i 0 x)
+    ... | h1 {i} {x} t = ? -- jnext< (odmax0 record { count = i ; hω2 = t }) (lemma i 1 x)
+    ... | he {i} {x} t = ? -- jnext< (odmax0 record { count = i ; hω2 = t }) x<nx
 
 3→Hω2 : List (Maybe Two) → HOD
 3→Hω2 t = list→hod t 0 where
diff -r 428227847d62 -r ad9ed7c4a0b3 src/Tychonoff1.agda
--- a/src/Tychonoff1.agda	Fri Jun 02 12:12:29 2023 +0900
+++ b/src/Tychonoff1.agda	Sat Jun 03 08:13:50 2023 +0900
@@ -37,28 +37,94 @@
 
 open Filter
 
-Filter-Proj1 : {P Q : HOD } → 
+filter-⊆ : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) →  {x : HOD} → filter F ∋ x  →  { z : Ordinal } 
+    → odef x z → odef (ZFP P Q) z
+filter-⊆ {P} {Q} F {x} fx {z} xz  = f⊆L F fx _ (subst (λ k → odef k z) (sym *iso) xz )
+
+rcp :  {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) → RXCod (filter F) P (λ x fx → ZP-proj1 P Q x (filter-⊆ F fx))
+rcp {P} {Q} F = record { ≤COD = λ {x} fx {z} ly → ZP1.aa ly }
+
+Filter-Proj1 : {P Q a : HOD } → ZFP P Q ∋ a → 
      (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  
       →    Filter {Power P} {P} (λ x → x) 
-Filter-Proj1 = ?
+Filter-Proj1 {P} {Q} pqa F = record { filter = FP ; f⊆L = fp00 ; filter1 = f1 ; filter2 = f2 }  where
+    FP : HOD
+    FP = Replace' (filter F) (λ x fx → ZP-proj1 P Q x (filter-⊆ F fx)) {P} (rcp  F)
+    isP→PxQ : {x : HOD} → (x⊆P : x ⊆ P ) → ZFP x Q ⊆ ZFP P Q
+    isP→PxQ {x} x⊆P (ab-pair p q) = ab-pair (x⊆P p) q
+    isQ→PxQ : {x : HOD} → (x⊆P : x ⊆ Q ) → ZFP P x ⊆ ZFP P Q
+    isQ→PxQ {x} x⊆Q (ab-pair p q) = ab-pair p (x⊆Q q) 
+    fp00 : FP ⊆ Power P 
+    fp00 {x} record { z = z ; az = az ; x=ψz = x=ψz } w xw with subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso ) xw
+    ... | record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } = aa
+    f0 :  {p q : HOD} → Power (ZFP P Q) ∋ q → filter F ∋ p → p ⊆ q → filter F ∋ q
+    f0 {p} {q} PQq fp p⊆q = filter1 F PQq fp p⊆q 
+    f1 :  {p q : HOD} → Power P ∋ q → FP ∋ p → p ⊆ q → FP ∋ q
+    f1 {p} {q} Pq record { z = z ; az = az ; x=ψz = x=ψz } p⊆q = record { z = & (ZFP q Q) ; az = fp01 ty05 ty06 ; x=ψz = q=proj1 } where
+       PQq : Power (ZFP P Q) ∋ ZFP q Q
+       PQq z zpq = isP→PxQ {* (& q)} (Pq _) ( subst (λ k → odef k z ) (trans *iso (cong (λ k → ZFP k Q) (sym *iso))) zpq )
+       q⊆P : q ⊆ P
+       q⊆P {w} qw = Pq _ (subst (λ k → odef k w ) (sym *iso) qw )
+       p⊆P : p ⊆ P
+       p⊆P {w} pw = q⊆P (p⊆q pw)
+       p=proj1 : & p ≡ & (ZP-proj1 P Q (* z) (filter-⊆ F (subst (odef (filter F)) (sym &iso) az)))
+       p=proj1 = x=ψz
+       p⊆ZP : (* z) ⊆ ZFP p Q
+       p⊆ZP = subst (λ k → (* z) ⊆ ZFP k Q) (sym (&≡&→≡ p=proj1)) ZP-proj1⊆ZFP 
+       ty05 : filter F ∋  ZFP p Q
+       ty05 = filter1 F (λ z wz → isP→PxQ p⊆P (subst (λ k → odef k z) *iso wz)) (subst (λ k → odef (filter F) k) (sym &iso) az) p⊆ZP
+       ty06 : ZFP p Q ⊆ ZFP q Q
+       ty06 (ab-pair wp wq ) = ab-pair (p⊆q wp) wq
+       fp01 : filter F ∋ ZFP p Q → ZFP p Q ⊆ ZFP q Q → filter F ∋ ZFP q Q
+       fp01 fzp zp⊆zq = filter1 F PQq fzp zp⊆zq
+       q=proj1 : & q ≡ & (ZP-proj1 P Q (* (& (ZFP q Q))) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (fp01 ty05 ty06))))
+       q=proj1 = cong (&) (ZP-proj1=rev (zp2 pqa) q⊆P *iso )
+    f2 : {p q : HOD} → FP ∋ p → FP ∋ q → Power P ∋ (p ∩ q) → FP ∋ (p ∩ q)
+    f2 {p} {q} record { z = zp ; az = fzp ; x=ψz = x=ψzp } record { z = zq ; az = fzq ; x=ψz = x=ψzq } Ppq 
+         = record { z = _ ; az = ty50 ; x=ψz = pq=proj1 } where
+       p⊆P : {zp : Ordinal} {p : HOD} (fzp : odef (filter F) zp) → ( & p ≡ &
+            (ZP-proj1 P Q (* zp) (filter-⊆ F (subst (odef (filter F)) (sym &iso) fzp)))) → p ⊆ P
+       p⊆P {zp} {p} fzp p=proj1 {x} px with subst (λ k → odef k x) (&≡&→≡ p=proj1) px
+       ... | record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab } = aa
+       x⊆pxq : {zp : Ordinal} {p : HOD} (fzp : odef (filter F) zp) → ( & p ≡ &
+            (ZP-proj1 P Q (* zp) (filter-⊆ F (subst (odef (filter F)) (sym &iso) fzp)))) → * zp ⊆ ZFP p Q
+       x⊆pxq {zp} {p} fzp p=proj1 = subst (λ k → (* zp) ⊆ ZFP k Q) (sym (&≡&→≡ p=proj1)) ZP-proj1⊆ZFP
+       ty54 : Power (ZFP P Q) ∋ (ZFP p Q ∩ ZFP q Q)
+       ty54 z xz = subst (λ k → ZFProduct P Q k ) (zp-iso pqz) (ab-pair pqz1 pqz2 ) where
+         pqz :  odef (ZFP (p ∩ q) Q)  z
+         pqz = subst (λ k → odef k z ) (trans *iso (sym (proj1 ZFP∩) ))  xz
+         pqz1 : odef P (zπ1 pqz)
+         pqz1 = p⊆P fzp x=ψzp (proj1 (zp1 pqz))
+         pqz2 : odef Q (zπ2 pqz)
+         pqz2 = zp2 pqz
+       ty53 : filter F ∋ ZFP p Q
+       ty53 = filter1 F (λ z wz → isP→PxQ (p⊆P fzp x=ψzp)
+         (subst (λ k → odef k z) *iso wz))
+         (subst (λ k → odef (filter F) k) (sym &iso) fzp ) (x⊆pxq fzp x=ψzp)
+       ty52 : filter F ∋ ZFP q Q
+       ty52 = filter1 F (λ z wz → isP→PxQ (p⊆P fzq x=ψzq)
+         (subst (λ k → odef k z) *iso wz))
+         (subst (λ k → odef (filter F) k) (sym &iso) fzq ) (x⊆pxq fzq x=ψzq)
+       ty51 : filter F ∋ ( ZFP p Q ∩ ZFP q Q )
+       ty51 = filter2 F ty53 ty52 ty54
+       ty50 : filter F ∋ ZFP (p ∩ q) Q
+       ty50 = subst (λ k → filter F ∋ k ) (sym (proj1 ZFP∩)) ty51
+       pq=proj1 : & (p ∩ q) ≡ & (ZP-proj1 P Q (* (& (ZFP (p ∩ q) Q))) (filter-⊆ F (subst (odef (filter F)) (sym &iso) ty50)))
+       pq=proj1 = cong (&) (ZP-proj1=rev (zp2 pqa) (λ {x} pqx → Ppq _ (subst (λ k → odef k x) (sym *iso) pqx)) *iso )
 
 Filter-Proj1-UF : {P Q : HOD } → 
      (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  (UF : ultra-filter F)
       →   (FP :  Filter {Power P} {P} (λ x → x) ) →   ultra-filter FP
 Filter-Proj1-UF = ?
 
-filter-⊆ : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) →  {x : HOD} → filter F ∋ x  →  { z : Ordinal } 
-    → odef x z → odef (ZFP P Q) z
-filter-⊆ {P} {Q} F {x} fx {z} xz  = f⊆L F fx _ (subst (λ k → odef k z) (sym *iso) xz )
-
 rcf :  {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x)) → RXCod (filter F) (ZFP Q P) (λ x fx → ZPmirror P Q x (filter-⊆ F fx))
 rcf {P} {Q} F = record { ≤COD = λ {x} fx {z} ly → ZPmirror⊆ZFPBA P Q x (filter-⊆ F fx) ly }
 
-Filter-sym : {P Q a : HOD } → ZFP P Q ∋ a → 
+Filter-sym : {P Q : HOD } → 
      (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  
      → Filter {Power (ZFP Q P)} {ZFP Q P} (λ x → x)
-Filter-sym {P} {Q} {z} pqz F = 
-    record { filter = fqp ; f⊆L = fqp<P ; filter1 = f1 ; filter2 = ? }  where
+Filter-sym {P} {Q} F = 
+    record { filter = fqp ; f⊆L = fqp<P ; filter1 = f1 ; filter2 = f2 }  where
     fqp : HOD
     fqp = Replace' (filter F) (λ x fx → ZPmirror P Q x (filter-⊆ F fx)) {ZFP Q P} (rcf  F)
     fqp<P : fqp ⊆ Power (ZFP Q P)
@@ -67,7 +133,9 @@
             (subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso ) xw) 
     f1 : {p q : HOD} → Power (ZFP Q P) ∋ q → fqp ∋ p → p ⊆ q → fqp ∋ q
     f1 {p} {q} QPq fqp p⊆q = record { z = _ ; az = fis00 {ZPmirror Q P p p⊆ZQP } {ZPmirror Q P q q⊆ZQP } fig01 fig03 fis04 
-      ; x=ψz = ? }  where
+      ; x=ψz = fis05 }  where
+         fis00 : {p q : HOD} → Power (ZFP P Q) ∋ q → filter F ∋ p → p ⊆ q → filter F ∋ q
+         fis00 = filter1 F 
          q⊆ZQP : q ⊆ ZFP Q P
          q⊆ZQP {x} qx = QPq _ (subst (λ k → odef k x) (sym *iso) qx) 
          p⊆ZQP : p ⊆ ZFP Q P
@@ -76,20 +144,44 @@
          fig06 = Replaced1.x=ψz fqp
          fig03 : filter F ∋  ZPmirror Q P p p⊆ZQP
          fig03 with Replaced1.az fqp 
-         ... | fz = subst (λ k → odef (filter F) k ) ?  fz where
-             fig07 :  Replaced1.z fqp ≡ & (ZPmirror Q P p (λ px → QPq x (subst (λ k → def (HOD.od k) x) (sym *iso) (p⊆q px))))
-             fig07 = ?
+         ... | fz = subst (λ k → odef (filter F) k ) fig07  fz where
+             fig07 :  Replaced1.z fqp ≡ & (ZPmirror Q P p (λ {x} px → QPq x (subst (λ k → def (HOD.od k) x ) (sym *iso) (p⊆q px))))
+             fig07 = trans (sym &iso) ( sym (cong (&) (ZPmirror-rev (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) (sym fig06) )))))
          fig01 : Power (ZFP P Q) ∋ ZPmirror Q P q q⊆ZQP
-         fig01 x xz  = ? -- 
-         fis00 : {p q : HOD} → Power (ZFP P Q) ∋ q → filter F ∋ p → p ⊆ q → filter F ∋ q
-         fis00 = filter1 F 
+         fig01 x xz  = ZPmirror⊆ZFPBA Q P q q⊆ZQP (subst (λ k → odef k x) *iso xz)
          fis04 : ZPmirror Q P p (λ z → q⊆ZQP (p⊆q z)) ⊆ ZPmirror Q P q q⊆ZQP
-         fis04 = ? 
+         fis04 = ZPmirror-⊆ p⊆q
          fis05 : & q ≡ & (ZPmirror P Q (* (& (ZPmirror Q P q q⊆ZQP)))
              (filter-⊆ F (subst (odef (filter F)) (sym &iso) (fis00 fig01 fig03 fis04))))
-         fis05 = ?
-
-
+         fis05 = cong (&) (sym ( ZPmirror-rev (sym *iso) ))
+    f2 : {p q : HOD} → fqp ∋ p → fqp ∋ q → Power (ZFP Q P) ∋ (p ∩ q) → fqp ∋ (p ∩ q)
+    f2 {p} {q} fp fq QPpq = record { z = _ ; az = fis12 {ZPmirror Q P p p⊆ZQP} {ZPmirror Q P q q⊆ZQP} fig03 fig04 fig01
+      ; x=ψz = fis05 }  where
+         fis12 : {p q : HOD} → filter F ∋ p → filter F ∋ q → Power (ZFP P Q) ∋ (p ∩ q) → filter F ∋ (p ∩ q)
+         fis12 {p} {q} fp fq PQpq = filter2 F fp fq PQpq
+         p⊆ZQP : p ⊆ ZFP Q P
+         p⊆ZQP {z} px = fqp<P fp _ (subst (λ k → odef k z) (sym *iso) px)
+         q⊆ZQP : q ⊆ ZFP Q P
+         q⊆ZQP {z} qx = fqp<P fq _ (subst (λ k → odef k z) (sym *iso) qx)
+         pq⊆ZQP : (p ∩ q) ⊆ ZFP Q P
+         pq⊆ZQP {z} pqx = QPpq _ (subst (λ k → odef k z) (sym *iso) pqx)
+         fig06 : & p ≡ & (ZPmirror P Q (* (Replaced1.z fp)) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (Replaced1.az fp))))
+         fig06 = Replaced1.x=ψz fp
+         fig09 : & q ≡ & (ZPmirror P Q (* (Replaced1.z fq)) (filter-⊆ F (subst (odef (filter F)) (sym &iso) (Replaced1.az fq))))
+         fig09 = Replaced1.x=ψz fq
+         fig03 : filter F ∋  ZPmirror Q P p p⊆ZQP
+         fig03 = subst (λ k → odef (filter F) k ) fig07 ( Replaced1.az fp )  where
+             fig07 :  Replaced1.z fp ≡ & (ZPmirror Q P p p⊆ZQP )
+             fig07 = trans (sym &iso) ( sym (cong (&) (ZPmirror-rev (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) (sym fig06) )))))
+         fig04 : filter F ∋  ZPmirror Q P q q⊆ZQP
+         fig04 = subst (λ k → odef (filter F) k ) fig08 ( Replaced1.az fq )  where
+             fig08 :  Replaced1.z fq ≡ & (ZPmirror Q P q q⊆ZQP )
+             fig08 = trans (sym &iso) ( sym (cong (&) (ZPmirror-rev (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) (sym fig09) )))))
+         fig01 : Power (ZFP P Q) ∋ ( ZPmirror Q P p p⊆ZQP ∩ ZPmirror Q P q q⊆ZQP )
+         fig01 x xz  = ZPmirror⊆ZFPBA Q P q q⊆ZQP (proj2 (subst (λ k → odef k x) *iso xz))
+         fis05 : & (p ∩ q) ≡ & (ZPmirror P Q (* (& (ZPmirror Q P p p⊆ZQP ∩ ZPmirror Q P q q⊆ZQP))) 
+             (filter-⊆ F (subst (odef (filter F)) (sym &iso) (fis12 fig03 fig04 fig01) )))
+         fis05 = cong (&) (sym ( ZPmirror-rev {Q} {P} {_} {_} {pq⊆ZQP} (trans ZPmirror-∩ (sym *iso) ) ))
 
 Filter-sym-UF : {P Q : HOD } → 
      (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  (UF : ultra-filter F)
@@ -100,5 +192,5 @@
 Filter-Proj2 : {P Q a : HOD } → ZFP P Q ∋ a → 
      (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  
       →    Filter {Power Q} {Q} (λ x → x) 
-Filter-Proj2 {P} {Q} {a} pqa F = Filter-Proj1 {Q} {P} (Filter-sym pqa F )
+Filter-Proj2 {P} {Q} {a} pqa F = Filter-Proj1 {Q} {P} ? (Filter-sym F )
 
diff -r 428227847d62 -r ad9ed7c4a0b3 src/ZProduct.agda
--- a/src/ZProduct.agda	Fri Jun 02 12:12:29 2023 +0900
+++ b/src/ZProduct.agda	Sat Jun 03 08:13:50 2023 +0900
@@ -242,6 +242,41 @@
             * x ≡⟨ sym (cong (*) (ty32 pp qx  )) ⟩
             * (zπ2 (subst (odef (ZFP P Q)) (sym &iso) (ab-pair pp qx  ))) ∎ where open ≡-Reasoning
 
+record ZP1 (A B C : HOD) ( cab : C ⊆ ZFP A B ) (a : Ordinal) : Set n where
+    field
+       b : Ordinal
+       aa : odef A a
+       bb : odef B b
+       c∋ab : odef C (& < * a , * b > )
+
+ZP-proj1 : (A B C : HOD) → C  ⊆ ZFP A B → HOD
+ZP-proj1 A B C cab = record { od = record { def = λ x → ZP1 A B C cab x } ; odmax = & A ; <odmax = λ lt → odef< (ZP1.aa lt) } 
+
+ZP-proj1⊆ZFP : {A B C : HOD} → {cab : C ⊆ ZFP A B} → C ⊆ ZFP (ZP-proj1 A B C cab) B
+ZP-proj1⊆ZFP {A} {B} {C} {cab} {c} cc with cab cc
+... | ab-pair {a} {b} aa bb = ab-pair record { b = _ ; aa = aa ; bb = bb ; c∋ab = cc }  bb
+
+ZP-proj1=rev : {A B a m : HOD} {b : Ordinal } → {cab : m ⊆ ZFP A B} → odef B b → a ⊆ A → m ≡ ZFP a B → a ≡ ZP-proj1 A B m cab 
+ZP-proj1=rev {A} {B} {a} {m} {b} {cab} bb a⊆A refl = ==→o≡ record { eq→ = zp00 ; eq← = zp01 } where
+     zp00 : {x : Ordinal } → odef a x → ZP1 A B (ZFP a B) cab x
+     zp00 {x} ax = record { b = _ ; aa = a⊆A ax ; bb = bb ; c∋ab = ab-pair ax bb  }  
+     zp01 : {x : Ordinal } → ZP1 A B (ZFP a B) cab x → odef a x
+     zp01 {x} record { b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab }  = zp02 c∋ab refl where
+        zp02 : {z : Ordinal } → odef (ZFP a B) z → z ≡ & < * x , * b > → odef a x
+        zp02 {.(& < * _ , * _ >)} (ab-pair {a1} {b1} aa1 bb1) eq = subst (λ k → odef a k) (*≡*→≡ zp03) aa1 where
+           zp03 : * a1 ≡ * x
+           zp03 = proj1 (prod-≡ (&≡&→≡ eq))
+
+record ZP2 (A B C : HOD) ( cab : C ⊆ ZFP A B ) (b : Ordinal) : Set n where
+    field
+       a : Ordinal
+       aa : odef A a
+       bb : odef B b
+       c∋ab : odef C (& < * a , * b > )
+
+ZP-proj2 : (A B C : HOD) → C  ⊆ ZFP A B → HOD
+ZP-proj2 A B C cab = record { od = record { def = λ x → ZP2 A B C cab x } ; odmax = & B ; <odmax = λ lt → odef< (ZP2.bb lt) } 
+
 record Func (A B : HOD) : Set n where
     field
        func : {x : Ordinal } → odef A x → Ordinal
@@ -392,6 +427,48 @@
         zs02 = cong₂ (λ j k → & < j , k >) (sym (proj2 (prod-≡ (subst₂ (λ j k → j ≡ k) *iso  *iso  (cong (*) x=ba)))))  
                                            (sym (proj1 (prod-≡ (subst₂ (λ j k → j ≡ k) *iso  *iso  (cong (*) x=ba))))) 
 
+ZPmirror-rev : {A B C m : HOD}  → {cab : C  ⊆ ZFP A B } → ZPmirror A B C cab ≡ m 
+       → {m⊆Z : m ⊆ ZFP B A } → ZPmirror B A m m⊆Z   ≡ C  
+ZPmirror-rev {A} {B} {C} {m} {cab} eq {m⊆Z} = ==→o≡ record { eq→  = zs02 ; eq← = zs04 } where
+    zs02 : {x : Ordinal} → ZPC B A m m⊆Z x → odef C x
+    zs02 {x} record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab ; x=ba = x=ba } with subst (λ k → odef k (& < * a , * b > )) (sym eq) c∋ab 
+    ... | record { a = b1 ; b = a1 ; aa = bb1 ; bb = aa1 ; c∋ab = c∋ab1 ; x=ba = x=ba1 } = subst (λ k → odef C k) zs03  c∋ab1 where
+        a=a1 : * a ≡ * a1 
+        a=a1 = proj1 (prod-≡ (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) x=ba1)))
+        b=b1 : * b ≡ * b1 
+        b=b1 = proj2 (prod-≡ (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) x=ba1)))
+        zs03 : & < * b1 , * a1 > ≡ x
+        zs03 = begin
+          & < * b1 , * a1 > ≡⟨ cong₂ (λ j k → & < j , k >) (sym b=b1) (sym a=a1)  ⟩ 
+          & < * b , * a > ≡⟨ sym x=ba ⟩ 
+          x ∎ where open ≡-Reasoning
+    zs04 : {x : Ordinal} → odef C x → ZPC B A m m⊆Z x 
+    zs04 {x} cx with cab cx 
+    ... | ab-pair {a} {b} aa bb  = record { a = b ; b = a ; aa = bb ; bb = aa 
+      ; c∋ab = subst (λ k → odef k (& < * b , * a >)) eq zs05 ; x=ba = refl } where
+        zs05 : odef (ZPmirror A B C cab)  (& < * b , * a >)
+        zs05 = record { a = _ ; b = _ ; aa = aa ; bb = bb ; c∋ab = cx ; x=ba = refl } 
+
+ZPmirror-⊆ : {A B C D : HOD}  → (C⊆D : C ⊆ D) → {cab : C  ⊆ ZFP A B } {dab : D  ⊆ ZFP A B } → ZPmirror A B C cab ⊆ ZPmirror A B D dab
+ZPmirror-⊆ {A} {B} {C} {D} C⊆D {cab} {dab} {x} record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab ; x=ba = x=ba } = 
+        record { a = _ ; b = _ ; aa = aa ; bb = bb ; c∋ab = C⊆D c∋ab ; x=ba = x=ba } 
+
+ZPmirror-∩ : {A B C D : HOD}  → {cdab : (C ∩ D) ⊆ ZFP A B } {cab : C  ⊆ ZFP A B } {dab : D  ⊆ ZFP A B } 
+        → ZPmirror A B (C ∩ D) cdab ≡ ZPmirror A B C cab ∩ ZPmirror A B D dab
+ZPmirror-∩ {A} {B} {C} {D} {cdab} {cab} {dab} = ==→o≡ record { eq→ = za06 ; eq← = za07 } where
+        za06 :  ZPmirror A B (C ∩ D) cdab ⊆ ( ZPmirror A B C cab ∩ ZPmirror A B D dab )
+        za06 {x} record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab ; x=ba = x=ba } = ⟪
+             record { a = _ ; b = _ ; aa = aa ; bb = bb ; c∋ab = proj1 c∋ab ; x=ba = x=ba } ,
+             record { a = _ ; b = _ ; aa = aa ; bb = bb ; c∋ab = proj2 c∋ab ; x=ba = x=ba } ⟫
+        za07 :  ( ZPmirror A B C cab ∩ ZPmirror A B D dab ) ⊆ ZPmirror A B (C ∩ D) cdab 
+        za07 {x} ⟪ record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = c∋ab1 ; x=ba = x=ba } ,
+             record { a = a' ; b = b' ; aa = aa' ; bb = bb' ; c∋ab = c∋ab2 ; x=ba = x=ba' } ⟫ =
+             record { a = a ; b = b ; aa = aa ; bb = bb ; c∋ab = ⟪ c∋ab1 , subst (λ k → odef D k) (sym zs02) c∋ab2 ⟫ ; x=ba = x=ba } where
+            zs02 : & < * a , * b > ≡ & < * a' , * b' >
+            zs02 = cong₂ (λ j k → & < j , k >) (sym (proj2 (prod-≡ (subst₂ (λ j k → j ≡ k) *iso  *iso  (cong (*) (trans (sym x=ba') x=ba))))))  
+                                           (sym (proj1 (prod-≡ (subst₂ (λ j k → j ≡ k) *iso  *iso  (cong (*) (trans (sym x=ba') x=ba)))))) 
+
+
 ZFP∩  : {A B C : HOD} → ( ZFP (A ∩ B) C ≡ ZFP A C ∩ ZFP B C ) ∧ ( ZFP C (A ∩ B) ≡ ZFP C A  ∩ ZFP C B )
 proj1 (ZFP∩ {A} {B} {C} ) = ==→o≡ record { eq→ = zfp00  ; eq← = zfp01 } where
    zfp00 : {x : Ordinal} → ZFProduct (A ∩ B) C x → odef (ZFP A C ∩ ZFP B C) x