Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison cardinal.agda @ 239:b6d80eec5f9e
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 20 Aug 2019 10:36:37 +0900 |
parents | a8c6239176db |
children | c76c812de395 |
comparison
equal
deleted
inserted
replaced
238:a8c6239176db | 239:b6d80eec5f9e |
---|---|
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 π1' : { p : OD } → ZFProduct ∋ p → OD | 36 π1 : { p : OD } → ZFProduct ∋ p → Ordinal |
37 π1' lt = ord→od (pi1 lt) where | 37 π1 lt = pi1 lt where |
38 pi1 : { p : Ordinal } → ord-pair p → Ordinal | 38 pi1 : { p : Ordinal } → ord-pair p → Ordinal |
39 pi1 ( pair x y ) = x | 39 pi1 ( pair x y ) = x |
40 | 40 |
41 π2' : { p : OD } → ZFProduct ∋ p → OD | 41 π2 : { p : OD } → ZFProduct ∋ p → Ordinal |
42 π2' lt = ord→od (pi2 lt) where | 42 π2 lt = pi2 lt where |
43 pi2 : { p : Ordinal } → ord-pair p → Ordinal | 43 pi2 : { p : Ordinal } → ord-pair p → Ordinal |
44 pi2 ( pair x y ) = y | 44 pi2 ( pair x y ) = y |
45 | 45 |
46 p-cons : { x y : OD } → ZFProduct ∋ < x , y > | 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 ( | 47 p-cons {x} {y} = def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl ( |
50 ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩ | 50 ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩ |
51 od→ord < x , y > | 51 od→ord < x , y > |
52 ∎ ) | 52 ∎ ) |
53 | 53 |
54 | 54 |
55 | |
56 record SetProduct ( A B : OD ) : Set n where | |
57 field | |
58 π1 : Ordinal | |
59 π2 : Ordinal | |
60 A∋π1 : def A π1 | |
61 B∋π2 : def B π2 | |
62 -- opair : x ≡ od→ord (Ord ( omax (omax π1 π1) (omax π1 π2) )) -- < π1 , π2 > | |
63 | |
64 open SetProduct | |
65 | |
66 ∋-p : (A x : OD ) → Dec ( A ∋ x ) | 55 ∋-p : (A x : OD ) → Dec ( A ∋ x ) |
67 ∋-p A x with p∨¬p ( A ∋ x ) | 56 ∋-p A x with p∨¬p ( A ∋ x ) |
68 ∋-p A x | case1 t = yes t | 57 ∋-p A x | case1 t = yes t |
69 ∋-p A x | case2 t = no t | 58 ∋-p A x | case2 t = no t |
70 | 59 |
71 _⊗_ : (A B : OD) → OD | 60 _⊗_ : (A B : OD) → OD |
72 A ⊗ B = record { def = λ x → SetProduct A B } | 61 A ⊗ B = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkAB p ) } where |
73 -- A ⊗ B = record { def = λ x → (y z : Ordinal) → def A y ∧ def B z ∧ ( x ≡ od→ord (< ord→od y , ord→od z >) ) } | 62 checkAB : { p : Ordinal } → def ZFProduct p → Set n |
63 checkAB (pair x y) = def A x ∧ def B y | |
74 | 64 |
75 -- Power (Power ( A ∪ B )) ∋ ( A ⊗ B ) | 65 -- Power (Power ( A ∪ B )) ∋ ( A ⊗ B ) |
76 | 66 |
77 Func : ( A B : OD ) → OD | 67 Func : ( A B : OD ) → OD |
78 Func A B = record { def = λ x → def (Power (A ⊗ B)) x } | 68 Func A B = record { def = λ x → def (Power (A ⊗ B)) x } |
79 | 69 |
80 -- power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x) | 70 -- power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x) |
81 | |
82 func←od : { dom cod : OD } → {f : Ordinal } → def (Func dom cod ) f → (Ordinal → Ordinal ) | |
83 func←od {dom} {cod} {f} lt x = sup-o ( λ y → lemma y ) where | |
84 lemma : Ordinal → Ordinal | |
85 lemma 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) | |
86 lemma y | p | no n = o∅ | |
87 lemma y | p | yes f∋y with double-neg-eilm ( p {ord→od y} f∋y ) -- p : {x : OD} → f ∋ x → ¬ ¬ (dom ⊗ cod ∋ x) | |
88 ... | t with decp ( x ≡ π1 t ) | |
89 ... | yes _ = π2 t | |
90 ... | no _ = o∅ | |
91 | 71 |
92 | 72 |
93 func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD | 73 func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD |
94 func→od f dom = Replace dom ( λ x → < x , ord→od (f (od→ord x)) > ) | 74 func→od f dom = Replace dom ( λ x → < x , ord→od (f (od→ord x)) > ) |
95 | 75 |
96 record Func←cd { dom cod : OD } {f : Ordinal } (f<F : def (Func dom cod ) f) : Set n where | 76 record Func←cd { dom cod : OD } {f : Ordinal } (f<F : def (Func dom cod ) f) : Set n where |
97 field | 77 field |
98 func-1 : Ordinal → Ordinal | 78 func-1 : Ordinal → Ordinal |
99 func→od∈Func-1 : (Func dom (Ord (sup-o (λ x → func-1 x)) )) ∋ func→od func-1 dom | 79 func→od∈Func-1 : (Func dom (Ord (sup-o (λ x → func-1 x)) )) ∋ func→od func-1 dom |
100 | 80 |
81 od→func : { dom cod : OD } → {f : Ordinal } → def (Func dom cod ) f → (Ordinal → Ordinal ) | |
82 od→func {dom} {cod} {f} lt x = sup-o ( λ y → lemma y ) where | |
83 lemma2 : {p : Ordinal} → ord-pair p → Ordinal | |
84 lemma2 (pair x1 y1) with decp ( x1 ≡ x) | |
85 lemma2 (pair x1 y1) | yes p = y1 | |
86 lemma2 (pair x1 y1) | no ¬p = o∅ | |
87 lemma : Ordinal → Ordinal | |
88 lemma 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) | |
89 lemma y | p | no n = o∅ | |
90 lemma y | p | yes f∋y = lemma2 (proj1 (double-neg-eilm ( p {ord→od y} f∋y ))) -- p : {y : OD} → f ∋ y → ¬ ¬ (dom ⊗ cod ∋ y) | |
91 | |
101 func←od1 : { dom cod : OD } → {f : Ordinal } → (f<F : def (Func dom cod ) f ) → Func←cd {dom} {cod} {f} f<F | 92 func←od1 : { dom cod : OD } → {f : Ordinal } → (f<F : def (Func dom cod ) f ) → Func←cd {dom} {cod} {f} f<F |
102 func←od1 {dom} {cod} {f} lt = record { func-1 = λ x → sup-o ( λ y → lemma x y ) ; func→od∈Func-1 = {!!} } where | 93 func←od1 {dom} {cod} {f} lt = record { func-1 = λ x → sup-o ( λ y → lemma x y ) ; func→od∈Func-1 = {!!} } where |
103 lemma : Ordinal → Ordinal → Ordinal | 94 lemma : Ordinal → Ordinal → Ordinal |
104 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) | 95 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) |
105 lemma x y | p | no n = o∅ | 96 lemma x y | p | no n = o∅ |
106 lemma x y | p | yes f∋y with double-neg-eilm ( p {ord→od y} f∋y ) -- p : {x : OD} → f ∋ x → ¬ ¬ (dom ⊗ cod ∋ x) | 97 lemma x y | p | yes f∋y with double-neg-eilm ( p {ord→od y} f∋y ) -- p : {x : OD} → f ∋ x → ¬ ¬ (dom ⊗ cod ∋ x) |
107 ... | t with decp ( x ≡ π1 t ) | 98 ... | t with decp ( x ≡ π1 {!!} ) |
108 ... | yes _ = π2 t | 99 ... | yes _ = π2 {!!} |
109 ... | no _ = o∅ | 100 ... | no _ = o∅ |
110 | 101 |
111 func→od∈Func : (f : Ordinal → Ordinal ) ( dom : OD ) → (Func dom (Ord (sup-o (λ x → f x)) )) ∋ func→od f dom | 102 func→od∈Func : (f : Ordinal → Ordinal ) ( dom : OD ) → (Func dom (Ord (sup-o (λ x → f x)) )) ∋ func→od f dom |
112 func→od∈Func f dom = record { proj1 = {!!} ; proj2 = {!!} } | 103 func→od∈Func f dom = record { proj1 = {!!} ; proj2 = {!!} } |
113 | 104 |
131 xmap : Ordinal | 122 xmap : Ordinal |
132 ymap : Ordinal | 123 ymap : Ordinal |
133 xfunc : def (Func X Y) xmap | 124 xfunc : def (Func X Y) xmap |
134 yfunc : def (Func Y X) ymap | 125 yfunc : def (Func Y X) ymap |
135 onto-iso : {y : Ordinal } → (lty : def Y y ) → | 126 onto-iso : {y : Ordinal } → (lty : def Y y ) → |
136 func←od {X} {Y} {xmap} xfunc ( func←od yfunc y ) ≡ y | 127 od→func {X} {Y} {xmap} xfunc ( od→func yfunc y ) ≡ y |
137 | 128 |
138 open Onto | 129 open Onto |
139 | 130 |
140 onto-restrict : {X Y Z : OD} → Onto X Y → ({x : OD} → _⊆_ Z Y {x}) → Onto X Z | 131 onto-restrict : {X Y Z : OD} → Onto X Y → ({x : OD} → _⊆_ Z Y {x}) → Onto X Z |
141 onto-restrict {X} {Y} {Z} onto Z⊆Y = record { | 132 onto-restrict {X} {Y} {Z} onto Z⊆Y = record { |
151 zmap = {!!} | 142 zmap = {!!} |
152 xfunc1 : def (Func X Z) xmap1 | 143 xfunc1 : def (Func X Z) xmap1 |
153 xfunc1 = {!!} | 144 xfunc1 = {!!} |
154 zfunc : def (Func Z X) zmap | 145 zfunc : def (Func Z X) zmap |
155 zfunc = {!!} | 146 zfunc = {!!} |
156 onto-iso1 : {z : Ordinal } → (ltz : def Z z ) → func←od xfunc1 ( func←od zfunc z ) ≡ z | 147 onto-iso1 : {z : Ordinal } → (ltz : def Z z ) → od→func xfunc1 ( od→func zfunc z ) ≡ z |
157 onto-iso1 = {!!} | 148 onto-iso1 = {!!} |
158 | 149 |
159 | 150 |
160 record Cardinal (X : OD ) : Set n where | 151 record Cardinal (X : OD ) : Set n where |
161 field | 152 field |