# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1678067134 -32400
# Node ID 362e43a1477c33c9afdc37529e70eca525951934
# Parent  287d40830be583aa0491e53e55eb18c70f07cc8e
brain damaged fix

diff -r 287d40830be5 -r 362e43a1477c src/OD.agda
--- a/src/OD.agda	Sun Mar 05 23:49:10 2023 +0900
+++ b/src/OD.agda	Mon Mar 06 10:45:34 2023 +0900
@@ -90,6 +90,8 @@
 
 open HOD
 
+open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
+
 record ODAxiom : Set (suc n) where
  field
   -- HOD is isomorphic to Ordinal (by means of Goedel number)
@@ -102,10 +104,10 @@
   ==→o≡  :  {x y : HOD  }   → (od x == od y) → x ≡ y
   sup-o  :  (A : HOD) → (     ( x : Ordinal ) → def (od A) x →  Ordinal ) →  Ordinal -- required in Replace
   sup-o≤ :  (A : HOD) → { ψ : ( x : Ordinal ) → def (od A) x →  Ordinal } → ∀ {x : Ordinal } → (lt : def (od A) x ) → ψ x lt o≤  sup-o A ψ
+  ∋-irr : {X : HOD} {x : Ordinal } → (a b : def (od X) x) → a ≅ b
 -- possible order restriction (required in the axiom of infinite )
   ho< : {x : HOD} → & x o< next (odmax x)
 
-
 postulate  odAxiom : ODAxiom
 open ODAxiom odAxiom
 
@@ -369,7 +371,7 @@
       az : odef A z
       x=ψz  : x ≡ ψ z az
 
-Replace' : (X : HOD)  → ((x : HOD) → X ∋ x → HOD) → HOD
+Replace' : (X : HOD) → ((x : HOD) → X ∋ x → HOD) → HOD
 Replace' X ψ = record { od = record { def = λ x → Replaced1 X (λ z xz → & (ψ (* z) (subst (λ k → odef X k) (sym &iso) xz) )) x  } ; odmax = rmax ; <odmax = rmax< } where
         rmax : Ordinal
         rmax = osuc ( sup-o X (λ y X∋y → & (ψ (* y) (d→∋ X X∋y) )) )
@@ -378,6 +380,26 @@
             r01 : & (ψ ( * (Replaced1.z lt ) ) (subst (λ k → odef X k) (sym &iso) (Replaced1.az lt) )) ≡ y
             r01 = sym (Replaced1.x=ψz lt )
 
+
+Replace'-iso : (X : HOD) → (ψ : (x : HOD) → X ∋ x → HOD) → 
+      Replace' (* (& X)) (λ y xy → ψ y (subst (λ k → k ∋ y ) *iso xy) ) ≡ Replace' X ( λ y xy → ψ y xy ) 
+Replace'-iso X ψ = ==→o≡ record { eq→ = ri0 ; eq← = ri1 } where
+    ri2 : {z : Ordinal } (a b : X ∋ (* z)) → & (ψ (* z) a) ≡ & (ψ (* z) b)
+    ri2 {z} a b = cong (λ k → & (ψ (* z) k)) ( HE.≅-to-≡ ( ∋-irr {X} {& (* z)} a b ) )
+    ri0 : {x : Ordinal} 
+        → Replaced1 (* (& X)) (λ z xz → & (ψ (* z) (subst (λ k → k ∋ * z) *iso (subst (odef (* (& X))) (sym &iso) xz)))) x 
+        → Replaced1 X (λ z xz → & (ψ (* z) (subst (odef X) (sym &iso) xz))) x
+    ri0 {x} record { z = z ; az = az ; x=ψz = refl } = record { z = z ; az = subst (λ k → odef k z) *iso az 
+       ; x=ψz = ri2 (subst (λ k → k ∋ * z) *iso (subst (odef (* (& X))) (sym &iso) az))  
+                    (subst (odef X) (sym &iso) (subst (λ k → odef k z) *iso az) ) }  
+    ri1 : {x : Ordinal} 
+        → Replaced1 X (λ z xz → & (ψ (* z) (subst (odef X) (sym &iso) xz))) x
+        → Replaced1 (* (& X)) (λ z xz → & (ψ (* z) (subst (λ k → k ∋ * z) *iso (subst (odef (* (& X))) (sym &iso) xz)))) x 
+    ri1 {x} record { z = z ; az = az ; x=ψz = refl } = record { z = z ; az = subst (λ k → odef k z) (sym *iso) az 
+       ; x=ψz = ri2 (subst (λ k → odef X k) (sym &iso) az  )   -- brain damaged below
+           (subst (λ k → k ∋ * z) *iso (subst (odef (* (& X))) (sym &iso) (subst (λ k → odef k z) (sym *iso) az))) } 
+
+
 -- replacement←1 : {ψ : HOD → HOD} (X x : HOD) →  X ∋ x → Replace1 X ψ ∋ ψ x
 -- replacement←1 {ψ} X x lt = record { z = & x ; az = lt  ; x=ψz = cong (λ k → & (ψ k)) (sym *iso) }
 -- replacement→1 : {ψ : HOD → HOD} (X x : HOD) → (lt : Replace1 X ψ ∋ x) → ¬ ( (y : HOD) → ¬ (x =h= ψ y))
diff -r 287d40830be5 -r 362e43a1477c src/OPair.agda
--- a/src/OPair.agda	Sun Mar 05 23:49:10 2023 +0900
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,256 +0,0 @@
-{-# OPTIONS --allow-unsolved-metas #-}
-
-open import Level
-open import Ordinals
-module OPair {n : Level } (O : Ordinals {n})   where
-
-open import zf
-open import logic
-import OD 
-import ODUtil
-import OrdUtil
-
-open import Relation.Nullary
-open import Relation.Binary
-open import Data.Empty
-open import Relation.Binary
-open import Relation.Binary.Core
-open import  Relation.Binary.PropositionalEquality
-open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
-
-open OD O
-open OD.OD
-open OD.HOD
-open ODAxiom odAxiom
-
-open Ordinals.Ordinals  O
-open Ordinals.IsOrdinals isOrdinal
-open Ordinals.IsNext isNext
-open OrdUtil O
-open ODUtil O
-
-open _∧_
-open _∨_
-open Bool
-
-open _==_
-
-<_,_> : (x y : HOD) → HOD
-< x , y > = (x , x ) , (x , y )
-
-exg-pair : { x y : HOD } → (x , y ) =h= ( y , x )
-exg-pair {x} {y} = record { eq→ = left ; eq← = right } where
-    left : {z : Ordinal} → odef (x , y) z → odef (y , x) z 
-    left (case1 t) = case2 t
-    left (case2 t) = case1 t
-    right : {z : Ordinal} → odef (y , x) z → odef (x , y) z 
-    right (case1 t) = case2 t
-    right (case2 t) = case1 t
-
-ord≡→≡ : { x y : HOD } → & x ≡ & y → x ≡ y
-ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) *iso *iso ( cong ( λ k → * k ) eq )
-
-od≡→≡ : { x y : Ordinal } → * x ≡ * y → x ≡ y
-od≡→≡ eq = subst₂ (λ j k → j ≡ k ) &iso &iso ( cong ( λ k → & k ) eq )
-
-eq-prod : { x x' y y' : HOD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' >
-eq-prod refl refl = refl
-
-xx=zy→x=y : {x y z : HOD } → ( x , x ) =h= ( z , y ) → x ≡ y
-xx=zy→x=y {x} {y} eq with trio< (& x) (& y) 
-xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c with eq← eq {& y} (case2 refl) 
-xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c | case1 s = ⊥-elim ( o<¬≡ (sym s) a )
-xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c | case2 s = ⊥-elim ( o<¬≡ (sym s) a )
-xx=zy→x=y {x} {y} eq | tri≈ ¬a b ¬c = ord≡→≡ b
-xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c  with eq← eq {& y} (case2 refl) 
-xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c | case1 s = ⊥-elim ( o<¬≡ s c )
-xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c | case2 s = ⊥-elim ( o<¬≡ s c )
-
-prod-eq : { x x' y y' : HOD } → < x , y > =h= < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' )
-prod-eq {x} {x'} {y} {y'} eq = ⟪ lemmax , lemmay ⟫ where
-    lemma2 : {x y z : HOD } → ( x , x ) =h= ( z , y ) → z ≡ y
-    lemma2 {x} {y} {z} eq = trans (sym (xx=zy→x=y lemma3 )) ( xx=zy→x=y eq )  where
-        lemma3 : ( x , x ) =h= ( y , z )
-        lemma3 = ==-trans eq exg-pair
-    lemma1 : {x y : HOD } → ( x , x ) =h= ( y , y ) → x ≡ y
-    lemma1 {x} {y} eq with eq← eq {& y} (case2 refl)
-    lemma1 {x} {y} eq | case1 s = ord≡→≡ (sym s)
-    lemma1 {x} {y} eq | case2 s = ord≡→≡ (sym s)
-    lemma4 : {x y z : HOD } → ( x , y ) =h= ( x , z ) → y ≡ z
-    lemma4 {x} {y} {z} eq with eq← eq {& z} (case2 refl)
-    lemma4 {x} {y} {z} eq | case1 s with ord≡→≡ s -- x ≡ z
-    ... | refl with lemma2 (==-sym eq )
-    ... | refl = refl
-    lemma4 {x} {y} {z} eq | case2 s = ord≡→≡ (sym s) -- y ≡ z
-    lemmax : x ≡ x'
-    lemmax with eq→ eq {& (x , x)} (case1 refl) 
-    lemmax | case1 s = lemma1 (ord→== s )  -- (x,x)≡(x',x')
-    lemmax | case2 s with lemma2 (ord→== s ) -- (x,x)≡(x',y') with x'≡y'
-    ... | refl = lemma1 (ord→== s )
-    lemmay : y ≡ y'
-    lemmay with lemmax
-    ... | refl with lemma4 eq -- with (x,y)≡(x,y')
-    ... | eq1 = lemma4 (ord→== (cong (λ  k → & k )  eq1 ))
-
-prod-≡ : { x x' y y' : HOD } → < x , y > ≡ < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' )
-prod-≡ eq = prod-eq (ord→== (cong (&) eq ))
-
---
--- unlike ordered pair, ZFPair is not a HOD
-
-data ord-pair : (p : Ordinal) → Set n where
-   pair : (x y : Ordinal ) → ord-pair ( & ( < * x , * y > ) )
-
-ZFPair : OD
-ZFPair = record { def = λ x → ord-pair x }
-
--- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
--- eq-pair : { x x' y y' : Ordinal } → x ≡ x' → y ≡ y' → pair x y ≅ pair x' y'
--- eq-pair refl refl = HE.refl
-
-pi1 : { p : Ordinal } →   ord-pair p →  Ordinal
-pi1 ( pair x y) = x
-
-π1 : { p : HOD } → def ZFPair (& p) → HOD
-π1 lt = * (pi1 lt )
-
-pi2 : { p : Ordinal } →   ord-pair p →  Ordinal
-pi2 ( pair x y ) = y
-
-π2 : { p : HOD } → def ZFPair (& p) → HOD
-π2 lt = * (pi2 lt )
-
-op-cons :  ( ox oy  : Ordinal ) → def ZFPair (& ( < * ox , * oy >   ))
-op-cons ox oy = pair ox oy
-
-def-subst :  {Z : OD } {X : Ordinal  }{z : OD } {x : Ordinal  }→ def Z X → Z ≡ z  →  X ≡ x  →  def z x
-def-subst df refl refl = df
-
-p-cons :  ( x y  : HOD ) → def ZFPair (& ( < x , y >))
-p-cons x y = def-subst {_} {_} {ZFPair} {& (< x , y >)} (pair (& x) ( & y )) refl (
-   let open ≡-Reasoning in begin
-       & < * (& x) , * (& y) >
-   ≡⟨ cong₂ (λ j k → & < j , k >) *iso *iso ⟩
-       & < x , y >
-   ∎ ) 
-
-op-iso :  { op : Ordinal } → (q : ord-pair op ) → & < * (pi1 q) , * (pi2 q) > ≡ op
-op-iso (pair ox oy) = refl
-
-p-iso :  { x  : HOD } → (p : def ZFPair (&  x) ) → < π1 p , π2 p > ≡ x
-p-iso {x} p = ord≡→≡ (op-iso p) 
-
-p-pi1 :  { x y : HOD } → (p : def ZFPair (&  < x , y >) ) →  π1 p ≡ x
-p-pi1 {x} {y} p = proj1 ( prod-eq ( ord→== (op-iso p) ))
-
-p-pi2 :  { x y : HOD } → (p : def ZFPair (&  < x , y >) ) →  π2 p ≡ y
-p-pi2 {x} {y} p = proj2 ( prod-eq ( ord→== (op-iso p)))
-
-_⊗_ : (A B : HOD) → HOD
-A ⊗ B  = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) ))
-
-product→ : {A B a b : HOD} → A ∋ a → B ∋ b  → ( A ⊗ B ) ∋ < a , b >
-product→ {A} {B} {a} {b} A∋a B∋b = record { owner = _ ; ao = lemma1 ; ox = subst (λ k → odef k _) (sym *iso) lemma2  } where
-    lemma1 :  odef (Replace B (λ b₁ → Replace A (λ a₁ → < a₁ , b₁ >))) (& (Replace A (λ a₁ → < a₁ , b >)))
-    lemma1 = replacement← B b B∋b
-    lemma2 : odef (Replace A (λ a₁ → < a₁ , b >)) (& < a , b >)
-    lemma2 = replacement← A a A∋a
-
-x<nextA : {A x : HOD} → A ∋ x →  & x o< next (odmax A)
-x<nextA {A} {x} A∋x = ordtrans (c<→o< {x} {A} A∋x) ho<
-
-A<Bnext : {A B x : HOD} → & A o< & B → A ∋ x → & x o< next (odmax B)
-A<Bnext {A} {B} {x} lt A∋x = osucprev (begin
-          osuc (& x)  
-       <⟨ osucc (c<→o< A∋x) ⟩
-          osuc (& A)
-       <⟨ osucc lt ⟩
-          osuc (& B)
-       <⟨ osuc<nx ho<  ⟩
-          next (odmax B)
-       ∎ ) where open o≤-Reasoning O
-
-data ZFProduct  (A B : HOD) : (p : Ordinal) → Set n where
-    ab-pair : {a b : Ordinal } → odef A a → odef B b → ZFProduct A B ( & ( < * a , * b > ) )
-
-ZFP  : (A B : HOD) → HOD
-ZFP  A B = record { od = record { def = λ x → ZFProduct A B x  } 
-        ; odmax = odmax ( A ⊗ B ) ; <odmax = λ {y} px → <odmax ( A ⊗ B ) (lemma0 px) }  
-   where
-        lemma0 :  {A B : HOD} {x : Ordinal} → ZFProduct A B x → odef (A ⊗ B) x
-        lemma0 {A} {B} {px} ( ab-pair {a} {b} ax by ) = product→ (d→∋ A ax) (d→∋ B by)
-
-ZFP→ : {A B a b : HOD} → A ∋ a → B ∋ b  → ZFP A B ∋ < a , b >
-ZFP→ {A} {B} {a} {b} aa bb = subst (λ k → ZFProduct A B k ) (cong₂ (λ j k → & < j , k >) *iso *iso ) ( ab-pair aa bb ) 
-
-zπ1 : {A B : HOD} → {x : Ordinal } → odef (ZFP A B) x → Ordinal
-zπ1 {A} {B} {.(& < * _ , * _ >)} (ab-pair {a} {b} aa bb) = a
-
-zp1 : {A B : HOD} → {x : Ordinal } → (zx : odef (ZFP A B) x) → odef A (zπ1 zx)
-zp1 {A} {B} {.(& < * _ , * _ >)} (ab-pair {a} {b} aa bb ) = aa
-
-zπ2 : {A B : HOD} → {x : Ordinal } → odef (ZFP A B) x → Ordinal
-zπ2 (ab-pair {a} {b} aa bb) = b
-
-zp2 : {A B : HOD} → {x : Ordinal } → (zx : odef (ZFP A B) x) → odef B (zπ2 zx)
-zp2 {A} {B} {.(& < * _ , * _ >)} (ab-pair {a} {b} aa bb ) = bb
-
-zp-iso :  { A B : HOD } → {x : Ordinal } → (p : odef (ZFP A B) x ) → & < * (zπ1 p) , * (zπ2 p) > ≡ x
-zp-iso {A} {B} {_} (ab-pair {a} {b} aa bb)  = refl
-
-zp-iso1 :  { A B : HOD } → {a b : Ordinal } → (p : odef (ZFP A B) (& < * a , * b > )) → (* (zπ1 p) ≡ (* a)) ∧ (* (zπ2 p) ≡ (* b))
-zp-iso1 {A} {B} {a} {b} pab = prod-≡ (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) zz11) ) where
-      zz11 : & < * (zπ1 pab) , * (zπ2 pab) > ≡ & < * a , * b >
-      zz11 = zp-iso pab
-
-ZFP⊆⊗ :  {A B : HOD} {x : Ordinal} → odef (ZFP A B) x → odef (A ⊗ B) x
-ZFP⊆⊗ {A} {B} {px} ( ab-pair {a} {b} ax by ) = product→ (d→∋ A ax) (d→∋ B by)
-
-⊗⊆ZFPair : {A B x : HOD} → ( A ⊗ B ) ∋ x → def ZFPair (& x)
-⊗⊆ZFPair {A} {B} {x} record { owner = owner ; ao = record { z = a ; az = aa ; x=ψz = x=ψa } ; ox = ox } = zfp01 where
-       zfp02 : Replace A (λ z → < z , * a >) ≡ * owner
-       zfp02 = subst₂ ( λ j k → j ≡ k ) *iso refl (sym (cong (*) x=ψa ))
-       zfp01 : def ZFPair (& x)
-       zfp01 with subst (λ k → odef k (& x) ) (sym zfp02) ox
-       ... | record { z = b ; az = ab ; x=ψz = x=ψb } = subst (λ  k → def ZFPair  k) (cong (&) zfp00) (op-cons b a )  where
-           zfp00 : < * b , * a > ≡ x
-           zfp00 = sym ( subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) x=ψb) )
-
-⊗⊆ZFP : {A B x : HOD} → ( A ⊗ B ) ∋ x → odef (ZFP A B) (& x)
-⊗⊆ZFP {A} {B} {x} record { owner = owner ; ao = record { z = a ; az = ba ; x=ψz = x=ψa } ; ox = ox } = zfp01 where
-       zfp02 : Replace A (λ z → < z , * a >) ≡ * owner
-       zfp02 = subst₂ ( λ j k → j ≡ k ) *iso refl (sym (cong (*) x=ψa ))
-       zfp01 : odef (ZFP A B) (& x)
-       zfp01 with subst (λ k → odef k (& x) ) (sym zfp02) ox
-       ... | record { z = b ; az = ab ; x=ψz = x=ψb } = subst (λ k → ZFProduct A B k ) (sym x=ψb) (ab-pair ab ba) 
-
-ZFPproj1 : {A B X : HOD} → X ⊆ ZFP A B  → HOD
-ZFPproj1 {A} {B} {X} X⊆P = Replace' X ( λ x px → * (zπ1 (X⊆P px) )) 
-
-ZFPproj2 : {A B X : HOD} → X ⊆ ZFP A B  → HOD
-ZFPproj2 {A} {B} {X} X⊆P = Replace' X ( λ x px → * (zπ2 (X⊆P px) )) 
-
--- simple version 
-
-record ZProj1 (L : HOD) (x : Ordinal) : Set n where 
-    field
-        pq : Ordinal
-        opq : ord-pair pq
-        Lpq : odef L pq    
-        x=pi1 : x ≡ pi1 opq
-
--- LP' = Replace' L ( λ p lp → ZFPproj1 {P} {Q} {p} (λ {x} px → (LPQ lp _ (subst (λ k → odef k x) (sym *iso) px  ) )))           
-
-Proj1 : (L P Q : HOD) → HOD
-Proj1 L P Q = record { od = record { def = λ x → odef P x ∧ ZProj1 L x } ; odmax = & P ; <odmax = odef∧< }
-   
-record ZProj2 (L : HOD) (x : Ordinal) : Set n where 
-    field
-        pq : Ordinal
-        opq : ord-pair pq
-        Lpq : odef L pq    
-        x=pi2 : x ≡ pi2 opq
-
-Proj2 : (L P Q : HOD) → HOD
-Proj2 L P Q = record { od = record { def = λ x → odef Q x ∧ ZProj2 L x } ; odmax = & Q ; <odmax = odef∧< }
-   
diff -r 287d40830be5 -r 362e43a1477c src/PFOD.agda
--- a/src/PFOD.agda	Sun Mar 05 23:49:10 2023 +0900
+++ b/src/PFOD.agda	Mon Mar 06 10:45:34 2023 +0900
@@ -51,8 +51,7 @@
 open import Data.List hiding (filter)
 open import Data.Maybe 
 
-import OPair
-open OPair O
+open import ZProduct O
 
 data Hω2 :  (i : Nat) ( x : Ordinal  ) → Set n where
   hφ :  Hω2 0 o∅
diff -r 287d40830be5 -r 362e43a1477c src/Topology.agda
--- a/src/Topology.agda	Sun Mar 05 23:49:10 2023 +0900
+++ b/src/Topology.agda	Mon Mar 06 10:45:34 2023 +0900
@@ -34,7 +34,7 @@
 open ODC O
 
 open import filter O
-open import OPair O
+open import ZProduct O
 
 record Topology  ( L : HOD ) : Set (suc n) where
    field
diff -r 287d40830be5 -r 362e43a1477c src/Tychonoff.agda
--- a/src/Tychonoff.agda	Sun Mar 05 23:49:10 2023 +0900
+++ b/src/Tychonoff.agda	Mon Mar 06 10:45:34 2023 +0900
@@ -33,7 +33,7 @@
 open ODC O
 
 open import filter O
-open import OPair O
+open import ZProduct O
 open import Topology O
 -- open import maximum-filter O
 
@@ -312,6 +312,11 @@
 
 -- product topology of compact topology is compact
 
+import Axiom.Extensionality.Propositional
+postulate f-extensionality : { n m : Level}  → Axiom.Extensionality.Propositional.Extensionality n m
+open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
+
+
 Tychonoff : {P Q : HOD } → (TP : Topology P) → (TQ : Topology Q)  → Compact TP → Compact TQ   → Compact (ProductTopology TP TQ)
 Tychonoff {P} {Q} TP TQ CP CQ = FIP→Compact (ProductTopology TP TQ) (UFLP→FIP (ProductTopology TP TQ) uflPQ ) where
      uflP : (F : Filter {Power P} {P} (λ x → x))  (UF : ultra-filter F)
@@ -330,11 +335,19 @@
          ... | case2 flp = subst (λ k → odef (filter F) k) (cong (&) (==→o≡ fl20))  flp where
              fl20 :  (ZFP P Q ＼ Ord o∅) =h=  ZFP P Q
              fl20 = record { eq→ = λ {x} lt → proj1 lt ; eq← = λ {x} lt → ⟪ lt , (λ lt → ⊥-elim (¬x<0 lt) )  ⟫  }
-         0<P : o∅ o< & (ZFP P Q)
-         0<P with trio< o∅ (& (ZFP P Q))
+         0<PQ : o∅ o< & (ZFP P Q)
+         0<PQ with trio< o∅ (& (ZFP P Q))
          ... | tri< a ¬b ¬c = a
          ... | tri≈ ¬a b ¬c = ⊥-elim (ultra-filter.proper UF (subst (λ k → odef (filter F) k) (trans (sym b) (sym ord-od∅)) F∋PQ) )
          ... | tri> ¬a ¬b c = ⊥-elim (¬x<0 c)
+         apq : HOD
+         apq = ODC.minimal O (ZFP P Q) (0<P→ne 0<PQ)
+         is-apq : ZFP P Q ∋ apq
+         is-apq = ODC.x∋minimal O (ZFP P Q) (0<P→ne 0<PQ)
+         ap : odef P ( zπ1 is-apq  )
+         ap = zp1 is-apq
+         aq : odef Q ( zπ2 is-apq  )
+         aq = zp2 is-apq
          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
          F⊆pxq : {x : HOD } → filter F ∋ x →  x ⊆ ZFP P Q
@@ -366,16 +379,28 @@
                  ty12 = begin
                     * x ≡⟨ sym (cong (*) (ty32 px qq )) ⟩
                     * (zπ1 (F⊆pxq fp (subst (odef (ZFP p Q)) (sym &iso) (ab-pair px qq )))) ∎ where open ≡-Reasoning
-                   
+          
+
          FPSet : HOD
          FPSet = Replace' (filter F) (λ x fx → Replace' x ( λ y xy → * (zπ1 (F⊆pxq fx xy) )))
          FPSet∋zpq : {q : HOD} → q ⊆ P → filter F ∋  ZFP q Q → FPSet ∋ q
          FPSet∋zpq {q} q⊆P fq = record { z = _ ; az = fq ; x=ψz = sym (cong (&) ty10) } where
+              -- brain damaged one
+              ty11 : {y : HOD} {xy : (* (& (ZFP q Q))) ∋ y } → 
+                 * (zπ1 ( (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) ≡ * (zπ1 ( (F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy)  )))
+              ty11 {y} {xy}  = cong (λ k → * (zπ1 k)) ( HE.≅-to-≡ (∋-irr {ZFP P Q} a b )) where
+                 a = F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy
+                 b = F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy)  
               ty10 : Replace' (* (& (ZFP q Q))) (λ y xy → * (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) ≡ q
               ty10 = begin
-                  Replace' (* (& (ZFP q Q))) (λ y xy → * (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) ≡⟨ ? ⟩
+                  Replace' (* (& (ZFP q Q))) (λ y xy → * (zπ1 (F⊆pxq (subst (odef (filter F)) (sym &iso) fq) xy))) 
+                     ≡⟨ 
+                  cong (λ k → Replace' (* (& (ZFP q Q))) k ) (f-extensionality (λ y → (f-extensionality (λ xy → ty11 {y} {xy}))))
+                      ⟩
+                  Replace' (* (& (ZFP q Q))) (λ y xy → * (zπ1 (F⊆pxq fq (subst (λ k → odef k (& y)) *iso xy)  ))) 
+                     ≡⟨ Replace'-iso _  ( λ y xy → * (zπ1 (F⊆pxq fq xy) )) ⟩
                   Replace' (ZFP q Q) ( λ y xy → * (zπ1 (F⊆pxq fq xy) )) ≡⟨ refl ⟩ 
-                  fx→px fq ≡⟨ fx→px1 ? fq  ⟩
+                  fx→px fq ≡⟨ fx→px1 aq fq  ⟩
                   q ∎ where open ≡-Reasoning
          FPSet⊆PP :  FPSet  ⊆ Power P
          FPSet⊆PP {x} record { z = z ; az = fz ; x=ψz = x=ψz } w xw with subst (λ k → odef k w) (trans (cong (*) x=ψz) *iso) xw
@@ -383,7 +408,7 @@
             = subst (λ k → odef P k) (sym (trans x=ψz1 &iso)) 
                (zp1 (F⊆pxq (subst (λ k → odef (filter F) k) (sym &iso) fz) (subst (λ k → odef (* z) k) (sym &iso) az1))  )
          FP : Filter {Power P} {P} (λ x → x)
-         FP = record { filter = FPSet ; f⊆L = FPSet⊆PP ; filter1 = ty01 ; filter2 = {!!} } where
+         FP = record { filter = FPSet ; f⊆L = FPSet⊆PP ; filter1 = ty01 ; filter2 = ty02 } where
              ty01 : {p q : HOD} → Power P ∋ q → FPSet ∋ p → p ⊆ q → FPSet ∋ q
              ty01 {p} {q} Pq record { z = x ; az = fx ; x=ψz = x=ψz } p⊆q = FPSet∋zpq q⊆P (ty10 ty05 ty06 )
                 where
@@ -420,6 +445,8 @@
                   ty06 (ab-pair wp wq ) = ab-pair (p⊆q wp) wq
                   ty10 : filter F ∋ ZFP p Q → ZFP p Q ⊆ ZFP q Q → filter F ∋  ZFP q Q
                   ty10 fzp zp⊆zq = filter1 F ty03 fzp zp⊆zq
+             ty02 : {p q : HOD} → FPSet ∋ p → FPSet ∋ q → Power P ∋ (p ∩ q) → FPSet ∋ (p ∩ q)
+             ty02 = ?
 
          UFP : ultra-filter FP
          UFP = record { proper = {!!} ; ultra = {!!} }
@@ -427,9 +454,7 @@
          uflp = FIP→UFLP TP (Compact→FIP TP CP) FP UFP
 
          FQ : Filter {Power Q} {Q} (λ x → x)
-         FQ = record { filter = Proj2 (filter F) (Power P) (Power Q) ; f⊆L = ty00 ; filter1 = {!!} ; filter2 = {!!} } where
-             ty00 :  Proj2 (filter F) (Power P) (Power Q) ⊆ Power Q
-             ty00 {x} ⟪ QPx , ppf ⟫ = QPx
+         FQ = record { filter = ? ; f⊆L = ? ; filter1 = ? ; filter2 = {!!} } 
          UFQ : ultra-filter FQ
          UFQ = record { proper = {!!} ; ultra = {!!} }
          uflq : UFLP TQ FQ UFQ
@@ -454,10 +479,10 @@
                  --    x is also an elment of Proj1 F because Proj1 F has UFLP (uflp)
                  --    BaseP ∩ F is not empty
                  --    (Base P ∩ F) ⊆ F , (Base P ) ⊆ F ,
-                 il1 : odef (Power P) z ∧ ZProj1 (filter F) z
+                 il1 : odef (Power P) z ∧ ? -- ZFPproj1 (filter F) z
                  il1 = {!!} -- UFLP.is-limit uflp ? bz
                  nei1 : HOD
-                 nei1 = Proj1 (* (Neighbor.u npq)) (Power P) (Power Q)
+                 nei1 = ? -- ZFPproj1 (* (Neighbor.u npq)) (Power P) (Power Q)
                  plimit : Ordinal
                  plimit = UFLP.limit uflp
                  nproper : {b : Ordinal } →  * b ⊆ nei1 → o∅ o< b
diff -r 287d40830be5 -r 362e43a1477c src/ZProduct.agda
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZProduct.agda	Mon Mar 06 10:45:34 2023 +0900
@@ -0,0 +1,226 @@
+{-# OPTIONS --allow-unsolved-metas #-}
+
+open import Level
+open import Ordinals
+module ZProduct {n : Level } (O : Ordinals {n})   where
+
+open import zf
+open import logic
+import OD 
+import ODUtil
+import OrdUtil
+
+open import Relation.Nullary
+open import Relation.Binary
+open import Data.Empty
+open import Relation.Binary
+open import Relation.Binary.Core
+open import  Relation.Binary.PropositionalEquality
+open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
+
+open OD O
+open OD.OD
+open OD.HOD
+open ODAxiom odAxiom
+
+open Ordinals.Ordinals  O
+open Ordinals.IsOrdinals isOrdinal
+open Ordinals.IsNext isNext
+open OrdUtil O
+open ODUtil O
+
+open _∧_
+open _∨_
+open Bool
+
+open _==_
+
+<_,_> : (x y : HOD) → HOD
+< x , y > = (x , x ) , (x , y )
+
+exg-pair : { x y : HOD } → (x , y ) =h= ( y , x )
+exg-pair {x} {y} = record { eq→ = left ; eq← = right } where
+    left : {z : Ordinal} → odef (x , y) z → odef (y , x) z 
+    left (case1 t) = case2 t
+    left (case2 t) = case1 t
+    right : {z : Ordinal} → odef (y , x) z → odef (x , y) z 
+    right (case1 t) = case2 t
+    right (case2 t) = case1 t
+
+ord≡→≡ : { x y : HOD } → & x ≡ & y → x ≡ y
+ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) *iso *iso ( cong ( λ k → * k ) eq )
+
+od≡→≡ : { x y : Ordinal } → * x ≡ * y → x ≡ y
+od≡→≡ eq = subst₂ (λ j k → j ≡ k ) &iso &iso ( cong ( λ k → & k ) eq )
+
+eq-prod : { x x' y y' : HOD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' >
+eq-prod refl refl = refl
+
+xx=zy→x=y : {x y z : HOD } → ( x , x ) =h= ( z , y ) → x ≡ y
+xx=zy→x=y {x} {y} eq with trio< (& x) (& y) 
+xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c with eq← eq {& y} (case2 refl) 
+xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c | case1 s = ⊥-elim ( o<¬≡ (sym s) a )
+xx=zy→x=y {x} {y} eq | tri< a ¬b ¬c | case2 s = ⊥-elim ( o<¬≡ (sym s) a )
+xx=zy→x=y {x} {y} eq | tri≈ ¬a b ¬c = ord≡→≡ b
+xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c  with eq← eq {& y} (case2 refl) 
+xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c | case1 s = ⊥-elim ( o<¬≡ s c )
+xx=zy→x=y {x} {y} eq | tri> ¬a ¬b c | case2 s = ⊥-elim ( o<¬≡ s c )
+
+prod-eq : { x x' y y' : HOD } → < x , y > =h= < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' )
+prod-eq {x} {x'} {y} {y'} eq = ⟪ lemmax , lemmay ⟫ where
+    lemma2 : {x y z : HOD } → ( x , x ) =h= ( z , y ) → z ≡ y
+    lemma2 {x} {y} {z} eq = trans (sym (xx=zy→x=y lemma3 )) ( xx=zy→x=y eq )  where
+        lemma3 : ( x , x ) =h= ( y , z )
+        lemma3 = ==-trans eq exg-pair
+    lemma1 : {x y : HOD } → ( x , x ) =h= ( y , y ) → x ≡ y
+    lemma1 {x} {y} eq with eq← eq {& y} (case2 refl)
+    lemma1 {x} {y} eq | case1 s = ord≡→≡ (sym s)
+    lemma1 {x} {y} eq | case2 s = ord≡→≡ (sym s)
+    lemma4 : {x y z : HOD } → ( x , y ) =h= ( x , z ) → y ≡ z
+    lemma4 {x} {y} {z} eq with eq← eq {& z} (case2 refl)
+    lemma4 {x} {y} {z} eq | case1 s with ord≡→≡ s -- x ≡ z
+    ... | refl with lemma2 (==-sym eq )
+    ... | refl = refl
+    lemma4 {x} {y} {z} eq | case2 s = ord≡→≡ (sym s) -- y ≡ z
+    lemmax : x ≡ x'
+    lemmax with eq→ eq {& (x , x)} (case1 refl) 
+    lemmax | case1 s = lemma1 (ord→== s )  -- (x,x)≡(x',x')
+    lemmax | case2 s with lemma2 (ord→== s ) -- (x,x)≡(x',y') with x'≡y'
+    ... | refl = lemma1 (ord→== s )
+    lemmay : y ≡ y'
+    lemmay with lemmax
+    ... | refl with lemma4 eq -- with (x,y)≡(x,y')
+    ... | eq1 = lemma4 (ord→== (cong (λ  k → & k )  eq1 ))
+
+prod-≡ : { x x' y y' : HOD } → < x , y > ≡ < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' )
+prod-≡ eq = prod-eq (ord→== (cong (&) eq ))
+
+--
+-- unlike ordered pair, ZFPair is not a HOD
+
+data ord-pair : (p : Ordinal) → Set n where
+   pair : (x y : Ordinal ) → ord-pair ( & ( < * x , * y > ) )
+
+ZFPair : OD
+ZFPair = record { def = λ x → ord-pair x }
+
+-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+-- eq-pair : { x x' y y' : Ordinal } → x ≡ x' → y ≡ y' → pair x y ≅ pair x' y'
+-- eq-pair refl refl = HE.refl
+
+pi1 : { p : Ordinal } →   ord-pair p →  Ordinal
+pi1 ( pair x y) = x
+
+π1 : { p : HOD } → def ZFPair (& p) → HOD
+π1 lt = * (pi1 lt )
+
+pi2 : { p : Ordinal } →   ord-pair p →  Ordinal
+pi2 ( pair x y ) = y
+
+π2 : { p : HOD } → def ZFPair (& p) → HOD
+π2 lt = * (pi2 lt )
+
+op-cons :  ( ox oy  : Ordinal ) → def ZFPair (& ( < * ox , * oy >   ))
+op-cons ox oy = pair ox oy
+
+def-subst :  {Z : OD } {X : Ordinal  }{z : OD } {x : Ordinal  }→ def Z X → Z ≡ z  →  X ≡ x  →  def z x
+def-subst df refl refl = df
+
+p-cons :  ( x y  : HOD ) → def ZFPair (& ( < x , y >))
+p-cons x y = def-subst {_} {_} {ZFPair} {& (< x , y >)} (pair (& x) ( & y )) refl (
+   let open ≡-Reasoning in begin
+       & < * (& x) , * (& y) >
+   ≡⟨ cong₂ (λ j k → & < j , k >) *iso *iso ⟩
+       & < x , y >
+   ∎ ) 
+
+op-iso :  { op : Ordinal } → (q : ord-pair op ) → & < * (pi1 q) , * (pi2 q) > ≡ op
+op-iso (pair ox oy) = refl
+
+p-iso :  { x  : HOD } → (p : def ZFPair (&  x) ) → < π1 p , π2 p > ≡ x
+p-iso {x} p = ord≡→≡ (op-iso p) 
+
+p-pi1 :  { x y : HOD } → (p : def ZFPair (&  < x , y >) ) →  π1 p ≡ x
+p-pi1 {x} {y} p = proj1 ( prod-eq ( ord→== (op-iso p) ))
+
+p-pi2 :  { x y : HOD } → (p : def ZFPair (&  < x , y >) ) →  π2 p ≡ y
+p-pi2 {x} {y} p = proj2 ( prod-eq ( ord→== (op-iso p)))
+
+_⊗_ : (A B : HOD) → HOD
+A ⊗ B  = Union ( Replace B (λ b → Replace A (λ a → < a , b > ) ))
+
+product→ : {A B a b : HOD} → A ∋ a → B ∋ b  → ( A ⊗ B ) ∋ < a , b >
+product→ {A} {B} {a} {b} A∋a B∋b = record { owner = _ ; ao = lemma1 ; ox = subst (λ k → odef k _) (sym *iso) lemma2  } where
+    lemma1 :  odef (Replace B (λ b₁ → Replace A (λ a₁ → < a₁ , b₁ >))) (& (Replace A (λ a₁ → < a₁ , b >)))
+    lemma1 = replacement← B b B∋b
+    lemma2 : odef (Replace A (λ a₁ → < a₁ , b >)) (& < a , b >)
+    lemma2 = replacement← A a A∋a
+
+data ZFProduct  (A B : HOD) : (p : Ordinal) → Set n where
+    ab-pair : {a b : Ordinal } → odef A a → odef B b → ZFProduct A B ( & ( < * a , * b > ) )
+
+ZFP  : (A B : HOD) → HOD
+ZFP  A B = record { od = record { def = λ x → ZFProduct A B x  } 
+        ; odmax = odmax ( A ⊗ B ) ; <odmax = λ {y} px → <odmax ( A ⊗ B ) (lemma0 px) }  
+   where
+        lemma0 :  {A B : HOD} {x : Ordinal} → ZFProduct A B x → odef (A ⊗ B) x
+        lemma0 {A} {B} {px} ( ab-pair {a} {b} ax by ) = product→ (d→∋ A ax) (d→∋ B by)
+
+ZFP→ : {A B a b : HOD} → A ∋ a → B ∋ b  → ZFP A B ∋ < a , b >
+ZFP→ {A} {B} {a} {b} aa bb = subst (λ k → ZFProduct A B k ) (cong₂ (λ j k → & < j , k >) *iso *iso ) ( ab-pair aa bb ) 
+
+zπ1 : {A B : HOD} → {x : Ordinal } → odef (ZFP A B) x → Ordinal
+zπ1 {A} {B} {.(& < * _ , * _ >)} (ab-pair {a} {b} aa bb) = a
+
+zp1 : {A B : HOD} → {x : Ordinal } → (zx : odef (ZFP A B) x) → odef A (zπ1 zx)
+zp1 {A} {B} {.(& < * _ , * _ >)} (ab-pair {a} {b} aa bb ) = aa
+
+zπ2 : {A B : HOD} → {x : Ordinal } → odef (ZFP A B) x → Ordinal
+zπ2 (ab-pair {a} {b} aa bb) = b
+
+zp2 : {A B : HOD} → {x : Ordinal } → (zx : odef (ZFP A B) x) → odef B (zπ2 zx)
+zp2 {A} {B} {.(& < * _ , * _ >)} (ab-pair {a} {b} aa bb ) = bb
+
+zp-iso :  { A B : HOD } → {x : Ordinal } → (p : odef (ZFP A B) x ) → & < * (zπ1 p) , * (zπ2 p) > ≡ x
+zp-iso {A} {B} {_} (ab-pair {a} {b} aa bb)  = refl
+
+zp-iso1 :  { A B : HOD } → {a b : Ordinal } → (p : odef (ZFP A B) (& < * a , * b > )) → (* (zπ1 p) ≡ (* a)) ∧ (* (zπ2 p) ≡ (* b))
+zp-iso1 {A} {B} {a} {b} pab = prod-≡ (subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) zz11) ) where
+      zz11 : & < * (zπ1 pab) , * (zπ2 pab) > ≡ & < * a , * b >
+      zz11 = zp-iso pab
+
+ZFP⊆⊗ :  {A B : HOD} {x : Ordinal} → odef (ZFP A B) x → odef (A ⊗ B) x
+ZFP⊆⊗ {A} {B} {px} ( ab-pair {a} {b} ax by ) = product→ (d→∋ A ax) (d→∋ B by)
+
+⊗⊆ZFPair : {A B x : HOD} → ( A ⊗ B ) ∋ x → def ZFPair (& x)
+⊗⊆ZFPair {A} {B} {x} record { owner = owner ; ao = record { z = a ; az = aa ; x=ψz = x=ψa } ; ox = ox } = zfp01 where
+       zfp02 : Replace A (λ z → < z , * a >) ≡ * owner
+       zfp02 = subst₂ ( λ j k → j ≡ k ) *iso refl (sym (cong (*) x=ψa ))
+       zfp01 : def ZFPair (& x)
+       zfp01 with subst (λ k → odef k (& x) ) (sym zfp02) ox
+       ... | record { z = b ; az = ab ; x=ψz = x=ψb } = subst (λ  k → def ZFPair  k) (cong (&) zfp00) (op-cons b a )  where
+           zfp00 : < * b , * a > ≡ x
+           zfp00 = sym ( subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) x=ψb) )
+
+⊗⊆ZFP : {A B x : HOD} → ( A ⊗ B ) ∋ x → odef (ZFP A B) (& x)
+⊗⊆ZFP {A} {B} {x} record { owner = owner ; ao = record { z = a ; az = ba ; x=ψz = x=ψa } ; ox = ox } = zfp01 where
+       zfp02 : Replace A (λ z → < z , * a >) ≡ * owner
+       zfp02 = subst₂ ( λ j k → j ≡ k ) *iso refl (sym (cong (*) x=ψa ))
+       zfp01 : odef (ZFP A B) (& x)
+       zfp01 with subst (λ k → odef k (& x) ) (sym zfp02) ox
+       ... | record { z = b ; az = ab ; x=ψz = x=ψb } = subst (λ k → ZFProduct A B k ) (sym x=ψb) (ab-pair ab ba) 
+
+ZFPproj1 : {A B X : HOD} → X ⊆ ZFP A B  → HOD
+ZFPproj1 {A} {B} {X} X⊆P = Replace' X ( λ x px → * (zπ1 (X⊆P px) )) 
+
+ZFPproj2 : {A B X : HOD} → X ⊆ ZFP A B  → HOD
+ZFPproj2 {A} {B} {X} X⊆P = Replace' X ( λ x px → * (zπ2 (X⊆P px) )) 
+
+ZFProj1-iso : {P Q : HOD} {a b x : Ordinal } ( p : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ1 p ≡ a
+ZFProj1-iso {P} {Q} {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq))
+... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) a=c)
+
+ZFProj2-iso : {P Q : HOD} {a b x : Ordinal } ( p : ZFProduct P Q x ) → x ≡ & < * a , * b > → zπ2 p ≡ b
+ZFProj2-iso {P} {Q} {a} {b} (ab-pair {c} {d} zp zq) eq with prod-≡ (subst₂ (λ j k → j ≡ k) *iso *iso (cong (*) eq))
+... | ⟪ a=c , b=d ⟫ = subst₂ (λ j k → j ≡ k) &iso &iso (cong (&) b=d)
+
diff -r 287d40830be5 -r 362e43a1477c src/cardinal.agda
--- a/src/cardinal.agda	Sun Mar 05 23:49:10 2023 +0900
+++ b/src/cardinal.agda	Mon Mar 06 10:45:34 2023 +0900
@@ -10,7 +10,6 @@
 import OD hiding ( _⊆_ )
 
 import ODC
-import OPair
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ )
 open import Relation.Binary.PropositionalEquality
 open import Data.Nat.Properties
@@ -22,8 +21,8 @@
 open inOrdinal O
 open OD O
 open OD.OD
-open OPair O
 open ODAxiom odAxiom
+open import ZProduct O
 
 import OrdUtil
 import ODUtil
diff -r 287d40830be5 -r 362e43a1477c src/generic-filter.agda
--- a/src/generic-filter.agda	Sun Mar 05 23:49:10 2023 +0900
+++ b/src/generic-filter.agda	Mon Mar 06 10:45:34 2023 +0900
@@ -52,8 +52,7 @@
 open import Data.List hiding (filter)
 open import Data.Maybe 
 
-import OPair
-open OPair O
+open import ZProduct O
 
 record CountableModel : Set (suc (suc n)) where
    field