Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison cardinal.agda @ 242:c10048d69614
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sun, 25 Aug 2019 18:44:41 +0900 |
parents | ccc84f289c98 |
children | f97a2e4df451 |
comparison
equal
deleted
inserted
replaced
241:ccc84f289c98 | 242:c10048d69614 |
---|---|
31 pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) ) | 31 pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) ) |
32 | 32 |
33 ZFProduct : OD | 33 ZFProduct : OD |
34 ZFProduct = record { def = λ x → ord-pair x } | 34 ZFProduct = record { def = λ x → ord-pair x } |
35 | 35 |
36 pi1 : { p : Ordinal } → ord-pair p → Ordinal | |
37 pi1 ( pair x y ) = x | |
38 | |
36 π1 : { p : OD } → ZFProduct ∋ p → Ordinal | 39 π1 : { p : OD } → ZFProduct ∋ p → Ordinal |
37 π1 lt = pi1 lt where | 40 π1 lt = pi1 lt |
38 pi1 : { p : Ordinal } → ord-pair p → Ordinal | 41 |
39 pi1 ( pair x y ) = x | 42 pi2 : { p : Ordinal } → ord-pair p → Ordinal |
43 pi2 ( pair x y ) = y | |
40 | 44 |
41 π2 : { p : OD } → ZFProduct ∋ p → Ordinal | 45 π2 : { p : OD } → ZFProduct ∋ p → Ordinal |
42 π2 lt = pi2 lt where | 46 π2 lt = pi2 lt |
43 pi2 : { p : Ordinal } → ord-pair p → Ordinal | 47 |
44 pi2 ( pair x y ) = y | 48 p-cons : ( x y : OD ) → ZFProduct ∋ < x , y > |
45 | 49 p-cons x y = def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl ( |
46 p-cons : { x y : OD } → ZFProduct ∋ < x , y > | |
47 p-cons {x} {y} = def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl ( | |
48 let open ≡-Reasoning in begin | 50 let open ≡-Reasoning in begin |
49 od→ord < ord→od (od→ord x) , ord→od (od→ord y) > | 51 od→ord < ord→od (od→ord x) , ord→od (od→ord y) > |
50 ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩ | 52 ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩ |
51 od→ord < x , y > | 53 od→ord < x , y > |
52 ∎ ) | 54 ∎ ) |
55 | |
56 π1-iso : { x y : OD } → π1 ( p-cons x y ) ≡ od→ord x | |
57 π1-iso {x} {y} = {!!} where | |
58 lemma : {ox oy : Ordinal} → pi1 ( pair ox oy ) ≡ ox | |
59 lemma = refl | |
60 lemma2 : {ox oy : Ordinal} → | |
61 def-subst {ZFProduct} {_} (pair (od→ord (ord→od ox)) (od→ord (ord→od oy))) refl (trans (cong₂ (λ j k → od→ord < j , k >) oiso oiso) refl) ≡ pair ox oy | |
62 lemma2 {ox} {oy} = let open ≡-Reasoning in begin | |
63 def-subst {ZFProduct} {_} (pair (od→ord (ord→od ox)) (od→ord (ord→od oy))) refl (trans (cong₂ (λ j k → od→ord < j , k >) oiso oiso) refl) | |
64 ≡⟨ ? ⟩ | |
65 pair ox oy | |
66 ∎ | |
67 lemma1 : {ox oy : Ordinal} → π1 ( p-cons (ord→od ox) (ord→od oy) ) ≡ ox | |
68 lemma1 {ox} {oy} = let open ≡-Reasoning in begin | |
69 π1 ( p-cons (ord→od ox) (ord→od oy) ) | |
70 ≡⟨⟩ | |
71 pi1 (pair (pi1 (def-subst {ZFProduct} {_} (pair (od→ord (ord→od ox)) (od→ord (ord→od oy))) refl (trans (cong₂ (λ j k → od→ord < j , k >) oiso oiso) refl))) oy ) | |
72 ≡⟨ cong (λ k → pi1 k) lemma2 ⟩ | |
73 pi1 (pair ox oy ) | |
74 ≡⟨ lemma {ox} {oy} ⟩ | |
75 ox | |
76 ∎ | |
77 | |
78 p-iso : { x : OD } → {p : ZFProduct ∋ x } → < ord→od (π1 p) , ord→od (π2 p) > ≡ x | |
79 p-iso {x} {p} = pi p pc where | |
80 pc : ZFProduct ∋ < ord→od (π1 p) , ord→od (π2 p) > | |
81 pc = p-cons (ord→od (π1 p)) (ord→od (π2 p)) | |
82 pi : { prod prod1 : Ordinal } → ord-pair prod → ord-pair prod1 → {!!} | |
83 pi (pair p1 p2) (pair q1 q2) = {!!} | |
84 | |
53 | 85 |
54 | 86 |
55 ∋-p : (A x : OD ) → Dec ( A ∋ x ) | 87 ∋-p : (A x : OD ) → Dec ( A ∋ x ) |
56 ∋-p A x with p∨¬p ( A ∋ x ) | 88 ∋-p A x with p∨¬p ( A ∋ x ) |
57 ∋-p A x | case1 t = yes t | 89 ∋-p A x | case1 t = yes t |
60 _⊗_ : (A B : OD) → OD | 92 _⊗_ : (A B : OD) → OD |
61 A ⊗ B = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkAB p ) } where | 93 A ⊗ B = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkAB p ) } where |
62 checkAB : { p : Ordinal } → def ZFProduct p → Set n | 94 checkAB : { p : Ordinal } → def ZFProduct p → Set n |
63 checkAB (pair x y) = def A x ∧ def B y | 95 checkAB (pair x y) = def A x ∧ def B y |
64 | 96 |
97 func→od0 : (f : Ordinal → Ordinal ) → OD | |
98 func→od0 f = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkfunc p ) } where | |
99 checkfunc : { p : Ordinal } → def ZFProduct p → Set n | |
100 checkfunc (pair x y) = f x ≡ y | |
101 | |
65 -- Power (Power ( A ∪ B )) ∋ ( A ⊗ B ) | 102 -- Power (Power ( A ∪ B )) ∋ ( A ⊗ B ) |
66 | 103 |
67 Func : ( A B : OD ) → OD | 104 Func : ( A B : OD ) → OD |
68 Func A B = record { def = λ x → def (Power (A ⊗ B)) x } | 105 Func A B = record { def = λ x → def (Power (A ⊗ B)) x } |
69 | 106 |
71 | 108 |
72 | 109 |
73 func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD | 110 func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD |
74 func→od f dom = Replace dom ( λ x → < x , ord→od (f (od→ord x)) > ) | 111 func→od f dom = Replace dom ( λ x → < x , ord→od (f (od→ord x)) > ) |
75 | 112 |
76 record Func←cd { dom cod : OD } {f : Ordinal } (f<F : def (Func dom cod ) f) : Set n where | 113 record Func←cd { dom cod : OD } {f : Ordinal } : Set n where |
77 field | 114 field |
78 func-1 : Ordinal → Ordinal | 115 func-1 : Ordinal → Ordinal |
79 func→od∈Func-1 : (Func dom (Ord (sup-o (λ x → func-1 x)) )) ∋ func→od func-1 dom | 116 func→od∈Func-1 : Func dom cod ∋ func→od func-1 dom |
80 | 117 |
81 od→func : { dom cod : OD } → {f : Ordinal } → (f<F : def (Func dom cod ) f ) → Func←cd {dom} {cod} {f} f<F | 118 od→func : { dom cod : OD } → {f : Ordinal } → def (Func dom cod ) f → Func←cd {dom} {cod} {f} |
82 od→func {dom} {cod} {f} lt = record { func-1 = λ x → sup-o ( λ y → lemma x y ) ; func→od∈Func-1 = record { proj1 = {!!} ; proj2 = {!!} } } where | 119 od→func {dom} {cod} {f} lt = record { func-1 = λ x → sup-o ( λ y → lemma x y ) ; func→od∈Func-1 = record { proj1 = {!!} ; proj2 = {!!} } } where |
83 lemma : Ordinal → Ordinal → Ordinal | 120 lemma : Ordinal → Ordinal → Ordinal |
84 lemma x y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → def (Power (dom ⊗ cod)) k ) (sym diso) lt ) | ∋-p (ord→od f) (ord→od y) | 121 lemma x y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → def (Power (dom ⊗ cod)) k ) (sym diso) lt ) | ∋-p (ord→od f) (ord→od y) |
85 lemma x y | p | no n = o∅ | 122 lemma x y | p | no n = o∅ |
86 lemma x y | p | yes f∋y = lemma2 (proj1 (double-neg-eilm ( p {ord→od y} f∋y ))) where -- p : {y : OD} → f ∋ y → ¬ ¬ (dom ⊗ cod ∋ y) | 123 lemma x y | p | yes f∋y = lemma2 (proj1 (double-neg-eilm ( p {ord→od y} f∋y ))) where -- p : {y : OD} → f ∋ y → ¬ ¬ (dom ⊗ cod ∋ y) |
87 lemma2 : {p : Ordinal} → ord-pair p → Ordinal | 124 lemma2 : {p : Ordinal} → ord-pair p → Ordinal |
88 lemma2 (pair x1 y1) with decp ( x1 ≡ x) | 125 lemma2 (pair x1 y1) with decp ( x1 ≡ x) |
89 lemma2 (pair x1 y1) | yes p = y1 | 126 lemma2 (pair x1 y1) | yes p = y1 |
90 lemma2 (pair x1 y1) | no ¬p = o∅ | 127 lemma2 (pair x1 y1) | no ¬p = o∅ |
128 fod : OD | |
129 fod = Replace dom ( λ x → < x , ord→od (sup-o ( λ y → lemma (od→ord x) y )) > ) | |
91 | 130 |
92 | 131 |
93 open Func←cd | 132 open Func←cd |
94 | |
95 func→od∈Func : (f : Ordinal → Ordinal ) ( dom : OD ) → (Func dom (Ord (sup-o (λ x → f x)) )) ∋ func→od f dom | |
96 func→od∈Func f dom = record { proj1 = {!!} ; proj2 = {!!} } where | |
97 f<F : def (Func dom (Ord (sup-o (λ x → f x)))) (od→ord (func→od f dom)) | |
98 f<F = {!!} | |
99 odfunc : Func←cd {dom} f<F | |
100 odfunc = ( od→func {dom} {Ord (sup-o (λ x → f x))} {od→ord (func→od f dom)} f<F ) | |
101 lemma : Func dom (Ord (sup-o ( func-1 odfunc ) )) ∋ func→od (func-1 odfunc ) dom | |
102 lemma = func→od∈Func-1 odfunc | |
103 | 133 |
104 -- contra position of sup-o< | 134 -- contra position of sup-o< |
105 -- | 135 -- |
106 | 136 |
107 -- postulate | 137 -- postulate |