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

comparison OD.agda @ 388:19687f3304c9

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 Sat, 25 Jul 2020 12:54:28 +0900
parents 8b0715e28b33
children 43b0a6ca7602
comparison
equal deleted inserted replaced
387:8b0715e28b33 388:19687f3304c9
164 otrans : {a x y : Ordinal } → odef (Ord a) x → odef (Ord x) y → odef (Ord a) y 164 otrans : {a x y : Ordinal } → odef (Ord a) x → odef (Ord x) y → odef (Ord a) y
165 otrans x<a y<x = ordtrans y<x x<a 165 otrans x<a y<x = ordtrans y<x x<a
166 166
167 odef→o< : {X : HOD } → {x : Ordinal } → odef X x → x o< od→ord X 167 odef→o< : {X : HOD } → {x : Ordinal } → odef X x → x o< od→ord X
168 odef→o< {X} {x} lt = o<-subst {_} {_} {x} {od→ord X} ( c<→o< ( odef-subst {X} {x} lt (sym oiso) (sym diso) )) diso diso 168 odef→o< {X} {x} lt = o<-subst {_} {_} {x} {od→ord X} ( c<→o< ( odef-subst {X} {x} lt (sym oiso) (sym diso) )) diso diso
169
170 odefo→o< : {X y : Ordinal } → odef (ord→od X) y → y o< X
171 odefo→o< {X} {y} lt = subst₂ (λ j k → j o< k ) diso diso ( c<→o< (subst (λ k → odef (ord→od X) k ) (sym diso ) lt ))
169 172
170 -- avoiding lv != Zero error 173 -- avoiding lv != Zero error
171 orefl : { x : HOD } → { y : Ordinal } → od→ord x ≡ y → od→ord x ≡ y 174 orefl : { x : HOD } → { y : Ordinal } → od→ord x ≡ y → od→ord x ≡ y
172 orefl refl = refl 175 orefl refl = refl
173 176
317 induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox) 320 induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox)
318 induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) 321 induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso )))
319 ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy) 322 ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
320 ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy 323 ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy
321 324
322 -- level trick (what'a shame) 325 -- level trick (what'a shame) for LEM / minimal
323 -- ε-induction1 : { ψ : HOD → Set (suc n)} 326 ε-induction1 : { ψ : HOD → Set (suc n)}
324 -- → ( {x : HOD } → ({ y : HOD } → x ∋ y → ψ y ) → ψ x ) 327 → ( {x : HOD } → ({ y : HOD } → x ∋ y → ψ y ) → ψ x )
325 -- → (x : HOD ) → ψ x 328 → (x : HOD ) → ψ x
326 -- ε-induction1 {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc ) where 329 ε-induction1 {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc ) where
327 -- induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox) 330 induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox)
328 -- induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) 331 induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso )))
329 -- ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy) 332 ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
330 -- ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (ord→od oy)} induction oy 333 ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (ord→od oy)} induction oy
331 334
332 Select : (X : HOD ) → ((x : HOD ) → Set n ) → HOD 335 Select : (X : HOD ) → ((x : HOD ) → Set n ) → HOD
333 Select X ψ = record { od = record { def = λ x → ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) } 336 Select X ψ = record { od = record { def = λ x → ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) }
334 337
335 Replace : HOD → (HOD → HOD) → HOD 338 Replace : HOD → (HOD → HOD) → HOD