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

comparison cardinal.agda @ 233:af60c40298a4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
function continue
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 12 Aug 2019 13:28:59 +0900
parents 1b1620e2053c
children e06b76e5b682
comparison
equal deleted inserted replaced
231:cb6f025a991e 233:af60c40298a4
22 open Bool 22 open Bool
23 23
24 -- we have to work on Ordinal to keep OD Level n 24 -- we have to work on Ordinal to keep OD Level n
25 -- since we use p∨¬p which works only on Level n 25 -- since we use p∨¬p which works only on Level n
26 26
27 func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD 27 <_,_> : (x y : OD) → OD
28 func→od f dom = Replace dom ( λ x → x , (ord→od (f (od→ord x) ))) 28 < x , y > = (x , x ) , (x , y )
29 29
30 record _⊗_ (A B : Ordinal) : Set n where 30 record SetProduct ( A B : OD ) (x : Ordinal ) : Set n where
31 field 31 field
32 π1 : Ordinal 32 π1 : Ordinal
33 π2 : Ordinal 33 π2 : Ordinal
34 A∋π1 : def (ord→od A) π1 34 A∋π1 : def A π1
35 B∋π2 : def (ord→od B) π2 35 B∋π2 : def B π2
36 -- opair : x ≡ od→ord (Ord ( omax (omax π1 π1) (omax π1 π2) )) -- < π1 , π2 >
36 37
37 -- Clearly wrong. We need ordered pair 38 open SetProduct
39
40 _⊗_ : (A B : OD) → OD
41 A ⊗ B = record { def = λ x → SetProduct A B x }
42 -- A ⊗ B = record { def = λ x → (y z : Ordinal) → def A y ∧ def B z ∧ ( x ≡ od→ord (< ord→od y , ord→od z >) ) }
43
44 -- Power (Power ( A ∪ B )) ∋ ( A ⊗ B )
45
38 Func : ( A B : OD ) → OD 46 Func : ( A B : OD ) → OD
39 Func A B = record { def = λ x → (od→ord A) ⊗ (od→ord B) } 47 Func A B = record { def = λ x → def (Power (A ⊗ B)) x }
40 48
41 open _⊗_ 49 -- power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)
42 50
43 func←od : { dom cod : OD } → (f : OD ) → Func dom cod ∋ f → (Ordinal → Ordinal ) 51 func←od : { dom cod : OD } → {f : OD } → Func dom cod ∋ f → (Ordinal → Ordinal )
44 func←od {dom} {cod} f lt x = sup-o ( λ y → lemma y ) where 52 func←od {dom} {cod} {f} lt x = sup-o ( λ y → lemma y ) where
45 lemma : Ordinal → Ordinal 53 lemma : Ordinal → Ordinal
46 lemma y with p∨¬p ( _⊗_.π1 lt ≡ x ) 54 lemma y with IsZF.power→ isZF (dom ⊗ cod) f lt
47 lemma y | case1 refl = _⊗_.π2 lt 55 lemma y | p with double-neg-eilm ( p {ord→od y} {!!} ) -- p : {x : OD} → f ∋ x → ¬ ¬ (dom ⊗ cod ∋ x)
48 lemma y | case2 not = o∅ 56 ... | t = π2 t
57
58 func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD
59 func→od f dom = Replace dom ( λ x → < x , ord→od (f (od→ord x)) > )
60
49 61
50 -- contra position of sup-o< 62 -- contra position of sup-o<
51 -- 63 --
52 64
53 postulate 65 postulate
66 field 78 field
67 xmap : Ordinal 79 xmap : Ordinal
68 ymap : Ordinal 80 ymap : Ordinal
69 xfunc : def (Func X Y) xmap 81 xfunc : def (Func X Y) xmap
70 yfunc : def (Func Y X) ymap 82 yfunc : def (Func Y X) ymap
71 onto-iso : {y : Ordinal } → (lty : def Y y ) → func←od (ord→od xmap) xfunc ( func←od (ord→od ymap) yfunc y ) ≡ y 83 onto-iso : {y : Ordinal } → (lty : def Y y ) → func←od {!!} ( func←od {!!} y ) ≡ y
72 84
73 open Onto 85 open Onto
74 86
75 onto-restrict : {X Y Z : OD} → Onto X Y → ({x : OD} → _⊆_ Z Y {x}) → Onto X Z 87 onto-restrict : {X Y Z : OD} → Onto X Y → ({x : OD} → _⊆_ Z Y {x}) → Onto X Z
76 onto-restrict {X} {Y} {Z} onto Z⊆Y = record { 88 onto-restrict {X} {Y} {Z} onto Z⊆Y = record {
86 zmap = {!!} 98 zmap = {!!}
87 xfunc1 : def (Func X Z) xmap1 99 xfunc1 : def (Func X Z) xmap1
88 xfunc1 = {!!} 100 xfunc1 = {!!}
89 zfunc : def (Func Z X) zmap 101 zfunc : def (Func Z X) zmap
90 zfunc = {!!} 102 zfunc = {!!}
91 onto-iso1 : {z : Ordinal } → (ltz : def Z z ) → func←od (ord→od xmap1) xfunc1 ( func←od (ord→od zmap) zfunc z ) ≡ z 103 onto-iso1 : {z : Ordinal } → (ltz : def Z z ) → func←od {!!} ( func←od zfunc z ) ≡ z
92 onto-iso1 = {!!} 104 onto-iso1 = {!!}
93 105
94 106
95 record Cardinal (X : OD ) : Set n where 107 record Cardinal (X : OD ) : Set n where
96 field 108 field