Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff HOD.agda @ 157:afc030b7c8d0
explict logical definition of Union failed
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 14 Jul 2019 08:04:16 +0900 |
| parents | 3e7475fb28db |
| children | b97b4ee06f01 |
line wrap: on
line diff
--- a/HOD.agda Thu Jul 11 20:00:30 2019 +0900 +++ b/HOD.agda Sun Jul 14 08:04:16 2019 +0900 @@ -339,8 +339,13 @@ union-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n} union-u {X} {z} U>z = ord→od ( osuc ( od→ord z ) ) union→ : (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z - union→ X z u xx = {!!} + union→ X z u xx not = ⊥-elim ( not (od→ord u) ( record { proj1 = proj1 xx + ; proj2 = subst ( λ k → def k (od→ord z)) (sym oiso) (proj2 xx) } )) + union-u' : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n} + union-u' {X} {z} U>z = record { def = λ x → ¬ ( (u : Ordinal ) → ¬ (def X u) ∧ (ord→od u ∋ z ) ∧ ( u ≡ x ) ) } + union←' : (X z : OD) (X∋z : Union X ∋ z) → ¬ ( (u : OD ) → ¬ ((X ∋ u) ∧ (u ∋ z ))) + union←' X z UX∋z = TransFiniteExists {suc (suc n)} {λ x → {!!} } {!!} {!!} where union← : (X z : OD) (X∋z : Union X ∋ z) → (X ∋ union-u {X} {z} X∋z ) ∧ (union-u {X} {z} X∋z ∋ z ) union← X z UX∋z = record { proj1 = lemma ; proj2 = lemma2 } where lemma : X ∋ union-u {X} {z} UX∋z