Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff HOD.agda @ 155:53371f91ce63
union continue
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 11 Jul 2019 07:32:28 +0900 |
parents | e51c23eb3803 |
children | 3e7475fb28db |
line wrap: on
line diff
--- a/HOD.agda Wed Jul 10 11:50:26 2019 +0900 +++ b/HOD.agda Thu Jul 11 07:32:28 2019 +0900 @@ -314,32 +314,40 @@ ord-⊆ : ( t x : OD {suc n} ) → _⊆_ t (Ord (od→ord t )) {x} ord-⊆ t x lt = c<→o< lt o<→c< : {x y : Ordinal {suc n}} {z : OD {suc n}}→ x o< y → _⊆_ (Ord x) (Ord y) {z} - o<→c< lt lt1 = ordtrans lt1 lt - -- a ⊆ b → od→ord a o≤ od→ord b ? + o<→c< lt lt1 = ordtrans lt1 lt + + ⊆→o< : {x y : Ordinal {suc n}} → (∀ (z : OD) → _⊆_ (Ord x) (Ord y) {z} ) → x o< osuc y + ⊆→o< {x} {y} lt with trio< x y + ⊆→o< {x} {y} lt | tri< a ¬b ¬c = ordtrans a <-osuc + ⊆→o< {x} {y} lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc + ⊆→o< {x} {y} lt | tri> ¬a ¬b c with lt (ord→od y) (o<-subst c (sym diso) refl ) + ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl )) Union-o : (X : Ordinal {suc n}) → OD {suc n} Union-o X = record { def = λ y → osuc y o< X } - - 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-ou : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → OD {suc n} + union-ou {X} {z} U>z = Ord ( osuc ( od→ord z ) ) ord-union→ : (x : Ordinal) (z u : OD) → (Ord x ∋ u) ∧ (u ∋ z) → Union-o x ∋ z ord-union→ x z u plt with trio< ( od→ord u ) ( osuc ( od→ord z )) ord-union→ x z u plt | tri< a ¬b ¬c with osuc-< a (c<→o< (proj2 plt)) ord-union→ x z u plt | tri< a ¬b ¬c | () ord-union→ x z u plt | tri≈ ¬a b ¬c = subst ( λ k → k o< x ) b (proj1 plt) ord-union→ x z u plt | tri> ¬a ¬b c = otrans (proj1 plt) c - ord-union← : (x : Ordinal) (z : OD) (X∋z : Union-o x ∋ z) - → (Ord x ∋ union-u {Ord x} {z} X∋z ) ∧ (union-u {Ord x} {z} X∋z ∋ z ) - ord-union← x z X∋z = record { proj1 = lemma ; proj2 = {!!} } where - lemma : Ord x ∋ union-u {Ord x} {z} X∋z - lemma = def-subst {suc n} {_} {_} {Ord x} {_} X∋z refl (sym diso) + -- ord-union← : (x : Ordinal) (z : OD) (X∋z : Union-o x ∋ z) + -- → (Ord x ∋ union-ou {Ord x} {z} X∋z ) ∧ (union-ou {Ord x} {z} X∋z ∋ z ) + -- ord-union← x z X∋z = record { proj1 = lemma ; proj2 = <-osuc } where + -- lemma : Ord x ∋ union-ou {Ord x} {z} X∋z + -- lemma = {!!} -- def-subst {suc n} {_} {_} {Ord x} {_} X∋z refl (sym diso) + 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 with trio< ( od→ord u ) ( osuc ( od→ord z )) union→ X z u xx | tri< a ¬b ¬c with osuc-< a (c<→o< (proj2 xx)) union→ X z u xx | tri< a ¬b ¬c | () union→ X z u xx | tri≈ ¬a b ¬c = def-subst {suc n} {_} {_} {X} {osuc (od→ord z)} (proj1 xx) refl b union→ X z u xx | tri> ¬a ¬b c = {!!} + 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