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

comparison src/OD.agda @ 1180:8e04e3cad0b5

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 Thu, 23 Feb 2023 18:44:47 +0900
parents 7d2bae0ff36b
children ffe5bc98f9d1
comparison
equal deleted inserted replaced
1179:f4cd937759fc 1180:8e04e3cad0b5
397 power→ : ( A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → A ∋ x 397 power→ : ( A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → A ∋ x
398 power→ A t P∋t {x} t∋x = P∋t (& x) (subst (λ k → odef k (& x) ) (sym *iso) t∋x ) 398 power→ A t P∋t {x} t∋x = P∋t (& x) (subst (λ k → odef k (& x) ) (sym *iso) t∋x )
399 399
400 power← : (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t 400 power← : (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t
401 power← A t t⊆A z xz = subst (λ k → odef A k ) &iso ( t⊆A (subst₂ (λ j k → odef j k) *iso (sym &iso) xz )) 401 power← A t t⊆A z xz = subst (λ k → odef A k ) &iso ( t⊆A (subst₂ (λ j k → odef j k) *iso (sym &iso) xz ))
402
403 Intersection : (X : HOD ) → HOD -- ∩ X
404 Intersection X = record { od = record { def = λ x → (x o< & X ) ∧ ( {y : Ordinal} → odef X y → odef (* y) x )} ; odmax = & X ; <odmax = λ lt → proj1 lt }
405
402 406
403 -- ｛_｝ : ZFSet → ZFSet 407 -- ｛_｝ : ZFSet → ZFSet
404 -- ｛ x ｝ = ( x , x ) -- better to use (x , x) directly 408 -- ｛ x ｝ = ( x , x ) -- better to use (x , x) directly
405 409
406 410