Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison cardinal.agda @ 251:9e0125b06e76
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 29 Aug 2019 01:04:52 +0900 |
parents | 08428a661677 |
children | 8a58e2cd1f55 |
comparison
equal
deleted
inserted
replaced
250:08428a661677 | 251:9e0125b06e76 |
---|---|
47 ==-sym : { x y : OD } → x == y → y == x | 47 ==-sym : { x y : OD } → x == y → y == x |
48 ==-sym x=y = record { eq→ = λ {m} t → eq← x=y t ; eq← = λ {m} t → eq→ x=y t } | 48 ==-sym x=y = record { eq→ = λ {m} t → eq← x=y t ; eq← = λ {m} t → eq→ x=y t } |
49 | 49 |
50 ord≡→≡ : { x y : OD } → od→ord x ≡ od→ord y → x ≡ y | 50 ord≡→≡ : { x y : OD } → od→ord x ≡ od→ord y → x ≡ y |
51 ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) oiso oiso ( cong ( λ k → ord→od k ) eq ) | 51 ord≡→≡ eq = subst₂ (λ j k → j ≡ k ) oiso oiso ( cong ( λ k → ord→od k ) eq ) |
52 | |
53 od≡→≡ : { x y : Ordinal } → ord→od x ≡ ord→od y → x ≡ y | |
54 od≡→≡ eq = subst₂ (λ j k → j ≡ k ) diso diso ( cong ( λ k → od→ord k ) eq ) | |
52 | 55 |
53 eq-prod : { x x' y y' : OD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' > | 56 eq-prod : { x x' y y' : OD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' > |
54 eq-prod refl refl = refl | 57 eq-prod refl refl = refl |
55 | 58 |
56 prod-eq : { x x' y y' : OD } → < x , y > == < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' ) | 59 prod-eq : { x x' y y' : OD } → < x , y > == < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' ) |
129 lemma66 = refl | 132 lemma66 = refl |
130 | 133 |
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 > | 134 lemma77 : {ox oy : Ordinal } → ZFProduct ∋ < ord→od (pi1 ( pair ox oy )) , ord→od (pi2 ( pair ox oy )) > ≡ ZFProduct ∋ < ord→od ox , ord→od oy > |
132 lemma77 = refl | 135 lemma77 = refl |
133 | 136 |
137 | |
138 p-iso : { x : OD } → (p : ZFProduct ∋ x ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ x | |
139 p-iso {x} p = {!!} where | |
140 | |
141 pair-iso : {op ox oy : Ordinal} (x : ord-pair (od→ord < ord→od ox , ord→od oy >) ) → pi1 x ≡ ox → pi2 x ≡ oy → x ≡ pair ox oy | |
142 pair-iso (pair ox oy) = {!!} | |
143 | |
134 p-iso3 : { ox oy : Ordinal } → (p : ZFProduct ∋ < ord→od ox , ord→od oy > ) → p ≡ pair ox oy | 144 p-iso3 : { ox oy : Ordinal } → (p : ZFProduct ∋ < ord→od ox , ord→od oy > ) → p ≡ pair ox oy |
135 p-iso3 p = {!!} where | 145 p-iso3 {ox} {oy} p with p-iso p |
136 lemma0 : {ox oy : Ordinal } → ord-pair (od→ord < ord→od ox , ord→od oy >) ≡ ZFProduct ∋ < ord→od ox , ord→od oy > | 146 ... | eq with prod-eq ( ord→== (cong (λ k → od→ord k) eq ) ) |
137 lemma0 = refl | 147 ... | record { proj1 = eq1 ; proj2 = eq2 } = lemma eq1 eq2 where |
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 > | 148 lemma : ord→od (pi1 p) ≡ ord→od ox → ord→od (pi2 p) ≡ ord→od oy → p ≡ pair ox oy |
139 lemma1 refl = refl | 149 lemma eq1 eq2 with od≡→≡ eq1 | od≡→≡ eq2 |
140 lemma : {op ox oy : Ordinal } → (p : ord-pair op ) → od→ord < ord→od ox , ord→od oy > ≡ op → p ≅ pair ox oy | 150 ... | eq1' | eq2' = pair-iso {od→ord < ord→od ox , ord→od oy >} {ox} {oy} p eq1' eq2' |
141 lemma {op} {ox} {oy} (pair ox' oy') eq = {!!} | |
142 | |
143 | 151 |
144 p-iso2 : { ox oy : Ordinal } → p-cons (ord→od ox) (ord→od oy) ≡ pair ox oy | 152 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 | 153 p-iso2 {ox} {oy} = p-iso3 (p-cons (ord→od ox) (ord→od oy)) |
146 | 154 |
147 p-iso1 : { x y : OD } → (p : ZFProduct ∋ < x , y > ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ < x , y > | 155 p-iso1 : { ox oy : Ordinal } → (p : ZFProduct ∋ < ord→od ox , ord→od oy > ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ < ord→od ox , ord→od oy > |
148 p-iso1 {x} {y} p with p-cons (ord→od (π1 p)) (ord→od (π2 p)) | 156 p-iso1 {x} {y} p with p-cons (ord→od (π1 p)) (ord→od (π2 p)) |
149 ... | t = {!!} | 157 ... | t with p-iso3 p | p-iso3 t |
158 ... | refl | refl = refl | |
150 | 159 |
151 | |
152 p-iso : { x : OD } → (p : ZFProduct ∋ x ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ x | |
153 p-iso {x} p = {!!} | |
154 | |
155 ∋-p : (A x : OD ) → Dec ( A ∋ x ) | 160 ∋-p : (A x : OD ) → Dec ( A ∋ x ) |
156 ∋-p A x with p∨¬p ( A ∋ x ) | 161 ∋-p A x with p∨¬p ( A ∋ x ) |
157 ∋-p A x | case1 t = yes t | 162 ∋-p A x | case1 t = yes t |
158 ∋-p A x | case2 t = no t | 163 ∋-p A x | case2 t = no t |
159 | 164 |