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

comparison OD.agda @ 387:8b0715e28b33

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 09:09:00 +0900
parents d2cb5278e46d
children 19687f3304c9
comparison
equal deleted inserted replaced
386:24a66a246316 387:8b0715e28b33
73 -- 73 --
74 -- In classical Set Theory, sup is defined by Uion, since we are working on constructive logic, 74 -- In classical Set Theory, sup is defined by Uion, since we are working on constructive logic,
75 -- we need explict assumption on sup. 75 -- we need explict assumption on sup.
76 -- 76 --
77 -- ==→o≡ is necessary to prove axiom of extensionality. 77 -- ==→o≡ is necessary to prove axiom of extensionality.
78
79 data One {n : Level } : Set n where
80 OneObj : One
81 78
82 -- Ordinals in OD , the maximum 79 -- Ordinals in OD , the maximum
83 Ords : OD 80 Ords : OD
84 Ords = record { def = λ x → One } 81 Ords = record { def = λ x → One }
85 82
271 field 268 field
272 incl : { x : HOD } → A ∋ x → B ∋ x 269 incl : { x : HOD } → A ∋ x → B ∋ x
273 270
274 open _⊆_ 271 open _⊆_
275 infixr 220 _⊆_ 272 infixr 220 _⊆_
273
274 trans-⊆ : { A B C : HOD} → A ⊆ B → B ⊆ C → A ⊆ C
275 trans-⊆ A⊆B B⊆C = record { incl = λ x → incl B⊆C (incl A⊆B x) }
276
277 refl-⊆ : {A : HOD} → A ⊆ A
278 refl-⊆ {A} = record { incl = λ x → x }
276 279
277 od⊆→o≤ : {x y : HOD } → x ⊆ y → od→ord x o< osuc (od→ord y) 280 od⊆→o≤ : {x y : HOD } → x ⊆ y → od→ord x o< osuc (od→ord y)
278 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 ))) 281 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 )))
279 282
280 -- if we have od→ord (x , x) ≡ osuc (od→ord x), ⊆→o≤ → c<→o< 283 -- if we have od→ord (x , x) ≡ osuc (od→ord x), ⊆→o≤ → c<→o<
315 induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) 318 induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso )))
316 ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy) 319 ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
317 ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy 320 ε-induction-ord ox {oy} lt = TransFinite {λ oy → ψ (ord→od oy)} induction oy
318 321
319 -- level trick (what'a shame) 322 -- level trick (what'a shame)
320 ε-induction1 : { ψ : HOD → Set (suc n)} 323 -- ε-induction1 : { ψ : HOD → Set (suc n)}
321 → ( {x : HOD } → ({ y : HOD } → x ∋ y → ψ y ) → ψ x ) 324 -- → ( {x : HOD } → ({ y : HOD } → x ∋ y → ψ y ) → ψ x )
322 → (x : HOD ) → ψ x 325 -- → (x : HOD ) → ψ x
323 ε-induction1 {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc ) where 326 -- ε-induction1 {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc ) where
324 induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox) 327 -- induction : (ox : Ordinal) → ((oy : Ordinal) → oy o< ox → ψ (ord→od oy)) → ψ (ord→od ox)
325 induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso ))) 328 -- induction ox prev = ind ( λ {y} lt → subst (λ k → ψ k ) oiso (prev (od→ord y) (o<-subst (c<→o< lt) refl diso )))
326 ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy) 329 -- ε-induction-ord : (ox : Ordinal) { oy : Ordinal } → oy o< ox → ψ (ord→od oy)
327 ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (ord→od oy)} induction oy 330 -- ε-induction-ord ox {oy} lt = TransFinite1 {λ oy → ψ (ord→od oy)} induction oy
328 331
329 Select : (X : HOD ) → ((x : HOD ) → Set n ) → HOD 332 Select : (X : HOD ) → ((x : HOD ) → Set n ) → HOD
330 Select X ψ = record { od = record { def = λ x → ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) } 333 Select X ψ = record { od = record { def = λ x → ( odef X x ∧ ψ ( ord→od x )) } ; odmax = odmax X ; <odmax = λ y → <odmax X (proj1 y) }
331 334
332 Replace : HOD → (HOD → HOD) → HOD 335 Replace : HOD → (HOD → HOD) → HOD