Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff OD.agda @ 387:8b0715e28b33
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 25 Jul 2020 09:09:00 +0900 |
parents | d2cb5278e46d |
children | 19687f3304c9 |
line wrap: on
line diff
--- a/OD.agda Thu Jul 23 17:50:28 2020 +0900 +++ b/OD.agda Sat Jul 25 09:09:00 2020 +0900 @@ -76,9 +76,6 @@ -- -- ==→o≡ is necessary to prove axiom of extensionality. -data One {n : Level } : Set n where - OneObj : One - -- Ordinals in OD , the maximum Ords : OD Ords = record { def = λ x → One } @@ -274,6 +271,12 @@ open _⊆_ infixr 220 _⊆_ +trans-⊆ : { A B C : HOD} → A ⊆ B → B ⊆ C → A ⊆ C +trans-⊆ A⊆B B⊆C = record { incl = λ x → incl B⊆C (incl A⊆B x) } + +refl-⊆ : {A : HOD} → A ⊆ A +refl-⊆ {A} = record { incl = λ x → x } + od⊆→o≤ : {x y : HOD } → x ⊆ y → od→ord x o< osuc (od→ord y) od⊆→o≤ {x} {y} lt = ⊆→o≤ {x} {y} (λ {z} x>z → subst (λ k → def (od y) k ) diso (incl lt (subst (λ k → def (od x) k ) (sym diso) x>z ))) @@ -317,14 +320,14 @@ ε-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 +-- ε-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) }