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

comparison cardinal.agda @ 236:650bdad56729

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 16 Aug 2019 15:53:29 +0900
parents 846e0926bb89
children 521290e85527
comparison
equal deleted inserted replaced
235:846e0926bb89 236:650bdad56729
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 <_,_> : (x y : OD) → OD 27 <_,_> : (x y : OD) → OD
28 < x , y > = (x , x ) , (x , y ) 28 < x , y > = (x , x ) , (x , y )
29 29
30 record SetProduct ( A B : OD ) (x : Ordinal ) : Set n where 30 record SetProduct ( A B : OD ) : Set n where
31 field 31 field
32 π1 : Ordinal 32 π1 : Ordinal
33 π2 : Ordinal 33 π2 : Ordinal
34 A∋π1 : def A π1 34 A∋π1 : def A π1
35 B∋π2 : def B π2 35 B∋π2 : def B π2
41 ∋-p A x with p∨¬p ( A ∋ x ) 41 ∋-p A x with p∨¬p ( A ∋ x )
42 ∋-p A x | case1 t = yes t 42 ∋-p A x | case1 t = yes t
43 ∋-p A x | case2 t = no t 43 ∋-p A x | case2 t = no t
44 44
45 _⊗_ : (A B : OD) → OD 45 _⊗_ : (A B : OD) → OD
46 A ⊗ B = record { def = λ x → SetProduct A B x } 46 A ⊗ B = record { def = λ x → SetProduct A B }
47 -- A ⊗ B = record { def = λ x → (y z : Ordinal) → def A y ∧ def B z ∧ ( x ≡ od→ord (< ord→od y , ord→od z >) ) } 47 -- A ⊗ B = record { def = λ x → (y z : Ordinal) → def A y ∧ def B z ∧ ( x ≡ od→ord (< ord→od y , ord→od z >) ) }
48 48
49 -- Power (Power ( A ∪ B )) ∋ ( A ⊗ B ) 49 -- Power (Power ( A ∪ B )) ∋ ( A ⊗ B )
50 50
51 Func : ( A B : OD ) → OD 51 Func : ( A B : OD ) → OD
61 lemma y | p | yes f∋y with double-neg-eilm ( p {ord→od y} f∋y ) -- p : {x : OD} → f ∋ x → ¬ ¬ (dom ⊗ cod ∋ x) 61 lemma y | p | yes f∋y with double-neg-eilm ( p {ord→od y} f∋y ) -- p : {x : OD} → f ∋ x → ¬ ¬ (dom ⊗ cod ∋ x)
62 ... | t with decp ( x ≡ π1 t ) 62 ... | t with decp ( x ≡ π1 t )
63 ... | yes _ = π2 t 63 ... | yes _ = π2 t
64 ... | no _ = o∅ 64 ... | no _ = o∅
65 65
66
66 func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD 67 func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD
67 func→od f dom = Replace dom ( λ x → < x , ord→od (f (od→ord x)) > ) 68 func→od f dom = Replace dom ( λ x → < x , ord→od (f (od→ord x)) > )
68 69
70 record Func←cd { dom cod : OD } {f : Ordinal } (f<F : def (Func dom cod ) f) : Set n where
71 field
72 func-1 : Ordinal → Ordinal
73 func→od∈Func-1 : (Func dom (Ord (sup-o (λ x → func-1 x)) )) ∋ func→od func-1 dom
74
75 func←od1 : { dom cod : OD } → {f : Ordinal } → (f<F : def (Func dom cod ) f ) → Func←cd {dom} {cod} {f} f<F
76 func←od1 {dom} {cod} {f} lt = record { func-1 = λ x → sup-o ( λ y → lemma x y ) ; func→od∈Func-1 = {!!} } where
77 lemma : Ordinal → Ordinal → Ordinal
78 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)
79 lemma x y | p | no n = o∅
80 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)
81 ... | t with decp ( x ≡ π1 t )
82 ... | yes _ = π2 t
83 ... | no _ = o∅
84
85 func→od∈Func : (f : Ordinal → Ordinal ) ( dom : OD ) → (Func dom (Ord (sup-o (λ x → f x)) )) ∋ func→od f dom
86 func→od∈Func f dom = record { proj1 = {!!} ; proj2 = {!!} }
69 87
70 -- contra position of sup-o< 88 -- contra position of sup-o<
71 -- 89 --
72 90
73 -- postulate 91 -- postulate