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

comparison cardinal.agda @ 234:e06b76e5b682

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ac from LEM in abstract ordinal
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 13 Aug 2019 22:21:10 +0900
parents af60c40298a4
children 846e0926bb89
comparison
equal deleted inserted replaced
233:af60c40298a4 234:e06b76e5b682
35 B∋π2 : def B π2 35 B∋π2 : def B π2
36 -- opair : x ≡ od→ord (Ord ( omax (omax π1 π1) (omax π1 π2) )) -- < π1 , π2 > 36 -- opair : x ≡ od→ord (Ord ( omax (omax π1 π1) (omax π1 π2) )) -- < π1 , π2 >
37 37
38 open SetProduct 38 open SetProduct
39 39
40 ∋-p : (A x : OD ) → Dec ( A ∋ x )
41 ∋-p A x with p∨¬p ( A ∋ x )
42 ∋-p A x | case1 t = yes t
43 ∋-p A x | case2 t = no t
44
40 _⊗_ : (A B : OD) → OD 45 _⊗_ : (A B : OD) → OD
41 A ⊗ B = record { def = λ x → SetProduct A B x } 46 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 >) ) } 47 -- A ⊗ B = record { def = λ x → (y z : Ordinal) → def A y ∧ def B z ∧ ( x ≡ od→ord (< ord→od y , ord→od z >) ) }
43 48
44 -- Power (Power ( A ∪ B )) ∋ ( A ⊗ B ) 49 -- Power (Power ( A ∪ B )) ∋ ( A ⊗ B )
46 Func : ( A B : OD ) → OD 51 Func : ( A B : OD ) → OD
47 Func A B = record { def = λ x → def (Power (A ⊗ B)) x } 52 Func A B = record { def = λ x → def (Power (A ⊗ B)) x }
48 53
49 -- power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x) 54 -- power→ : ( A t : OD) → Power A ∋ t → {x : OD} → t ∋ x → ¬ ¬ (A ∋ x)
50 55
51 func←od : { dom cod : OD } → {f : OD } → Func dom cod ∋ f → (Ordinal → Ordinal ) 56 func←od : { dom cod : OD } → {f : Ordinal } → def (Func dom cod ) f → (Ordinal → Ordinal )
52 func←od {dom} {cod} {f} lt x = sup-o ( λ y → lemma y ) where 57 func←od {dom} {cod} {f} lt x = sup-o ( λ y → lemma y ) where
58 lemma1 = subst (λ k → def (Power (dom ⊗ cod)) k ) (sym {!!}) lt
53 lemma : Ordinal → Ordinal 59 lemma : Ordinal → Ordinal
54 lemma y with IsZF.power→ isZF (dom ⊗ cod) f lt 60 lemma y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → def (Power (dom ⊗ cod)) k ) {!!} lt ) | ∋-p (ord→od f) (ord→od y)
55 lemma y | p with double-neg-eilm ( p {ord→od y} {!!} ) -- p : {x : OD} → f ∋ x → ¬ ¬ (dom ⊗ cod ∋ x) 61 lemma y | p | no n = o∅
56 ... | t = π2 t 62 lemma y | p | yes f∋y with double-neg-eilm ( p {ord→od y} f∋y ) -- p : {x : OD} → f ∋ x → ¬ ¬ (dom ⊗ cod ∋ x)
63 ... | t with decp ( x ≡ π1 t )
64 ... | yes _ = π2 t
65 ... | no _ = o∅
57 66
58 func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD 67 func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD
59 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)) > )
60 69
61 70
78 field 87 field
79 xmap : Ordinal 88 xmap : Ordinal
80 ymap : Ordinal 89 ymap : Ordinal
81 xfunc : def (Func X Y) xmap 90 xfunc : def (Func X Y) xmap
82 yfunc : def (Func Y X) ymap 91 yfunc : def (Func Y X) ymap
83 onto-iso : {y : Ordinal } → (lty : def Y y ) → func←od {!!} ( func←od {!!} y ) ≡ y 92 onto-iso : {y : Ordinal } → (lty : def Y y ) →
93 func←od {X} {Y} {xmap} xfunc ( func←od yfunc y ) ≡ y
84 94
85 open Onto 95 open Onto
86 96
87 onto-restrict : {X Y Z : OD} → Onto X Y → ({x : OD} → _⊆_ Z Y {x}) → Onto X Z 97 onto-restrict : {X Y Z : OD} → Onto X Y → ({x : OD} → _⊆_ Z Y {x}) → Onto X Z
88 onto-restrict {X} {Y} {Z} onto Z⊆Y = record { 98 onto-restrict {X} {Y} {Z} onto Z⊆Y = record {
98 zmap = {!!} 108 zmap = {!!}
99 xfunc1 : def (Func X Z) xmap1 109 xfunc1 : def (Func X Z) xmap1
100 xfunc1 = {!!} 110 xfunc1 = {!!}
101 zfunc : def (Func Z X) zmap 111 zfunc : def (Func Z X) zmap
102 zfunc = {!!} 112 zfunc = {!!}
103 onto-iso1 : {z : Ordinal } → (ltz : def Z z ) → func←od {!!} ( func←od zfunc z ) ≡ z 113 onto-iso1 : {z : Ordinal } → (ltz : def Z z ) → func←od xfunc1 ( func←od zfunc z ) ≡ z
104 onto-iso1 = {!!} 114 onto-iso1 = {!!}
105 115
106 116
107 record Cardinal (X : OD ) : Set n where 117 record Cardinal (X : OD ) : Set n where
108 field 118 field