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

comparison src/OD.agda @ 448:81691a6b352b

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 Sun, 13 Mar 2022 19:03:33 +0900
parents a5f8084b8368
children b27d92694ed5
comparison
equal deleted inserted replaced
447:364d738f871d 448:81691a6b352b
203 ≡o∅→=od∅ {x} eq = record { eq→ = λ {y} lt → ⊥-elim ( ¬x<0 {y} (subst₂ (λ j k → j o< k ) &iso eq ( c<→o< {* y} {x} (d→∋ x lt)))) 203 ≡o∅→=od∅ {x} eq = record { eq→ = λ {y} lt → ⊥-elim ( ¬x<0 {y} (subst₂ (λ j k → j o< k ) &iso eq ( c<→o< {* y} {x} (d→∋ x lt))))
204 ; eq← = λ {y} lt → ⊥-elim ( ¬x<0 lt )} 204 ; eq← = λ {y} lt → ⊥-elim ( ¬x<0 lt )}
205 205
206 =od∅→≡o∅ : {x : HOD} → od x == od od∅ → & x ≡ o∅ 206 =od∅→≡o∅ : {x : HOD} → od x == od od∅ → & x ≡ o∅
207 =od∅→≡o∅ {x} eq = trans (cong (λ k → & k ) (==→o≡ {x} {od∅} eq)) ord-od∅ 207 =od∅→≡o∅ {x} eq = trans (cong (λ k → & k ) (==→o≡ {x} {od∅} eq)) ord-od∅
208
209 ≡od∅→=od∅ : {x : HOD} → x ≡ od∅ → od x == od od∅
210 ≡od∅→=od∅ {x} eq = ≡o∅→=od∅ (subst (λ k → & x ≡ k ) ord-od∅ ( cong & eq ) )
208 211
209 ∅0 : record { def = λ x → Lift n ⊥ } == od od∅ 212 ∅0 : record { def = λ x → Lift n ⊥ } == od od∅
210 eq→ ∅0 {w} (lift ()) 213 eq→ ∅0 {w} (lift ())
211 eq← ∅0 {w} lt = lift (¬x<0 lt) 214 eq← ∅0 {w} lt = lift (¬x<0 lt)
212 215