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

comparison ordinal-definable.agda @ 79:c07c548b2ac1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add some lemma
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 03 Jun 2019 10:50:03 +0900
parents 9a7a64b2388c
children 461690d60d07
comparison
equal deleted inserted replaced
78:9a7a64b2388c 79:c07c548b2ac1
181 o<→o> {n} {x} {y} record { eq→ = xy ; eq← = yx } (case2 lt) with 181 o<→o> {n} {x} {y} record { eq→ = xy ; eq← = yx } (case2 lt) with
182 yx (def-subst {n} {ord→od (od→ord y)} {od→ord (ord→od (od→ord x))} (o<→c< (case2 lt )) oiso diso ) 182 yx (def-subst {n} {ord→od (od→ord y)} {od→ord (ord→od (od→ord x))} (o<→c< (case2 lt )) oiso diso )
183 ... | oyx with o<¬≡ (od→ord x) (od→ord x) refl (c<→o< oyx ) 183 ... | oyx with o<¬≡ (od→ord x) (od→ord x) refl (c<→o< oyx )
184 ... | () 184 ... | ()
185 185
186 ==→o≡ : {n : Level} → { x y : Ordinal {suc n} } → ord→od x == ord→od y → x ≡ y
187 ==→o≡ {n} {x} {y} eq with trio< {n} x y
188 ==→o≡ {n} {x} {y} eq | tri< a ¬b ¬c = ⊥-elim ( o<→o> eq (o<-subst a (sym ord-iso) (sym ord-iso )))
189 ==→o≡ {n} {x} {y} eq | tri≈ ¬a b ¬c = b
190 ==→o≡ {n} {x} {y} eq | tri> ¬a ¬b c = ⊥-elim ( o<→o> (eq-sym eq) (o<-subst c (sym ord-iso) (sym ord-iso )))
191
186 o<→¬== : {n : Level} → { x y : OD {n} } → (od→ord x ) o< ( od→ord y) → ¬ (x == y ) 192 o<→¬== : {n : Level} → { x y : OD {n} } → (od→ord x ) o< ( od→ord y) → ¬ (x == y )
187 o<→¬== {n} {x} {y} lt eq = o<→o> eq lt 193 o<→¬== {n} {x} {y} lt eq = o<→o> eq lt
188 194
189 o<→¬c> : {n : Level} → { x y : OD {n} } → (od→ord x ) o< ( od→ord y) → ¬ (y c< x ) 195 o<→¬c> : {n : Level} → { x y : OD {n} } → (od→ord x ) o< ( od→ord y) → ¬ (y c< x )
190 o<→¬c> {n} {x} {y} olt clt = o<> (od→ord x) (od→ord y) olt (c<→o< clt ) where 196 o<→¬c> {n} {x} {y} olt clt = o<> (od→ord x) (od→ord y) olt (c<→o< clt ) where
235 lemma1 : od→ord (ord→od o∅) ≡ od→ord od∅ 241 lemma1 : od→ord (ord→od o∅) ≡ od→ord od∅
236 lemma1 = cong ( λ k → od→ord k ) o∅→od∅ 242 lemma1 = cong ( λ k → od→ord k ) o∅→od∅
237 lemma o∅ ne | yes refl | () 243 lemma o∅ ne | yes refl | ()
238 lemma ox ne | no ¬p = subst ( λ k → def (ord→od ox) (od→ord k) ) o∅→od∅ (o<→c< (∅5 ¬p)) 244 lemma ox ne | no ¬p = subst ( λ k → def (ord→od ox) (od→ord k) ) o∅→od∅ (o<→c< (∅5 ¬p))
239 245
240 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 246 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
241 247
242 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} 248 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
243 OD→ZF {n} = record { 249 OD→ZF {n} = record {
244 ZFSet = OD {suc n} 250 ZFSet = OD {suc n}
245 ; _∋_ = _∋_ 251 ; _∋_ = _∋_