# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1680740212 -32400
# Node ID 7e7d8d825632adcd0074b4d3e1e7560bb4b9927f
# Parent  2cbe0db250da24f1c582d247a70db141aadc0f76
P x Q ⇆ Q x P done

diff -r 2cbe0db250da -r 7e7d8d825632 src/Tychonoff.agda
--- a/src/Tychonoff.agda	Wed Apr 05 17:05:32 2023 +0900
+++ b/src/Tychonoff.agda	Thu Apr 06 09:16:52 2023 +0900
@@ -35,7 +35,7 @@
 open import filter O
 open import ZProduct O
 open import Topology O
--- open import maximum-filter O
+open import maximum-filter O
 
 open Filter
 open Topology
@@ -80,6 +80,15 @@
        P∋limit : odef P limit
        is-limit : {v : Ordinal} → Neighbor TP limit v → filter F ∋ (* v)
 
+--
+-- If Any ultra filter has a limit that is  all neighbor of the limit is in the filter,
+-- it has finite intersection property.
+--
+-- Finite intersection defines a filter, so we have a ultra filter becaause Zorn lemma maximizing it.
+-- If the limit of filter is not contained by a closed set p in FIP, it is in P \ p. It is open and
+-- contains the limit, so it is in the ultra filter. This means p and P \ p is in the filter, which
+-- contradicts proper of the ultra filter.
+--
 UFLP→FIP : {P : HOD} (TP : Topology P) →
    ((F : Filter {Power P} {P} (λ x → x) ) (UF : ultra-filter F ) → UFLP TP F UF ) → FIP TP
 UFLP→FIP {P} TP uflp with trio< (& P) o∅
@@ -176,13 +185,13 @@
      --    otherwise the check requires a minute
      --
      maxf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → MaximumFilter (λ x → x) (F CSX fp)
-     maxf {X} 0<X CSX fp = ? -- F→Maximum {Power P} {P} (λ x → x) (CAP P)  (F CSX fp) 0<PP (N∋nc 0<X CSX fp) (proper CSX fp)
+     maxf {X} 0<X CSX fp = F→Maximum {Power P} {P} (λ x → x) (CAP P)  (F CSX fp) 0<PP (N∋nc 0<X CSX fp) (proper CSX fp)
      mf : {X : Ordinal} → o∅ o< X → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → Filter {Power P} {P} (λ x → x)
      mf {X} 0<X CSX fp =  MaximumFilter.mf (maxf 0<X CSX fp)
      ultraf : {X : Ordinal} → (0<X : o∅ o< X ) → (CSX : * X ⊆ CS TP) → (fp : fip {X} CSX) → ultra-filter ( mf 0<X CSX fp)
-     ultraf {X} 0<X CSX fp = ? -- F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp)  0<PP (N∋nc 0<X CSX fp) (proper CSX fp)
+     ultraf {X} 0<X CSX fp = F→ultra {Power P} {P} (λ x → x) (CAP P) (F CSX fp)  0<PP (N∋nc 0<X CSX fp) (proper CSX fp)
      --
-     -- so it has a limit as a limit of UIP
+     -- so it has a limit as a limit of FIP
      --
      limit : {X : Ordinal} → (CSX : * X ⊆ CS TP) → fip {X} CSX → Ordinal
      limit {X} CSX fp with trio< o∅ X
@@ -243,6 +252,13 @@
 P⊆Clx : {P : HOD} (TP : Topology P) →  {x : HOD} → x ⊆ P   → Cl TP x ⊆ P
 P⊆Clx {P} TP {x}  x<p {y} xy  = proj1 xy
 
+--
+-- Finite intersection property implies that any ultra filter have a limit, that is, neighbors of the limit is in the filter.
+--
+-- An ultra filter F is given. Take a closure of a filter. It is closed and it has finite intersection property, because F is porper.
+-- So it has a limit as a FIP. If a neighbor p which contains the limit, p or P \ p is in the ultra filter.
+-- If it is in P \ p, it cannot contains the limit, contradiction.
+--
 FIP→UFLP : {P : HOD} (TP : Topology P) →  FIP TP
    →  (F : Filter {Power P} {P} (λ x → x)) (UF : ultra-filter F ) → UFLP {P} TP F UF
 FIP→UFLP {P} TP fip F UF = record { limit = FIP.limit fip (subst (λ k → k ⊆ CS TP) (sym *iso) CF⊆CS) ufl01
@@ -345,18 +361,24 @@
 postulate f-extensionality : { n m : Level}  → Axiom.Extensionality.Propositional.Extensionality n m
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
 
-FilterQP : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  
-     → Filter {Power (ZFP Q P)} {ZFP Q P} (λ x → x) 
-FilterQP {P} {Q} F = record { filter = ? ; f⊆L = ? ; filter1 = ? ; filter2 = ? } 
+--    FilterQP : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  
+--         → Filter {Power (ZFP Q P)} {ZFP Q P} (λ x → x) 
+--    FilterQP {P} {Q} F = record { filter = ? ; f⊆L = ? ; filter1 = ? ; filter2 = ? } 
+-- 
+--    projection-of-filter : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  
+--         → Filter {Power P} {P} (λ x → x) 
+--    projection-of-filter = ?
+-- 
+--    projection-of-ultra-filter : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  (UF : ultra-filter F) 
+--         → ultra-filter (projection-of-filter F)
+--    projection-of-ultra-filter = ?
 
-projection-of-filter : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  
-     → Filter {Power P} {P} (λ x → x) 
-projection-of-filter = ?
-
-projection-of-ultra-filter : {P Q : HOD } → (F : Filter {Power (ZFP P Q)} {ZFP P Q} (λ x → x))  (UF : ultra-filter F) 
-     → ultra-filter (projection-of-filter F)
-projection-of-ultra-filter = ?
-
+--
+-- We have UFLP both in P and Q. Given an ultra filter F on P x Q. It has limits on P and Q because a projection of ultra filter
+-- is a ultra filter. Show the product of the limits is a limit of P x Q. A neighbor of P x Q contains subbase of P x Q,
+-- which is either inverse projection x of P or Q. The x in in projection of F, because of UFLP. So it is in F, because of the
+-- property of the filter.
+--
 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)
diff -r 2cbe0db250da -r 7e7d8d825632 src/ZProduct.agda
--- a/src/ZProduct.agda	Wed Apr 05 17:05:32 2023 +0900
+++ b/src/ZProduct.agda	Thu Apr 06 09:16:52 2023 +0900
@@ -6,7 +6,7 @@
 
 open import zf
 open import logic
-import OD 
+import OD
 import ODUtil
 import OrdUtil
 
@@ -16,7 +16,7 @@
 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 import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ )
 
 open OD O
 open OD.OD
@@ -40,10 +40,10 @@
 
 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 : {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 : {z : Ordinal} → odef (y , x) z → odef (x , y) z
     right (case1 t) = case2 t
     right (case2 t) = case1 t
 
@@ -57,12 +57,12 @@
 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 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  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 )
 
@@ -83,7 +83,7 @@
     ... | 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 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 )
@@ -118,14 +118,14 @@
     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) }  
+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 ) 
+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
@@ -148,7 +148,7 @@
       zz11 = zp-iso pab
 
 zp-iso0 :  { A B : HOD } → {a b : Ordinal } → (p : odef (ZFP A B) (& < * a , * b > )) → (zπ1 p ≡ a) ∧ (zπ2 p ≡ b)
-zp-iso0 {A} {B} {a} {b} pab = ⟪ subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj1 (zp-iso1 pab) ))  
+zp-iso0 {A} {B} {a} {b} pab = ⟪ subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj1 (zp-iso1 pab) ))
                               , subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj2 (zp-iso1 pab) ) )  ⟫
 
 ZFP⊆⊗ :  {A B : HOD} {x : Ordinal} → odef (ZFP A B) x → odef (A ⊗ B) x
@@ -160,13 +160,13 @@
        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) 
+       ... | record { z = b ; az = ab ; x=ψz = x=ψb } = subst (λ k → ZFProduct A B k ) (sym x=ψb) (ab-pair ab ba)
 
 ZPI1 : (A B : HOD) → HOD
-ZPI1 A B = Replace' (ZFP A B) ( λ x px → * (zπ1 px )) 
+ZPI1 A B = Replace' (ZFP A B) ( λ x px → * (zπ1 px ))
 
 ZPI2 : (A B  : HOD) → HOD
-ZPI2 A B = Replace' (ZFP A B) ( λ x px → * (zπ2 px )) 
+ZPI2 A B = Replace' (ZFP A B) ( λ x px → * (zπ2 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))
@@ -176,89 +176,6 @@
 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)
 
-record Func (A B : HOD) : Set n where
-    field
-       func : {x : Ordinal } → odef A x → Ordinal
-       is-func : {x : Ordinal } → (ax : odef A x) → odef B (func ax )
-
-data FuncHOD (A B : HOD) : (x : Ordinal) →  Set n where
-     felm :  (F : Func A B) → FuncHOD A B (& ( Replace' A ( λ x ax → < x , (* (Func.func F {& x} ax )) > )))
-
-FuncHOD→F : {A B : HOD} {x : Ordinal} → FuncHOD A B x → Func A B
-FuncHOD→F {A} {B} (felm F) = F
-
-FuncHOD=R : {A B : HOD} {x : Ordinal} → (fc : FuncHOD A B x) → (* x) ≡  Replace' A ( λ x ax → < x , (* (Func.func (FuncHOD→F fc) ax)) > )
-FuncHOD=R {A} {B}  (felm F) = *iso
-
---
---  Set of All function from A to B
---
-
-open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
-
-Funcs : (A B : HOD) → HOD
-Funcs A B = record { od = record { def = λ x → FuncHOD A B x } ; odmax = osuc (& (ZFP A B)) 
-       ; <odmax = λ {y} px → subst ( λ k → k o≤ (& (ZFP A B)) ) &iso (⊆→o≤ (lemma1 px)) } where
-    lemma1 : {y : Ordinal } → FuncHOD A B y → {x : Ordinal} → odef (* y) x → odef (ZFP A B) x
-    lemma1 {y} (felm F) {x} yx with subst (λ k → odef k x) *iso yx
-    ... | record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → ZFProduct A B k) 
-          (sym x=ψz) lemma4 where
-       lemma4 : ZFProduct A B (& < * z , * (Func.func F (subst (λ k → odef A k) (sym &iso) az)) > )
-       lemma4 = ab-pair az (Func.is-func F (subst (λ k → odef A k) (sym &iso) az))
-
-record Injection (A B : Ordinal ) : Set n where
-   field
-       i→  : (x : Ordinal ) → odef (* A)  x → Ordinal
-       iB  : (x : Ordinal ) → ( lt : odef (* A)  x ) → odef (* B) ( i→ x lt )
-       iiso : (x y : Ordinal ) → ( ltx : odef (* A)  x ) ( lty : odef (* A)  y ) → i→ x ltx ≡ i→ y lty → x ≡ y
-
-record HODBijection (A B : HOD ) : Set n where
-   field
-       fun←  : (x : Ordinal ) → odef A  x → Ordinal
-       fun→  : (x : Ordinal ) → odef B  x → Ordinal
-       funB  : (x : Ordinal ) → ( lt : odef A  x ) → odef B ( fun← x lt )
-       funA  : (x : Ordinal ) → ( lt : odef B  x ) → odef A ( fun→ x lt )
-       fiso← : (x : Ordinal ) → ( lt : odef B  x ) → fun← ( fun→ x lt ) ( funA x lt ) ≡ x
-       fiso→ : (x : Ordinal ) → ( lt : odef A  x ) → fun→ ( fun← x lt ) ( funB x lt ) ≡ x
-
-hodbij-refl : { a b : HOD } → a ≡ b → HODBijection a b
-hodbij-refl {a} refl = record {
-       fun←  = λ x _ → x 
-     ; fun→  = λ x _ → x 
-     ; funB  = λ x lt → lt
-     ; funA  = λ x lt → lt
-     ; fiso← = λ x lt → refl
-     ; fiso→ = λ x lt → refl
-    }
-
-pj12 : (A B : HOD) {x : Ordinal} → (ab : odef (ZFP A B) x ) → 
-   (zπ1  (subst (odef (ZFP A B)) (sym &iso) ab) ≡ & (* (zπ1 ab ))) ∧ 
-   (zπ2  (subst (odef (ZFP A B)) (sym &iso) ab) ≡ & (* (zπ2 ab )))
-pj12 A B (ab-pair {x} {y} ax by) = ⟪ subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj1 (prod-≡ pj24 ))) 
-      , subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj2 (prod-≡ pj24)))  ⟫ where
-   pj22 : odef (ZFP A B) (& (* (& < * x , * y >)))
-   pj22 = subst (odef (ZFP A B)) (sym &iso) (ab-pair ax by)
-   pj23 : & < * (zπ1 pj22 ) , * (zπ2 pj22) > ≡ & (* (& < * x , * y >) )
-   pj23 = zp-iso pj22
-   pj24 : < * (zπ1 (subst (odef (ZFP A B)) (sym &iso) (ab-pair ax by))) , * (zπ2 (subst (odef (ZFP A B)) (sym &iso) (ab-pair ax by))) >
-    ≡ < * (& (* x)) ,  * (& (* y)) >
-   pj24 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) ( trans pj23 (trans &iso 
-       (sym (cong (&) (cong₂ (λ j k → < j , k >) *iso *iso)) ))))
-pj02 : (A B : HOD) (x : Ordinal) → (ab : odef (ZFP A B) x ) → odef (ZPI2 A B) (zπ2 ab)
-pj02 A B x ab = record { z = _ ; az = ab ; x=ψz = trans (sym &iso) (trans ( sym (proj2 (pj12 A B ab))) (sym &iso))  }
-pj01 : (A B : HOD) (x : Ordinal) → (ab : odef (ZFP A B) x ) → odef (ZPI1 A B) (zπ1 ab)
-pj01 A B x ab = record { z = _ ; az = ab ; x=ψz = trans (sym &iso) (trans ( sym (proj1 (pj12 A B ab))) (sym &iso))  }
-pj2 :  (A B : HOD) (x : Ordinal) (lt : odef (ZFP A B) x) → odef (ZFP (ZPI2 A B) (ZPI1 A B)) (& < * (zπ2 lt) , * (zπ1 lt) >)
-pj2 A B x ab = ab-pair (pj02 A B x ab)  (pj01 A B x ab)
-aZPI1 : (A B : HOD) {y : Ordinal} → odef (ZPI1 A B) y → odef A y
-aZPI1 A B {y} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef A k) (trans (
-    trans (sym &iso) (trans (sym (proj1 (pj12 A B az))) (sym &iso))) (sym x=ψz)  ) ( zp1 az )
-aZPI2 : (A B : HOD) {y : Ordinal} → odef (ZPI2 A B) y → odef B y
-aZPI2 A B {y} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef B k) (trans (
-    trans (sym &iso) (trans (sym (proj2 (pj12 A B az))) (sym &iso))) (sym x=ψz)  ) ( zp2 az )
-pj1 :  (A B : HOD) (x : Ordinal) (lt : odef (ZFP (ZPI2 A B) (ZPI1 A B)) x) → odef (ZFP A B) (& < * (zπ2 lt) , * (zπ1 lt) >)
-pj1 A B _ (ab-pair ax by) = ab-pair (aZPI1 A B by) (aZPI2 A B ax) 
-
 ZPI1-iso : (A B : HOD) → {b : Ordinal } → odef B b → ZPI1 A B ≡ A
 ZPI1-iso P Q {q} qq = ==→o≡ record { eq→ = ty20 ; eq← = ty22 } where
      ty21 : {a b : Ordinal } → (pz : odef P a) → (qz : odef Q b) → ZFProduct P Q (& (* (& < * a , * b >)))
@@ -311,6 +228,91 @@
             * x ≡⟨ sym (cong (*) (ty32 pp qx  )) ⟩
             * (zπ2 (subst (odef (ZFP P Q)) (sym &iso) (ab-pair pp qx  ))) ∎ where open ≡-Reasoning
 
+record Func (A B : HOD) : Set n where
+    field
+       func : {x : Ordinal } → odef A x → Ordinal
+       is-func : {x : Ordinal } → (ax : odef A x) → odef B (func ax )
+
+data FuncHOD (A B : HOD) : (x : Ordinal) →  Set n where
+     felm :  (F : Func A B) → FuncHOD A B (& ( Replace' A ( λ x ax → < x , (* (Func.func F {& x} ax )) > )))
+
+FuncHOD→F : {A B : HOD} {x : Ordinal} → FuncHOD A B x → Func A B
+FuncHOD→F {A} {B} (felm F) = F
+
+FuncHOD=R : {A B : HOD} {x : Ordinal} → (fc : FuncHOD A B x) → (* x) ≡  Replace' A ( λ x ax → < x , (* (Func.func (FuncHOD→F fc) ax)) > )
+FuncHOD=R {A} {B}  (felm F) = *iso
+
+--
+--  Set of All function from A to B
+--
+
+open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
+
+Funcs : (A B : HOD) → HOD
+Funcs A B = record { od = record { def = λ x → FuncHOD A B x } ; odmax = osuc (& (ZFP A B))
+       ; <odmax = λ {y} px → subst ( λ k → k o≤ (& (ZFP A B)) ) &iso (⊆→o≤ (lemma1 px)) } where
+    lemma1 : {y : Ordinal } → FuncHOD A B y → {x : Ordinal} → odef (* y) x → odef (ZFP A B) x
+    lemma1 {y} (felm F) {x} yx with subst (λ k → odef k x) *iso yx
+    ... | record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → ZFProduct A B k)
+          (sym x=ψz) lemma4 where
+       lemma4 : ZFProduct A B (& < * z , * (Func.func F (subst (λ k → odef A k) (sym &iso) az)) > )
+       lemma4 = ab-pair az (Func.is-func F (subst (λ k → odef A k) (sym &iso) az))
+
+record Injection (A B : Ordinal ) : Set n where
+   field
+       i→  : (x : Ordinal ) → odef (* A)  x → Ordinal
+       iB  : (x : Ordinal ) → ( lt : odef (* A)  x ) → odef (* B) ( i→ x lt )
+       iiso : (x y : Ordinal ) → ( ltx : odef (* A)  x ) ( lty : odef (* A)  y ) → i→ x ltx ≡ i→ y lty → x ≡ y
+
+record HODBijection (A B : HOD ) : Set n where
+   field
+       fun←  : (x : Ordinal ) → odef A  x → Ordinal
+       fun→  : (x : Ordinal ) → odef B  x → Ordinal
+       funB  : (x : Ordinal ) → ( lt : odef A  x ) → odef B ( fun← x lt )
+       funA  : (x : Ordinal ) → ( lt : odef B  x ) → odef A ( fun→ x lt )
+       fiso← : (x : Ordinal ) → ( lt : odef B  x ) → fun← ( fun→ x lt ) ( funA x lt ) ≡ x
+       fiso→ : (x : Ordinal ) → ( lt : odef A  x ) → fun→ ( fun← x lt ) ( funB x lt ) ≡ x
+
+hodbij-refl : { a b : HOD } → a ≡ b → HODBijection a b
+hodbij-refl {a} refl = record {
+       fun←  = λ x _ → x
+     ; fun→  = λ x _ → x
+     ; funB  = λ x lt → lt
+     ; funA  = λ x lt → lt
+     ; fiso← = λ x lt → refl
+     ; fiso→ = λ x lt → refl
+    }
+
+pj12 : (A B : HOD) {x : Ordinal} → (ab : odef (ZFP A B) x ) →
+   (zπ1  (subst (odef (ZFP A B)) (sym &iso) ab) ≡ & (* (zπ1 ab ))) ∧
+   (zπ2  (subst (odef (ZFP A B)) (sym &iso) ab) ≡ & (* (zπ2 ab )))
+pj12 A B (ab-pair {x} {y} ax by) = ⟪ subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj1 (prod-≡ pj24 )))
+      , subst₂ (λ j k → j ≡ k ) &iso &iso (cong (&) (proj2 (prod-≡ pj24)))  ⟫ where
+   pj22 : odef (ZFP A B) (& (* (& < * x , * y >)))
+   pj22 = subst (odef (ZFP A B)) (sym &iso) (ab-pair ax by)
+   pj23 : & < * (zπ1 pj22 ) , * (zπ2 pj22) > ≡ & (* (& < * x , * y >) )
+   pj23 = zp-iso pj22
+   pj24 : < * (zπ1 (subst (odef (ZFP A B)) (sym &iso) (ab-pair ax by))) , * (zπ2 (subst (odef (ZFP A B)) (sym &iso) (ab-pair ax by))) >
+    ≡ < * (& (* x)) ,  * (& (* y)) >
+   pj24 = subst₂ (λ j k → j ≡ k ) *iso *iso (cong (*) ( trans pj23 (trans &iso
+       (sym (cong (&) (cong₂ (λ j k → < j , k >) *iso *iso)) ))))
+pj02 : (A B : HOD) (x : Ordinal) → (ab : odef (ZFP A B) x ) → odef (ZPI2 A B) (zπ2 ab)
+pj02 A B x ab = record { z = _ ; az = ab ; x=ψz = trans (sym &iso) (trans ( sym (proj2 (pj12 A B ab))) (sym &iso))  }
+pj01 : (A B : HOD) (x : Ordinal) → (ab : odef (ZFP A B) x ) → odef (ZPI1 A B) (zπ1 ab)
+pj01 A B x ab = record { z = _ ; az = ab ; x=ψz = trans (sym &iso) (trans ( sym (proj1 (pj12 A B ab))) (sym &iso))  }
+
+pj2 :  (A B : HOD) (x : Ordinal) (lt : odef (ZFP A B) x) → odef (ZFP (ZPI2 A B) (ZPI1 A B)) (& < * (zπ2 lt) , * (zπ1 lt) >)
+pj2 A B x ab = ab-pair (pj02 A B x ab)  (pj01 A B x ab)
+
+aZPI1 : (A B : HOD) {y : Ordinal} → odef (ZPI1 A B) y → odef A y
+aZPI1 A B {y} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef A k) (trans (
+    trans (sym &iso) (trans (sym (proj1 (pj12 A B az))) (sym &iso))) (sym x=ψz)  ) ( zp1 az )
+aZPI2 : (A B : HOD) {y : Ordinal} → odef (ZPI2 A B) y → odef B y
+aZPI2 A B {y} record { z = z ; az = az ; x=ψz = x=ψz } = subst (λ k → odef B k) (trans (
+    trans (sym &iso) (trans (sym (proj2 (pj12 A B az))) (sym &iso))) (sym x=ψz)  ) ( zp2 az )
+
+pj1 :  (A B : HOD) (x : Ordinal) (lt : odef (ZFP (ZPI2 A B) (ZPI1 A B)) x) → odef (ZFP A B) (& < * (zπ2 lt) , * (zπ1 lt) >)
+pj1 A B _ (ab-pair ax by) = ab-pair (aZPI1 A B by) (aZPI2 A B ax)
 
 ZFPsym1 : (A B  : HOD) → HODBijection (ZFP A B) (ZFP (ZPI2 A B) (ZPI1 A B))
 ZFPsym1 A B = record {
@@ -321,13 +323,16 @@
      ; fiso← = λ xy ab → pj00 A B ab
      ; fiso→ = λ xy ab → zp-iso ab
     } where
-       pj10 : (A B : HOD) → {xy : Ordinal} → (ab : odef (ZFP (ZPI2 A B) (ZPI1 A B)) xy ) 
+       pj10 : (A B : HOD) → {xy : Ordinal} → (ab : odef (ZFP (ZPI2 A B) (ZPI1 A B)) xy )
            → & < * (zπ1 ab) , * (zπ2 ab) > ≡ & < *  (zπ2 (pj1 A B xy ab)) ,  * (zπ1 (pj1 A B xy ab)) >
        pj10 A B {.(& < * _ , * _ >)} (ab-pair ax by ) = refl
-       pj00 : (A B : HOD) → {xy : Ordinal} → (ab : odef (ZFP (ZPI2 A B) (ZPI1 A B)) xy ) 
-           → & < * (zπ2 (pj1 A B xy ab)) , * (zπ1 (pj1 A B xy ab)) > ≡ xy 
+       pj00 : (A B : HOD) → {xy : Ordinal} → (ab : odef (ZFP (ZPI2 A B) (ZPI1 A B)) xy )
+           → & < * (zπ2 (pj1 A B xy ab)) , * (zπ1 (pj1 A B xy ab)) > ≡ xy
        pj00 A B {xy} ab = trans (sym (pj10 A B ab)) (zp-iso {ZPI2 A B} {ZPI1 A B} {xy} ab)
 
+--
+-- Bijection of (A x B) and (B x A) requires one element or axiom of choice
+--
 ZFPsym : (A B  : HOD) → {a b : Ordinal } → odef A a → odef B b  → HODBijection (ZFP A B) (ZFP B A)
 ZFPsym A B aa bb = subst₂ ( λ j k → HODBijection (ZFP A B) (ZFP j k)) (ZPI2-iso A B aa) (ZPI1-iso A B bb) ( ZFPsym1 A B )
 
@@ -342,7 +347,7 @@
        zfp06 : & < * (zπ1 q) , * (zπ2 q) > ≡ x
        zfp06 = zp-iso q
        zfp07 : & < * (zπ1 p) , * (zπ2 q) > ≡ x
-       zfp07 = trans (cong (λ k → & < k , * (zπ2 q)  >  ) 
+       zfp07 = trans (cong (λ k → & < k , * (zπ2 q)  >  )
            (proj1 (prod-≡ (subst₂ _≡_  *iso *iso (cong (*) (trans  zfp05 (sym (zfp06)))))))) zfp06
        zfp02 : {x  : Ordinal  } → (acx : odef (ZFP A C ∩ ZFP B C) x)   → odef (A ∩ B) (zπ1 (proj1 acx))
        zfp02 {.(& < * _ , * _ >)} ⟪ ab-pair {a} {b} ax bx , bcx ⟫ = ⟪ ax , zfp03 bcx refl ⟫ where
@@ -351,7 +356,7 @@
               zfp08 : a1 ≡ a
               zfp08 = subst₂ _≡_ &iso &iso (cong (&) (proj1 (prod-≡ (subst₂  _≡_  *iso *iso (cong (*) eq)))))
        zfp04 : {x : Ordinal } (acx : odef (ZFP B C) x )→ odef C (zπ2 acx)
-       zfp04 (ab-pair x x₁) = x₁ 
+       zfp04 (ab-pair x x₁) = x₁
 proj2 (ZFP∩ {A} {B} {C} ) = ==→o≡ record { eq→ = zfp00 ; eq← = zfp01  } where
    zfp00 : {x : Ordinal} → ZFProduct C (A ∩ B) x → odef (ZFP C A ∩ ZFP C B) x
    zfp00  (ab-pair qx ⟪ pa , pb ⟫ ) = ⟪ ab-pair qx pa  , ab-pair qx pb   ⟫
@@ -362,7 +367,7 @@
        zfp06 : & < * (zπ1 q) , * (zπ2 q) > ≡ x
        zfp06 = zp-iso q
        zfp07 : & < * (zπ1 p) , * (zπ2 q) > ≡ x
-       zfp07 = trans (cong (λ k → & < * (zπ1 p) , k  >  ) 
+       zfp07 = trans (cong (λ k → & < * (zπ1 p) , k  >  )
            (sym (proj2 (prod-≡ (subst₂ _≡_  *iso *iso (cong (*) (trans  zfp05 (sym (zfp06))))))))) zfp05
        zfp02 : {x  : Ordinal  } → (acx : odef (ZFP C A ∩ ZFP C B ) x)   → odef (A ∩ B) (zπ2 (proj2 acx))
        zfp02 {.(& < * _ , * _ >)} ⟪ bcx , ab-pair {b} {a} ax bx  ⟫ = ⟪ zfp03 bcx refl , bx ⟫ where
@@ -371,7 +376,7 @@
               zfp08 : a1 ≡ a
               zfp08 = subst₂ _≡_ &iso &iso (cong (&) (proj2 (prod-≡ (subst₂  _≡_  *iso *iso (cong (*) eq)))))
        zfp04 : {x : Ordinal } (acx : odef (ZFP C A ) x )→ odef C (zπ1 acx)
-       zfp04 (ab-pair x x₁) = x 
+       zfp04 (ab-pair x x₁) = x
 
 open import BAlgebra O
 
@@ -381,16 +386,16 @@
     ty70 ⟪ ab-pair {a} {b} Pa pb  , npq ⟫ = ab-pair ty72 pb  where
        ty72 : odef (P ＼ p ) a
        ty72 = ⟪ Pa , (λ pa → npq (ab-pair pa pb ) ) ⟫
-    ty71 : {x : Ordinal } → odef (ZFP (P ＼ p) Q) x → odef ( ZFP P Q ＼ ZFP p Q ) x 
-    ty71 (ab-pair {a} {b} ⟪ Pa , npa ⟫ Qb) = ⟪ ab-pair Pa Qb 
-        , (λ pab → npa (subst (λ k → odef p k) (proj1 (zp-iso0 pab)) (zp1 pab)) ) ⟫ 
+    ty71 : {x : Ordinal } → odef (ZFP (P ＼ p) Q) x → odef ( ZFP P Q ＼ ZFP p Q ) x
+    ty71 (ab-pair {a} {b} ⟪ Pa , npa ⟫ Qb) = ⟪ ab-pair Pa Qb
+        , (λ pab → npa (subst (λ k → odef p k) (proj1 (zp-iso0 pab)) (zp1 pab)) ) ⟫
     ty73 : {x : Ordinal } → odef ( ZFP P Q ＼ ZFP P p ) x →  odef (ZFP P (Q ＼ p) ) x
     ty73 ⟪ ab-pair {a} {b} pa Qb  , npq ⟫ = ab-pair pa ty72  where
        ty72 : odef (Q ＼ p ) b
        ty72 = ⟪ Qb , (λ qb → npq (ab-pair pa qb ) ) ⟫
-    ty75 : {x : Ordinal } → odef (ZFP P (Q ＼ p) ) x → odef ( ZFP P Q ＼ ZFP P p ) x 
-    ty75 (ab-pair {a} {b} Pa ⟪ Qb , nqb ⟫ ) = ⟪ ab-pair Pa Qb 
-        , (λ pab → nqb (subst (λ k → odef p k) (proj2 (zp-iso0 pab)) (zp2 pab)) ) ⟫ 
+    ty75 : {x : Ordinal } → odef (ZFP P (Q ＼ p) ) x → odef ( ZFP P Q ＼ ZFP P p ) x
+    ty75 (ab-pair {a} {b} Pa ⟪ Qb , nqb ⟫ ) = ⟪ ab-pair Pa Qb
+        , (λ pab → nqb (subst (λ k → odef p k) (proj2 (zp-iso0 pab)) (zp2 pab)) ) ⟫