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

comparison HOD.agda @ 145:f0fa9a755513

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
all done but ...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 08 Jul 2019 18:19:56 +0900
parents 3ba37037faf4
children 2eafa89733ed
comparison
equal deleted inserted replaced
144:3ba37037faf4 145:f0fa9a755513
298 Replace : OD {suc n} → (OD {suc n} → OD {suc n} ) → OD {suc n} 298 Replace : OD {suc n} → (OD {suc n} → OD {suc n} ) → OD {suc n}
299 Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x } 299 Replace X ψ = record { def = λ x → (x o< sup-o ( λ x → od→ord (ψ (ord→od x )))) ∧ def (in-codomain X ψ) x }
300 _,_ : OD {suc n} → OD {suc n} → OD {suc n} 300 _,_ : OD {suc n} → OD {suc n} → OD {suc n}
301 x , y = Ord (omax (od→ord x) (od→ord y)) 301 x , y = Ord (omax (od→ord x) (od→ord y))
302 _∩_ : ( A B : ZFSet ) → ZFSet 302 _∩_ : ( A B : ZFSet ) → ZFSet
303 A ∩ B = record { def = λ x → def A x ∧ def B x } -- Select (A , B) ( λ x → ( A ∋ x ) ∧ (B ∋ x) ) 303 A ∩ B = record { def = λ x → def A x ∧ def B x }
304 Union : OD {suc n} → OD {suc n} 304 Union : OD {suc n} → OD {suc n}
305 Union U = Replace ( record { def = λ x → osuc x o< od→ord U } ) ( λ x → U ∩ x ) 305 Union U = record { def = λ y → def U (osuc y) }
306 -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x → X ∋ x )
307 _∈_ : ( A B : ZFSet ) → Set (suc n) 306 _∈_ : ( A B : ZFSet ) → Set (suc n)
308 A ∈ B = B ∋ A 307 A ∈ B = B ∋ A
309 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set (suc n) 308 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set (suc n)
310 _⊆_ A B {x} = A ∋ x → B ∋ x 309 _⊆_ A B {x} = A ∋ x → B ∋ x
311 Power : OD {suc n} → OD {suc n} 310 Power : OD {suc n} → OD {suc n}
312 Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x ) 311 Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
313 -- _∪_ : ( A B : ZFSet ) → ZFSet
314 -- A ∪ B = Select (A , B) ( λ x → (A ∋ x) ∨ ( B ∋ x ) )
315 ｛_｝ : ZFSet → ZFSet 312 ｛_｝ : ZFSet → ZFSet
316 ｛ x ｝ = ( x , x ) 313 ｛ x ｝ = ( x , x )
317 314
318 infixr 200 _∈_ 315 infixr 200 _∈_
319 -- infixr 230 _∩_ _∪_ 316 -- infixr 230 _∩_ _∪_
344 341
345 empty : (x : OD {suc n} ) → ¬ (od∅ ∋ x) 342 empty : (x : OD {suc n} ) → ¬ (od∅ ∋ x)
346 empty x (case1 ()) 343 empty x (case1 ())
347 empty x (case2 ()) 344 empty x (case2 ())
348 345
349 union-lemma : {n : Level } {X z u : OD {suc n} } → (X ∋ u) → (u ∋ z) → osuc ( od→ord z ) o< od→ord u → X ∋ Ord (osuc ( od→ord z ) ) 346 union-d : (X : OD {suc n}) → OD {suc n}
350 union-lemma = {!!} 347 union-d X = record { def = λ y → def X (osuc y) }
351 union-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n} 348 union-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n}
352 union-u {X} {z} U>z = Ord ( osuc ( od→ord z ) ) 349 union-u {X} {z} U>z = Ord ( osuc ( od→ord z ) )
353 union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z 350 union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
354 union→ X z u xx with trio< ( od→ord u ) ( osuc ( od→ord z )) 351 union→ X z u xx with trio< ( od→ord u ) ( osuc ( od→ord z ))
355 union→ X z u xx | tri< a ¬b ¬c with osuc-< a (c<→o< (proj2 xx)) 352 union→ X z u xx | tri< a ¬b ¬c with osuc-< a (c<→o< (proj2 xx))
356 union→ X z u xx | tri< a ¬b ¬c | () 353 union→ X z u xx | tri< a ¬b ¬c | ()
357 union→ X z u xx | tri≈ ¬a b ¬c = {!!} 354 union→ X z u xx | tri≈ ¬a b ¬c = def-subst {suc n} {_} {_} {X} {osuc (od→ord z)} (proj1 xx) refl b
358 union→ X z u xx | tri> ¬a ¬b c = {!!} --- osuc ( od→ord z )) o< od→ord u o< od→ord X 355 union→ X z u xx | tri> ¬a ¬b c = def-subst lemma1 (sym lemma0) diso where
359 -- def-subst {suc n} {_} {_} {X} {osuc (od→ord z)} (union-lemma {n} {X} {z} {u} (proj1 xx) (proj2 xx) c ) refl (sym ord-Ord) 356 lemma0 : X ≡ Ord (od→ord X)
357 lemma0 = sym Ord-ord-≡
358 lemma : osuc (od→ord z) o< od→ord X
359 lemma = ordtrans c ( c<→o< ( proj1 xx ) )
360 lemma1 : Ord ( od→ord X) ∋ ord→od (osuc (od→ord z) )
361 lemma1 = o<-subst lemma (sym diso) refl
360 union← : (X z : OD) (X∋z : Union X ∋ z) → (X ∋ union-u {X} {z} X∋z ) ∧ (union-u {X} {z} X∋z ∋ z ) 362 union← : (X z : OD) (X∋z : Union X ∋ z) → (X ∋ union-u {X} {z} X∋z ) ∧ (union-u {X} {z} X∋z ∋ z )
361 union← X z X∋z = record { proj1 = lemma ; proj2 = <-osuc } where 363 union← X z UX∋z = record { proj1 = lemma ; proj2 = <-osuc } where
362 lemma : X ∋ union-u {X} {z} X∋z 364 lemma : X ∋ union-u {X} {z} UX∋z
363 lemma = def-subst {suc n} {_} {_} {X} {od→ord (Ord (osuc ( od→ord z )))} {!!} refl ord-Ord 365 lemma = def-subst {suc n} {_} {_} {X} {od→ord (Ord (osuc ( od→ord z )))} UX∋z refl ord-Ord
364 366
365 ψiso : {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y → ψ y 367 ψiso : {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y → ψ y
366 ψiso {ψ} t refl = t 368 ψiso {ψ} t refl = t
367 selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y) 369 selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
368 selection {ψ} {X} {y} = record { 370 selection {ψ} {X} {y} = record {
506 uxxx-ord : {x : OD {suc n}} → {y : Ordinal {suc n}} → def (Union (x , (x , x))) y ⇔ ( y o< osuc (od→ord x) ) 508 uxxx-ord : {x : OD {suc n}} → {y : Ordinal {suc n}} → def (Union (x , (x , x))) y ⇔ ( y o< osuc (od→ord x) )
507 uxxx-ord {x} {y} = subst (λ k → k ⇔ ( y o< osuc (od→ord x) )) (sym lemma) ( osuc2 y (od→ord x)) where 509 uxxx-ord {x} {y} = subst (λ k → k ⇔ ( y o< osuc (od→ord x) )) (sym lemma) ( osuc2 y (od→ord x)) where
508 lemma : {y : Ordinal {suc n}} → def (Union (x , (x , x))) y ≡ osuc y o< osuc (osuc (od→ord x)) 510 lemma : {y : Ordinal {suc n}} → def (Union (x , (x , x))) y ≡ osuc y o< osuc (osuc (od→ord x))
509 lemma {y} = let open ≡-Reasoning in begin 511 lemma {y} = let open ≡-Reasoning in begin
510 def (Union (x , (x , x))) y 512 def (Union (x , (x , x))) y
511 ≡⟨ {!!} ⟩ 513 ≡⟨⟩
512 def ( Ord ( omax (od→ord x) (od→ord (Ord (omax (od→ord x) (od→ord x) )) ))) ( osuc y ) 514 def ( Ord ( omax (od→ord x) (od→ord (Ord (omax (od→ord x) (od→ord x) )) ))) ( osuc y )
513 ≡⟨⟩ 515 ≡⟨⟩
514 osuc y o< omax (od→ord x) (od→ord (Ord (omax (od→ord x) (od→ord x) )) ) 516 osuc y o< omax (od→ord x) (od→ord (Ord (omax (od→ord x) (od→ord x) )) )
515 ≡⟨ cong (λ k → osuc y o< omax (od→ord x) k ) (sym ord-Ord) ⟩ 517 ≡⟨ cong (λ k → osuc y o< omax (od→ord x) k ) (sym ord-Ord) ⟩
516 osuc y o< omax (od→ord x) (omax (od→ord x) (od→ord x) ) 518 osuc y o< omax (od→ord x) (omax (od→ord x) (od→ord x) )