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

comparison src/OD.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 d6ad1af5299e
children 10195ebfbe2b
comparison
equal deleted inserted replaced
611:d6ad1af5299e 612:099ca2fea51c
212 =od∅→≡o∅ : {x : HOD} → od x == od od∅ → & x ≡ o∅ 212 =od∅→≡o∅ : {x : HOD} → od x == od od∅ → & x ≡ o∅
213 =od∅→≡o∅ {x} eq = trans (cong (λ k → & k ) (==→o≡ {x} {od∅} eq)) ord-od∅ 213 =od∅→≡o∅ {x} eq = trans (cong (λ k → & k ) (==→o≡ {x} {od∅} eq)) ord-od∅
214 214
215 ≡od∅→=od∅ : {x : HOD} → x ≡ od∅ → od x == od od∅ 215 ≡od∅→=od∅ : {x : HOD} → x ≡ od∅ → od x == od od∅
216 ≡od∅→=od∅ {x} eq = ≡o∅→=od∅ (subst (λ k → & x ≡ k ) ord-od∅ ( cong & eq ) ) 216 ≡od∅→=od∅ {x} eq = ≡o∅→=od∅ (subst (λ k → & x ≡ k ) ord-od∅ ( cong & eq ) )
217
218 -- o<-irr : { x y : Ordinal } → { lt lt1 : x o< y } → lt ≡ lt1
219 217
220 ∅0 : record { def = λ x → Lift n ⊥ } == od od∅ 218 ∅0 : record { def = λ x → Lift n ⊥ } == od od∅
221 eq→ ∅0 {w} (lift ()) 219 eq→ ∅0 {w} (lift ())
222 eq← ∅0 {w} lt = lift (¬x<0 lt) 220 eq← ∅0 {w} lt = lift (¬x<0 lt)
223 221