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

comparison ordinal-definable.agda @ 33:2b853472cb24

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 Tue, 21 May 2019 18:17:24 +0900
parents 3b0fdb95618e
children c9ad0d97ce41
comparison
equal deleted inserted replaced
30:3b0fdb95618e 33:2b853472cb24
94 c3 lx (Φ .lx) d not with not ( record { lv = lx ; ord = Φ lx } ) 94 c3 lx (Φ .lx) d not with not ( record { lv = lx ; ord = Φ lx } )
95 ... | t with t (case2 Φ< ) 95 ... | t with t (case2 Φ< )
96 c3 lx (Φ .lx) d not | t | () 96 c3 lx (Φ .lx) d not | t | ()
97 c3 lx (OSuc .lx x₁) d not with not ( record { lv = lx ; ord = OSuc lx x₁ } ) 97 c3 lx (OSuc .lx x₁) d not with not ( record { lv = lx ; ord = OSuc lx x₁ } )
98 ... | t with t (case2 (s< {!!} ) ) 98 ... | t with t (case2 (s< {!!} ) )
99 -- x d< OSuc lx x is bad on ℵ case
99 c3 lx (OSuc .lx x₁) d not | t | () 100 c3 lx (OSuc .lx x₁) d not | t | ()
100 c3 .(Suc lv) (ℵ lv) not = {!!} 101 c3 .(Suc lv) (ℵ lv) not = {!!}
101 102
102 ∅2 : {n : Level} → od→ord ( od∅ {n} ) ≡ o∅ {n} 103 ∅2 : {n : Level} → od→ord ( od∅ {n} ) ≡ o∅ {n}
103 ∅2 {n} = {!!} 104 ∅2 {n} = {!!}