# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1685619200 -32400
# Node ID f29970636e017f98b5eb94b569a22b581c93fba9
# Parent  302cfb533201cb79a60777849bbb58e71db5a59c
ZProduct with Replace sup

diff -r 302cfb533201 -r f29970636e01 src/ZProduct.agda
--- a/src/ZProduct.agda	Sat May 20 18:28:22 2023 +0900
+++ b/src/ZProduct.agda	Thu Jun 01 20:33:20 2023 +0900
@@ -37,6 +37,14 @@
 <_,_> : (x y : HOD) → HOD
 < x , y > = (x , x ) , (x , y )
 
+ZFP<AB : {X Y x y : HOD} → X ∋ x → Y ∋ y  → < x , y > ⊆ Power ( Union (X , Y ))
+ZFP<AB {X} {Y} {x} {y} xx yy (case1 refl ) z lt with subst (λ k → odef k z) *iso lt
+... | case1 refl = record { owner = _ ; ao = case1 refl  ; ox = subst₂ (λ j k → odef j k) (sym *iso) refl xx  }
+... | case2 refl = record { owner = _ ; ao = case1 refl  ; ox = subst₂ (λ j k → odef j k) (sym *iso) refl xx  }
+ZFP<AB {X} {Y} {x} {y} xx yy (case2 refl ) z lt with subst (λ k → odef k z) *iso lt
+... | case1 refl = record { owner = _ ; ao = case1 refl  ; ox = subst₂ (λ j k → odef j k) (sym *iso) refl xx  }
+... | case2 refl = record { owner = _ ; ao = case2 refl  ; ox = subst₂ (λ j k → odef j k) (sym *iso) refl yy  }
+
 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
@@ -118,13 +126,12 @@
 
 ZFP  : (A B : HOD) → HOD
 ZFP  A B = record { od = record { def = λ x → ZFProduct A B x  }
-        ; odmax = omax (& A) (& B) ; <odmax = λ {y} px → lemma0 px }
+        ; odmax =  osuc (& ( Power ( Union (A , B )))) ; <odmax = λ {y} px → lemma0 px }
    where
-        lemma0 :  {A B : HOD} {x : Ordinal} → ZFProduct A B x → x o< omax (& A) (& B)
-        lemma0 {A} {B} {px} ( ab-pair {a} {b} ax by ) with trio< a b
-        ... | tri< a<b ¬b ¬c = ?
-        ... | tri≈ ¬a a=b ¬c = ?
-        ... | tri> ¬a ¬b b<a = ?
+        lemma0 : {x : Ordinal } →  ZFProduct A B x → x o< osuc (& ( Power ( Union (A , B )) ))
+        lemma0 ( ab-pair {a} {b} ax by ) = lemma1  where
+            lemma1 : & < * a , * b > o< osuc (& (Power (Union (A , B))))
+            lemma1 = ⊆→o≤ (ZFP<AB (subst (λ k → odef A k) (sym &iso) ax) (subst (λ k → odef B k) (sym &iso) 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 )
@@ -166,10 +173,14 @@
 --        -- ... | 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 )) {Union A} record { ≤COD  = lemma1 } where
+    lemma1 : {x : Ordinal } (lt : odef (ZFP A B) x) → * (zπ1 lt) ⊆ Union A
+    lemma1  (ab-pair {a} {b} aa bb) {x} ax = record { owner = _ ; ao = aa ; ox = ax }
 
 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 )) {Union B} record { ≤COD  = lemma1 } where
+    lemma1 : {x : Ordinal } (lt : odef (ZFP A B) x) → * (zπ2 lt) ⊆ Union B
+    lemma1  (ab-pair {a} {b} aa bb) {x} bx = record { owner = _ ; ao = bb ; ox = bx }
 
 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))
@@ -231,18 +242,25 @@
             * x ≡⟨ sym (cong (*) (ty32 pp qx  )) ⟩
             * (zπ2 (subst (odef (ZFP P Q)) (sym &iso) (ab-pair pp qx  ))) ∎ where open ≡-Reasoning
 
+⊆-ZFP : {A B : HOD} {X Y x y : HOD} → X ⊆ A → Y ⊆ B → ZFP X Y ⊆ ZFP A B
+⊆-ZFP {A} {B} {X} {y} X<A Y<B (ab-pair xx yy) = ab-pair (X<A xx) (Y<B yy)
+
 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 )
+    fodmax : RXCod A (Power (Union (A , B))) (λ x ax → < x , * (func ax) >)
+    fodmax = record { ≤COD = λ {x} ax →  lemma1 ax } where
+        lemma1 : {x : HOD} → (ax : odef A (& x)) → < x , * (func ax) > ⊆ Power (Union (A , B)) 
+        lemma1 {x} ax = ZFP<AB ax (subst (λ k → odef B k) (sym &iso) ( is-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 )) > ) ? ))
+     felm :  (F : Func A B) → FuncHOD A B (& ( Replace' A ( λ x ax → < x , (* (Func.func F {& x} ax )) > ) (Func.fodmax F) ))
 
 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 : HOD} {x : Ordinal} → (fc : FuncHOD A B x) → (* x) ≡  Replace' A ( λ x ax → < x , (* (Func.func (FuncHOD→F fc) ax)) > ) (Func.fodmax (FuncHOD→F fc) )
 FuncHOD=R {A} {B}  (felm F) = *iso
 
 --