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

comparison cardinal.agda @ 240:c76c812de395

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 21 Aug 2019 16:43:29 +0900
parents b6d80eec5f9e
children ccc84f289c98
comparison
equal deleted inserted replaced
239:b6d80eec5f9e 240:c76c812de395
76 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
77 field 77 field
78 func-1 : Ordinal → Ordinal 78 func-1 : Ordinal → Ordinal
79 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
80 80
81 od→func : { dom cod : OD } → {f : Ordinal } → def (Func dom cod ) f → (Ordinal → Ordinal ) 81 od→func : { dom cod : OD } → {f : Ordinal } → (f<F : def (Func dom cod ) f ) → Func←cd {dom} {cod} {f} f<F
82 od→func {dom} {cod} {f} lt x = sup-o ( λ y → lemma y ) where 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
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
92 func←od1 : { dom cod : OD } → {f : Ordinal } → (f<F : def (Func dom cod ) f ) → Func←cd {dom} {cod} {f} f<F
93 func←od1 {dom} {cod} {f} lt = record { func-1 = λ x → sup-o ( λ y → lemma x y ) ; func→od∈Func-1 = {!!} } where
94 lemma : Ordinal → Ordinal → Ordinal 83 lemma : Ordinal → Ordinal → Ordinal
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) 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)
96 lemma x y | p | no n = o∅ 85 lemma x y | p | no n = o∅
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) 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)
98 ... | t with decp ( x ≡ π1 {!!} ) 87 lemma2 : {p : Ordinal} → ord-pair p → Ordinal
99 ... | yes _ = π2 {!!} 88 lemma2 (pair x1 y1) with decp ( x1 ≡ x)
100 ... | no _ = o∅ 89 lemma2 (pair x1 y1) | yes p = y1
90 lemma2 (pair x1 y1) | no ¬p = o∅
91
92
93 open Func←cd
101 94
102 func→od∈Func : (f : Ordinal → Ordinal ) ( dom : OD ) → (Func dom (Ord (sup-o (λ x → f x)) )) ∋ func→od f dom 95 func→od∈Func : (f : Ordinal → Ordinal ) ( dom : OD ) → (Func dom (Ord (sup-o (λ x → f x)) )) ∋ func→od f dom
103 func→od∈Func f dom = record { proj1 = {!!} ; proj2 = {!!} } 96 func→od∈Func f dom = record { proj1 = {!!} ; proj2 = {!!} } where
97 lemma : (Func dom (Ord (sup-o (λ x → f x)) )) ∋ func→od f dom
98 lemma = {!!} -- func→od∈Func-1 ( od→func {dom} {{!!}} {od→ord (func→od f {!!} )} {!!} )
104 99
105 -- contra position of sup-o< 100 -- contra position of sup-o<
106 -- 101 --
107 102
108 -- postulate 103 -- postulate
122 xmap : Ordinal 117 xmap : Ordinal
123 ymap : Ordinal 118 ymap : Ordinal
124 xfunc : def (Func X Y) xmap 119 xfunc : def (Func X Y) xmap
125 yfunc : def (Func Y X) ymap 120 yfunc : def (Func Y X) ymap
126 onto-iso : {y : Ordinal } → (lty : def Y y ) → 121 onto-iso : {y : Ordinal } → (lty : def Y y ) →
127 od→func {X} {Y} {xmap} xfunc ( od→func yfunc y ) ≡ y 122 func-1 ( od→func {X} {Y} {xmap} xfunc ) ( func-1 (od→func yfunc) y ) ≡ y
128 123
129 open Onto 124 open Onto
130 125
131 onto-restrict : {X Y Z : OD} → Onto X Y → ({x : OD} → _⊆_ Z Y {x}) → Onto X Z 126 onto-restrict : {X Y Z : OD} → Onto X Y → ({x : OD} → _⊆_ Z Y {x}) → Onto X Z
132 onto-restrict {X} {Y} {Z} onto Z⊆Y = record { 127 onto-restrict {X} {Y} {Z} onto Z⊆Y = record {
142 zmap = {!!} 137 zmap = {!!}
143 xfunc1 : def (Func X Z) xmap1 138 xfunc1 : def (Func X Z) xmap1
144 xfunc1 = {!!} 139 xfunc1 = {!!}
145 zfunc : def (Func Z X) zmap 140 zfunc : def (Func Z X) zmap
146 zfunc = {!!} 141 zfunc = {!!}
147 onto-iso1 : {z : Ordinal } → (ltz : def Z z ) → od→func xfunc1 ( od→func zfunc z ) ≡ z 142 onto-iso1 : {z : Ordinal } → (ltz : def Z z ) → func-1 (od→func xfunc1 ) (func-1 (od→func zfunc ) z ) ≡ z
148 onto-iso1 = {!!} 143 onto-iso1 = {!!}
149 144
150 145
151 record Cardinal (X : OD ) : Set n where 146 record Cardinal (X : OD ) : Set n where
152 field 147 field