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

comparison OD.agda @ 247:d09437fcfc7c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix pair
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 26 Aug 2019 12:27:20 +0900
parents 846e0926bb89
children 2ea2a19f9cd6
comparison
equal deleted inserted replaced
246:3506f53c7d83 247:d09437fcfc7c
267 Select : (X : OD ) → ((x : OD ) → Set n ) → OD 267 Select : (X : OD ) → ((x : OD ) → Set n ) → OD
268 Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) } 268 Select X ψ = record { def = λ x → ( def X x ∧ ψ ( ord→od x )) }
269 Replace : OD → (OD → OD ) → OD 269 Replace : OD → (OD → OD ) → OD
270 Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x } 270 Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x }
271 _,_ : OD → OD → OD 271 _,_ : OD → OD → OD
272 x , y = Ord (omax (od→ord x) (od→ord y)) 272 x , y = record { def = λ t → (t ≡ od→ord x ) ∨ ( t ≡ od→ord y ) } -- Ord (omax (od→ord x) (od→ord y))
273 _∩_ : ( A B : ZFSet ) → ZFSet 273 _∩_ : ( A B : ZFSet ) → ZFSet
274 A ∩ B = record { def = λ x → def A x ∧ def B x } 274 A ∩ B = record { def = λ x → def A x ∧ def B x }
275 Union : OD → OD 275 Union : OD → OD
276 Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) } 276 Union U = record { def = λ x → ¬ (∀ (u : Ordinal ) → ¬ ((def U u) ∧ (def (ord→od u) x))) }
277 _∈_ : ( A B : ZFSet ) → Set n 277 _∈_ : ( A B : ZFSet ) → Set n
292 infixr 200 _∈_ 292 infixr 200 _∈_
293 -- infixr 230 _∩_ _∪_ 293 -- infixr 230 _∩_ _∪_
294 isZF : IsZF (OD ) _∋_ _==_ od∅ _,_ Union Power Select Replace infinite 294 isZF : IsZF (OD ) _∋_ _==_ od∅ _,_ Union Power Select Replace infinite
295 isZF = record { 295 isZF = record {
296 isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans } 296 isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
297 ; pair = pair 297 ; pair→ = pair→
298 ; pair← = pair←
298 ; union→ = union→ 299 ; union→ = union→
299 ; union← = union← 300 ; union← = union←
300 ; empty = empty 301 ; empty = empty
301 ; power→ = power→ 302 ; power→ = power→
302 ; power← = power← 303 ; power← = power←
309 ; replacement→ = replacement→ 310 ; replacement→ = replacement→
310 ; choice-func = choice-func 311 ; choice-func = choice-func
311 ; choice = choice 312 ; choice = choice
312 } where 313 } where
313 314
314 pair : (A B : OD ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B) 315 pair→ : ( x y t : ZFSet ) → (x , y) ∋ t → ( t == x ) ∨ ( t == y )
315 proj1 (pair A B ) = omax-x (od→ord A) (od→ord B) 316 pair→ x y t (case1 t≡x ) = case1 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡x ))
316 proj2 (pair A B ) = omax-y (od→ord A) (od→ord B) 317 pair→ x y t (case2 t≡y ) = case2 (subst₂ (λ j k → j == k ) oiso oiso (o≡→== t≡y ))
318
319 pair← : ( x y t : ZFSet ) → ( t == x ) ∨ ( t == y ) → (x , y) ∋ t
320 pair← x y t (case1 t==x) = case1 (cong (λ k → od→ord k ) (==→o≡ t==x))
321 pair← x y t (case2 t==y) = case2 (cong (λ k → od→ord k ) (==→o≡ t==y))
322
323 -- pair0 : (A B : OD ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B)
324 -- proj1 (pair A B ) = omax-x (od→ord A) (od→ord B)
325 -- proj2 (pair A B ) = omax-y (od→ord A) (od→ord B)
317 326
318 empty : (x : OD ) → ¬ (od∅ ∋ x) 327 empty : (x : OD ) → ¬ (od∅ ∋ x)
319 empty x = ¬x<0 328 empty x = ¬x<0
320 329
321 o<→c< : {x y : Ordinal } {z : OD }→ x o< y → _⊆_ (Ord x) (Ord y) {z} 330 o<→c< : {x y : Ordinal } {z : OD }→ x o< y → _⊆_ (Ord x) (Ord y) {z}