Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 1297:ad9ed7c4a0b3
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 03 Jun 2023 08:13:50 +0900 |
| parents | 428227847d62 |
| children | 2c34f2b554cf |
| files | src/OD.agda src/ODUtil.agda src/OrdUtil.agda src/Ordinals.agda src/PFOD.agda src/Tychonoff1.agda src/ZProduct.agda |
| diffstat | 7 files changed, 282 insertions(+), 118 deletions(-) [+] |
line wrap: on
line diff
--- 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
--- 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∅
--- 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
--- 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
--- 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
--- 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 )
--- 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