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

comparison src/ordinal.agda @ 612:099ca2fea51c

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 Fri, 17 Jun 2022 21:20:24 +0900
parents b27d92694ed5
children 4f48fe1b884a 4186c0331abb
comparison
equal deleted inserted replaced
611:d6ad1af5299e 612:099ca2fea51c
198 lemma : (y : Ordinal) → y o< ordinal lx (OSuc lx ox) → ψ y 198 lemma : (y : Ordinal) → y o< ordinal lx (OSuc lx ox) → ψ y
199 lemma y lt with osuc-≡< lt 199 lemma y lt with osuc-≡< lt
200 lemma y lt | case1 refl = proj1 ( TransFinite1 lx ox ) 200 lemma y lt | case1 refl = proj1 ( TransFinite1 lx ox )
201 lemma y lt | case2 lt1 = proj2 ( TransFinite1 lx ox ) y lt1 201 lemma y lt | case2 lt1 = proj2 ( TransFinite1 lx ox ) y lt1
202 202
203 open import Data.Nat.Properties as DP
204 OrdIrr : {n : Level } {x y : Ordinal {suc n} } {lt lt1 : x o< y} → lt ≡ lt1
205 OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case1 x} {case1 x₁} = cong case1 (DP.<-irrelevant _ _ )
206 OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case1 x} {case2 x₁} = ⊥-elim ( nat-≡< ( d<→lv x₁ ) x )
207 OrdIrr {n} {ordinal lv₁ ord₁} {ordinal lv₂ ord₂} {case2 x} {case1 x₁} = ⊥-elim ( nat-≡< ( d<→lv x ) x₁ )
208 OrdIrr {n} {ordinal lv₁ .(Φ lv₁)} {ordinal .lv₁ .(OSuc lv₁ _)} {case2 Φ<} {case2 Φ<} = refl
209 OrdIrr {n} {ordinal lv₁ (OSuc lv₁ a)} {ordinal .lv₁ (OSuc lv₁ b)} {case2 (s< x)} {case2 (s< x₁)} = cong (λ k → case2 (s< k)) (lemma1 _ _ x x₁) where
210 lemma1 : {lx : Nat} (a b : OrdinalD {suc n} lx) → (x y : a d< b ) → x ≡ y
211 lemma1 {lx} .(Φ lx) .(OSuc lx _) Φ< Φ< = refl
212 lemma1 {lx} (OSuc lx a) (OSuc lx b) (s< x) (s< y) = cong s< (lemma1 {lx} a b x y )
213
203 open import Ordinals 214 open import Ordinals
204 215
205 C-Ordinal : {n : Level} → Ordinals {suc n} 216 C-Ordinal : {n : Level} → Ordinals {suc n}
206 C-Ordinal {n} = record { 217 C-Ordinal {n} = record {
207 Ordinal = Ordinal {suc n} 218 Ordinal = Ordinal {suc n}
214 ; trio< = trio< 225 ; trio< = trio<
215 ; ¬x<0 = ¬x<0 226 ; ¬x<0 = ¬x<0
216 ; <-osuc = <-osuc 227 ; <-osuc = <-osuc
217 ; osuc-≡< = osuc-≡< 228 ; osuc-≡< = osuc-≡<
218 ; TransFinite = TransFinite2 229 ; TransFinite = TransFinite2
230 ; o<-irr = OrdIrr
219 ; Oprev-p = Oprev-p 231 ; Oprev-p = Oprev-p
220 } ; 232 } ;
221 isNext = record { 233 isNext = record {
222 x<nx = x<nx 234 x<nx = x<nx
223 ; osuc<nx = λ {x} {y} → osuc<nx {x} {y} 235 ; osuc<nx = λ {x} {y} → osuc<nx {x} {y}