Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison cardinal.agda @ 250:08428a661677
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Wed, 28 Aug 2019 23:52:54 +0900 |
parents | 2ecda48298e3 |
children | 9e0125b06e76 |
comparison
equal
deleted
inserted
replaced
249:2ecda48298e3 | 250:08428a661677 |
---|---|
86 lemmay : y ≡ y' | 86 lemmay : y ≡ y' |
87 lemmay with lemmax | 87 lemmay with lemmax |
88 ... | refl with lemma4 eq -- with (x,y)≡(x,y') | 88 ... | refl with lemma4 eq -- with (x,y)≡(x,y') |
89 ... | eq1 = lemma4 (ord→== (cong (λ k → od→ord k ) eq1 )) | 89 ... | eq1 = lemma4 (ord→== (cong (λ k → od→ord k ) eq1 )) |
90 | 90 |
91 | |
91 data ord-pair : (p : Ordinal) → Set n where | 92 data ord-pair : (p : Ordinal) → Set n where |
92 pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) ) | 93 pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) ) |
93 | 94 |
94 ZFProduct : OD | 95 ZFProduct : OD |
95 ZFProduct = record { def = λ x → ord-pair x } | 96 ZFProduct = record { def = λ x → ord-pair x } |
116 ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩ | 117 ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩ |
117 od→ord < x , y > | 118 od→ord < x , y > |
118 ∎ ) | 119 ∎ ) |
119 | 120 |
120 | 121 |
121 p-iso-1 : { x y : OD } → (p : ZFProduct ∋ < x , y > ) → π1 p ≡ od→ord x | 122 lemma44 : {ox oy : Ordinal } → ord-pair (od→ord < ord→od ox , ord→od oy >) |
122 p-iso-1 {x} {y} p = lemma1 {od→ord < x , y >} {od→ord x} {od→ord y} p (cong₂ (λ j k → ord-pair (od→ord < j , k >)) (sym oiso) (sym oiso) ) where | 123 lemma44 {ox} {oy} = pair ox oy |
123 lemma1 : {op ox oy : Ordinal } → ( p : ord-pair op ) → ord-pair op ≡ ord-pair (od→ord ( < ord→od ox , ord→od oy > )) → pi1 p ≡ ox | 124 |
124 lemma1 (pair ox oy) eq = {!!} | 125 lemma55 : {ox oy : Ordinal } → ZFProduct ∋ < ord→od ox , ord→od oy > |
125 lemma2 : {op ox oy : Ordinal } → ord-pair op ≡ ord-pair (od→ord ( < ord→od ox , ord→od oy > )) | 126 lemma55 {ox} {oy} = pair ox oy |
126 lemma2 = {!!} | 127 |
127 lemma0 : {op ox oy : Ordinal } → ( p : ord-pair (od→ord ( < ord→od ox , ord→od oy > ))) → pi1 p ≡ ox | 128 lemma66 : {ox oy : Ordinal } → pair ( pi1 ( pair ox oy )) ( pi2 ( pair ox oy )) ≡ pair ox oy |
128 lemma0 = {!!} | 129 lemma66 = refl |
129 lemma3 : {ox oy : Ordinal } ( p : ord-pair (od→ord ( < ord→od ox , ord→od oy > )) ) → pi1 p ≡ ox | 130 |
130 lemma3 {ox} {oy} p = {!!} | 131 lemma77 : {ox oy : Ordinal } → ZFProduct ∋ < ord→od (pi1 ( pair ox oy )) , ord→od (pi2 ( pair ox oy )) > ≡ ZFProduct ∋ < ord→od ox , ord→od oy > |
131 lemma4 : {ox oy : Ordinal } → ord-pair (od→ord < ord→od ox , ord→od oy > ) ≡ ZFProduct ∋ < ord→od ox , ord→od oy > | 132 lemma77 = refl |
132 lemma4 = refl | 133 |
133 lemma : {p : OD } → ord-pair (od→ord p) ≡ ZFProduct ∋ p | 134 p-iso3 : { ox oy : Ordinal } → (p : ZFProduct ∋ < ord→od ox , ord→od oy > ) → p ≡ pair ox oy |
134 lemma = refl | 135 p-iso3 p = {!!} where |
136 lemma0 : {ox oy : Ordinal } → ord-pair (od→ord < ord→od ox , ord→od oy >) ≡ ZFProduct ∋ < ord→od ox , ord→od oy > | |
137 lemma0 = refl | |
138 lemma1 : {op ox oy : Ordinal } → op ≡ od→ord < ord→od ox , ord→od oy > → ord-pair op ≡ ZFProduct ∋ < ord→od ox , ord→od oy > | |
139 lemma1 refl = refl | |
140 lemma : {op ox oy : Ordinal } → (p : ord-pair op ) → od→ord < ord→od ox , ord→od oy > ≡ op → p ≅ pair ox oy | |
141 lemma {op} {ox} {oy} (pair ox' oy') eq = {!!} | |
142 | |
143 | |
144 p-iso2 : { ox oy : Ordinal } → p-cons (ord→od ox) (ord→od oy) ≡ pair ox oy | |
145 p-iso2 = subst₂ ( λ j k → j ≡ k ) {!!} {!!} refl | |
146 | |
147 p-iso1 : { x y : OD } → (p : ZFProduct ∋ < x , y > ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ < x , y > | |
148 p-iso1 {x} {y} p with p-cons (ord→od (π1 p)) (ord→od (π2 p)) | |
149 ... | t = {!!} | |
150 | |
135 | 151 |
136 p-iso : { x : OD } → (p : ZFProduct ∋ x ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ x | 152 p-iso : { x : OD } → (p : ZFProduct ∋ x ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ x |
137 p-iso {x} p = {!!} | 153 p-iso {x} p = {!!} |
138 | 154 |
139 ∋-p : (A x : OD ) → Dec ( A ∋ x ) | 155 ∋-p : (A x : OD ) → Dec ( A ∋ x ) |