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

comparison src/OD.agda @ 556:ba889c711524

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, 29 Apr 2022 17:53:31 +0900
parents b27d92694ed5
children d6ad1af5299e 3938bed729a5
comparison
equal deleted inserted replaced
555:726b6dac5eaa 556:ba889c711524
183 lemma : ( ox oy : Ordinal ) → ox ≡ oy → od (* ox) == od (* oy) 183 lemma : ( ox oy : Ordinal ) → ox ≡ oy → od (* ox) == od (* oy)
184 lemma ox ox refl = ==-refl 184 lemma ox ox refl = ==-refl
185 185
186 o≡→== : { x y : Ordinal } → x ≡ y → od (* x) == od (* y) 186 o≡→== : { x y : Ordinal } → x ≡ y → od (* x) == od (* y)
187 o≡→== {x} {.x} refl = ==-refl 187 o≡→== {x} {.x} refl = ==-refl
188
189 *≡*→≡ : { x y : Ordinal } → * x ≡ * y → x ≡ y
190 *≡*→≡ eq = subst₂ (λ j k → j ≡ k ) &iso &iso ( cong (&) eq )
191
192 &≡&→≡ : { x y : HOD } → & x ≡ & y → x ≡ y
193 &≡&→≡ eq = subst₂ (λ j k → j ≡ k ) *iso *iso ( cong (*) eq )
188 194
189 o∅≡od∅ : * (o∅ ) ≡ od∅ 195 o∅≡od∅ : * (o∅ ) ≡ od∅
190 o∅≡od∅ = ==→o≡ lemma where 196 o∅≡od∅ = ==→o≡ lemma where
191 lemma0 : {x : Ordinal} → odef (* o∅) x → odef od∅ x 197 lemma0 : {x : Ordinal} → odef (* o∅) x → odef od∅ x
192 lemma0 {x} lt with c<→o< {* x} {* o∅} (subst (λ k → odef (* o∅) k ) (sym &iso) lt) 198 lemma0 {x} lt with c<→o< {* x} {* o∅} (subst (λ k → odef (* o∅) k ) (sym &iso) lt)