Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff OD.agda @ 388:19687f3304c9
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 25 Jul 2020 12:54:28 +0900 |
parents | 8b0715e28b33 |
children | 43b0a6ca7602 |
line wrap: on
line diff
--- a/OD.agda Sat Jul 25 09:09:00 2020 +0900 +++ b/OD.agda Sat Jul 25 12:54:28 2020 +0900 @@ -167,6 +167,9 @@ odef→o< : {X : HOD } → {x : Ordinal } → odef X x → x o< od→ord X odef→o< {X} {x} lt = o<-subst {_} {_} {x} {od→ord X} ( c<→o< ( odef-subst {X} {x} lt (sym oiso) (sym diso) )) diso diso +odefo→o< : {X y : Ordinal } → odef (ord→od X) y → y o< X +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 )) + -- avoiding lv != Zero error orefl : { x : HOD } → { y : Ordinal } → od→ord x ≡ y → od→ord x ≡ y orefl refl = refl @@ -319,15 +322,15 @@ ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy) ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy --- level trick (what'a shame) --- ε-induction1 : { ψ : HOD → Set (suc n)} --- → ( {x : HOD } → ({ y : HOD } → x ∋ y → ψ y ) → ψ x ) --- → (x : HOD ) → ψ x --- ε-induction1 {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc ) where --- induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox) --- induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) --- ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy) --- ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (ord→od oy)} induction oy +-- level trick (what'a shame) for LEM / minimal +ε-induction1 : { ψ : HOD → Set (suc n)} + → ( {x : HOD } → ({ y : HOD } → x ∋ y → ψ y ) → ψ x ) + → (x : HOD ) → ψ x +ε-induction1 {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc ) where + induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox) + induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) + ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy) + ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (ord→od oy)} induction oy Select : (X : HOD ) → ((x : HOD ) → Set n ) → HOD Select X ψ = record { od = record { def = λ x → ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) }