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

comparison cardinal.agda @ 229:5e36744b8dce

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 Mon, 12 Aug 2019 02:26:32 +0900
parents 49736efc822b
children 1b1620e2053c
comparison
equal deleted inserted replaced
228:49736efc822b 229:5e36744b8dce
85 } where 85 } where
86 cardinal-p : (x : Ordinal ) → ( Ordinal ∧ Dec (Onto (Ord x) X) ) 86 cardinal-p : (x : Ordinal ) → ( Ordinal ∧ Dec (Onto (Ord x) X) )
87 cardinal-p x with p∨¬p ( Onto (Ord x) X ) 87 cardinal-p x with p∨¬p ( Onto (Ord x) X )
88 cardinal-p x | case1 True = record { proj1 = x ; proj2 = yes True } 88 cardinal-p x | case1 True = record { proj1 = x ; proj2 = yes True }
89 cardinal-p x | case2 False = record { proj1 = o∅ ; proj2 = no False } 89 cardinal-p x | case2 False = record { proj1 = o∅ ; proj2 = no False }
90 lemma1 : (x : Ordinal) → ((y : Ordinal) → y o< x → Lift (suc n) (y o< (osuc (sup-o (λ x₁ → proj1 (cardinal-p x₁)))) → Onto (Ord y) X)) → 90 S = sup-o (λ x → proj1 (cardinal-p x))
91 Lift (suc n) (x o< (osuc (sup-o (λ x₁ → proj1 (cardinal-p x₁)))) → Onto (Ord x) X) 91 lemma1 : (x : Ordinal) → ((y : Ordinal) → y o< x → Lift (suc n) (y o< (osuc S) → Onto (Ord y) X)) →
92 lemma1 = {!!} 92 Lift (suc n) (x o< (osuc S) → Onto (Ord x) X)
93 onto : Onto (Ord (sup-o (λ x → proj1 (cardinal-p x)))) X 93 lemma1 x prev with trio< x (osuc S)
94 onto with TransFinite {λ x → Lift (suc n) ( x o< osuc (sup-o (λ x → proj1 (cardinal-p x))) → Onto (Ord x) X ) } lemma1 (sup-o (λ x → proj1 (cardinal-p x))) 94 lemma1 x prev | tri< a ¬b ¬c with osuc-≡< a
95 lemma1 x prev | tri< a ¬b ¬c | case1 x=S = {!!}
96 lemma1 x prev | tri< a ¬b ¬c | case2 x<S = {!!}
97 lemma1 x prev | tri≈ ¬a b ¬c = lift ( λ lt → ⊥-elim ( o<¬≡ b lt ))
98 lemma1 x prev | tri> ¬a ¬b c = lift ( λ lt → ⊥-elim ( o<> c lt ))
99 onto : Onto (Ord S) X
100 onto with TransFinite {λ x → Lift (suc n) ( x o< osuc S → Onto (Ord x) X ) } lemma1 S
95 ... | lift t = t <-osuc where 101 ... | lift t = t <-osuc where
96 cmax : (y : Ordinal) → sup-o (λ x → proj1 (cardinal-p x)) o< y → ¬ Onto (Ord y) X 102 cmax : (y : Ordinal) → S o< y → ¬ Onto (Ord y) X
97 cmax y lt ontoy = o<> lt (o<-subst {_} {_} {y} {sup-o (λ x → proj1 (cardinal-p x))} 103 cmax y lt ontoy = o<> lt (o<-subst {_} {_} {y} {S}
98 (sup-o< {λ x → proj1 ( cardinal-p x)}{y} ) lemma refl ) where 104 (sup-o< {λ x → proj1 ( cardinal-p x)}{y} ) lemma refl ) where
99 lemma : proj1 (cardinal-p y) ≡ y 105 lemma : proj1 (cardinal-p y) ≡ y
100 lemma with p∨¬p ( Onto (Ord y) X ) 106 lemma with p∨¬p ( Onto (Ord y) X )
101 lemma | case1 x = refl 107 lemma | case1 x = refl
102 lemma | case2 not = ⊥-elim ( not ontoy ) 108 lemma | case2 not = ⊥-elim ( not ontoy )