Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff src/OPair.agda @ 1104:81b859b678a8
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 29 Dec 2022 14:42:28 +0900 |
parents | 9dcbf3524a5c |
children | fabcb7d9f50c |
line wrap: on
line diff
--- a/src/OPair.agda Thu Dec 29 10:58:42 2022 +0900 +++ b/src/OPair.agda Thu Dec 29 14:42:28 2022 +0900 @@ -194,7 +194,7 @@ ZFP : (A B : HOD) → HOD ZFP A B = record { od = record { def = λ x → ZFProduct A B x } - ; odmax = omax (next (odmax A)) (next (odmax B)) ; <odmax = λ {y} px → lemma y px } + ; odmax = omax (next (odmax A)) (next (odmax B)) ; <odmax = λ {y} px → lemma y px } -- this is too large where lemma : (y : Ordinal) → ZFProduct A B y → y o< omax (next (odmax A)) (next (odmax B)) lemma p ( ab-pair {x} {y} ax by ) with trio< (& A) (& B) @@ -212,6 +212,21 @@ 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 + 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)