Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison cardinal.agda @ 240:c76c812de395
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 |