Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison src/ZProduct.agda @ 1286:619e68271cf8

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 22 May 2023 19:06:25 +0900
parents 302cfb533201
children
comparison
equal deleted inserted replaced
1285:302cfb533201 1286:619e68271cf8
33 open Bool 33 open Bool
34 34
35 open _==_ 35 open _==_
36 36
37 <_,_> : (x y : HOD) → HOD 37 <_,_> : (x y : HOD) → HOD
38 < x , y > = (x , x ) , (x , y ) 38 < x , y > = (x , x) , (x , y)
39 39
40 exg-pair : { x y : HOD } → (x , y ) =h= ( y , x ) 40 exg-pair : { x y : HOD } → (x , y ) =h= ( y , x )
41 exg-pair {x} {y} = record { eq→ = left ; eq← = right } where 41 exg-pair {x} {y} = record { eq→ = left ; eq← = right } where
42 left : {z : Ordinal} → odef (x , y) z → odef (y , x) z 42 left : {z : Ordinal} → odef (x , y) z → odef (y , x) z
43 left (case1 t) = case2 t 43 left (case1 t) = case2 t
111 -- lemma1 : odef (Replace' B (λ b₁ lb → Replace' A (λ a₁ la → < a₁ , b₁ >) ? ) ? ) (& (Replace' A (λ a₁ la → < a₁ , b >) ? )) 111 -- lemma1 : odef (Replace' B (λ b₁ lb → Replace' A (λ a₁ la → < a₁ , b₁ >) ? ) ? ) (& (Replace' A (λ a₁ la → < a₁ , b >) ? ))
112 -- lemma1 = ? -- replacement← B b B∋b ? 112 -- lemma1 = ? -- replacement← B b B∋b ?
113 -- lemma2 : odef (Replace' A (λ a₁ la → < a₁ , b >) ? ) (& < a , b >) 113 -- lemma2 : odef (Replace' A (λ a₁ la → < a₁ , b >) ? ) (& < a , b >)
114 -- lemma2 = ? -- replacement← A a A∋a ? 114 -- lemma2 = ? -- replacement← A a A∋a ?
115 115
116 -- & (x , x) o< next (osuc (& x))
117 -- & (x , y) o< next (omax (& x) (& y))
118 -- & ((x , x) , (x , y)) o< next (omax (next (osuc (& x))) (next (omax (& x) (& y))))
119 -- o≤ next (next (omax (& A) (& B)))
120
116 data ZFProduct (A B : HOD) : (p : Ordinal) → Set n where 121 data ZFProduct (A B : HOD) : (p : Ordinal) → Set n where
117 ab-pair : {a b : Ordinal } → odef A a → odef B b → ZFProduct A B ( & ( < * a , * b > ) ) 122 ab-pair : {a b : Ordinal } → odef A a → odef B b → ZFProduct A B ( & ( < * a , * b > ) )
118 123
119 ZFP : (A B : HOD) → HOD 124 ZFP : (A B : HOD) → HOD
120 ZFP A B = record { od = record { def = λ x → ZFProduct A B x } 125 ZFP A B = record { od = record { def = λ x → ZFProduct A B x }
121 ; odmax = omax (& A) (& B) ; <odmax = λ {y} px → lemma0 px } 126 ; odmax = omax (& A) (& B) ; <odmax = λ {y} px → lemma0 px }
122 where 127 where
123 lemma0 : {A B : HOD} {x : Ordinal} → ZFProduct A B x → x o< omax (& A) (& B) 128 lemma0 : {A B : HOD} {x : Ordinal} → ZFProduct A B x → x o< omax (& A) (& B)
124 lemma0 {A} {B} {px} ( ab-pair {a} {b} ax by ) with trio< a b 129 lemma0 {A} {B} {px} ( ab-pair {a} {b} ax by ) with trio< a b | inspect (omax a) b
125 ... | tri< a<b ¬b ¬c = ? 130 ... | tri< a<b ¬b ¬c | record { eq = eq1 } = ?
126 ... | tri≈ ¬a a=b ¬c = ? 131 ... | tri≈ ¬a a=b ¬c | record { eq = eq1 } = ?
127 ... | tri> ¬a ¬b b<a = ? 132 ... | tri> ¬a ¬b b<a | record { eq = eq1 } = ?
128 133
129 ZFP→ : {A B a b : HOD} → A ∋ a → B ∋ b → ZFP A B ∋ < a , b > 134 ZFP→ : {A B a b : HOD} → A ∋ a → B ∋ b → ZFP A B ∋ < a , b >
130 ZFP→ {A} {B} {a} {b} aa bb = subst (λ k → ZFProduct A B k ) (cong₂ (λ j k → & < j , k >) *iso *iso ) ( ab-pair aa bb ) 135 ZFP→ {A} {B} {a} {b} aa bb = subst (λ k → ZFProduct A B k ) (cong₂ (λ j k → & < j , k >) *iso *iso ) ( ab-pair aa bb )
131 136
132 zπ1 : {A B : HOD} → {x : Ordinal } → odef (ZFP A B) x → Ordinal 137 zπ1 : {A B : HOD} → {x : Ordinal } → odef (ZFP A B) x → Ordinal