Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison OD.agda @ 247:d09437fcfc7c
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} |