Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison cardinal.agda @ 247:d09437fcfc7c
fix pair
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 26 Aug 2019 12:27:20 +0900 |
parents | 3506f53c7d83 |
children | 9fd85b954477 |
comparison
equal
deleted
inserted
replaced
246:3506f53c7d83 | 247:d09437fcfc7c |
---|---|
59 eq-pair refl refl = HE.refl | 59 eq-pair refl refl = HE.refl |
60 | 60 |
61 eq-prod : { x x' y y' : OD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' > | 61 eq-prod : { x x' y y' : OD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' > |
62 eq-prod refl refl = refl | 62 eq-prod refl refl = refl |
63 | 63 |
64 -- prod-eq : { x x' y y' : OD } → < x , y > ≡ < x' , y' > → (x ≡ x' ) ∧ ( y ≡ y' ) | |
65 -- prod-eq {x} {x'} {y} {y'} eq = {!!} where | |
66 -- lemma : < x , y > ≡ < x , y' > → y ≡ y' | |
67 -- lemma eq1 with trio< (od→ord x) (od→ord y) | |
68 -- lemma eq1 | tri< a ¬b ¬c = {!!} | |
69 -- lemma eq1 | tri≈ ¬a b ¬c = {!!} | |
70 -- lemma eq1 | tri> ¬a ¬b c = {!!} | |
71 | |
64 postulate | 72 postulate |
65 def-eq : { P Q p q : OD } → P ≡ Q → p ≡ q → (pt : P ∋ p ) → (qt : Q ∋ q ) → pt ≅ qt | 73 def-eq : { P Q p q : OD } → P ≡ Q → p ≡ q → (pt : P ∋ p ) → (qt : Q ∋ q ) → pt ≅ qt |
66 | 74 |
75 ∈-to-ord : {p : Ordinal } → ( ZFProduct ∋ ord→od p ) → ord-pair p | |
76 ∈-to-ord {p} lt = def-subst {ZFProduct} {(od→ord (ord→od p))} {_} {_} lt refl diso | |
77 | |
78 ord-to-∈ : {p : Ordinal } → ord-pair p → ZFProduct ∋ ord→od p | |
79 ord-to-∈ {p} lt = def-subst {_} {_} {ZFProduct} {(od→ord (ord→od p))} lt refl (sym diso) | |
80 | |
81 lemma333 : { A a : OD } → { x : A ∋ a } → def-subst {A} {od→ord a} (def-subst {A} {od→ord a} x refl refl ) refl refl ≡ x | |
82 lemma333 = refl | |
83 | |
84 lemma334 : { A B : OD } → {a b : Ordinal} → { x : A ∋ ord→od a } → { y : B ∋ ord→od b } → (f1 : A ≡ B) → (f2 : a ≡ b) | |
85 → def-subst {B} {od→ord (ord→od b)} (def-subst {A} { od→ord (ord→od a)} x f1 (cong (λ k → od→ord (ord→od k)) f2 )) refl refl ≅ x | |
86 lemma334 {A} {A} {a} {a} {x} {y} refl refl with def-eq {A} {A} {ord→od a} {ord→od a} refl refl x y | |
87 ... | HE.refl = HE.refl | |
88 | |
89 lemma335 : { A B C : OD } → {a b c : Ordinal} → { x : A ∋ ord→od a } → { y : C ∋ ord→od c } → (f1 : A ≡ B) → (f2 : a ≡ b) → (g1 : B ≡ C) → (g2 : b ≡ c) | |
90 → def-subst {B} {od→ord (ord→od b)} (def-subst {A} { od→ord (ord→od a)} x f1 (cong (λ k → od→ord (ord→od k)) f2 )) g1 (cong (λ k → od→ord (ord→od k)) g2 ) | |
91 ≅ def-subst {A} { od→ord (ord→od a)} {C } { od→ord (ord→od c)} x (trans f1 g1) | |
92 (trans (cong (λ k → od→ord (ord→od k)) f2 ) (cong (λ k → od→ord (ord→od k)) g2 )) | |
93 lemma335 {A} {A} {A} {a} {a} {a} {x} {y} refl refl refl refl with def-eq {A} {A} {ord→od a} {ord→od a} refl refl x y | |
94 ... | HE.refl = HE.refl | |
95 | |
96 ∈-to-ord-oiso : { p : Ordinal } → { x : ord-pair p } → ∈-to-ord (ord-to-∈ x) ≡ x | |
97 ∈-to-ord-oiso {p} {x} = {!!} where | |
98 lemma : def-subst {_} {_} {ZFProduct} {{!!}} (def-subst {_} {_} {ZFProduct} {{!!}} x refl (sym diso)) refl diso ≡ x | |
99 lemma = {!!} | |
100 | |
67 lemma34 : { p q : Ordinal } → (x : ord-pair p ) → (y : ord-pair q ) → p ≡ q → x ≅ y | 101 lemma34 : { p q : Ordinal } → (x : ord-pair p ) → (y : ord-pair q ) → p ≡ q → x ≅ y |
68 lemma34 {p} {q} x y eq = {!!} where | 102 lemma34 {p} {q} x y refl = subst₂ (λ j k → j ≅ k) ∈-to-ord-oiso ∈-to-ord-oiso (HE.cong (λ k → ∈-to-ord k) lemma1 ) where |
69 lemma : (pt : ZFProduct ∋ ord→od p ) → (qt : ZFProduct ∋ ord→od q ) → p ≡ q → pt ≅ qt | 103 lemma : (pt : ZFProduct ∋ ord→od p ) → (qt : ZFProduct ∋ ord→od q ) → p ≡ q → pt ≅ qt |
70 lemma pt qt eq = def-eq {ZFProduct} {ZFProduct} refl {!!} {!!} {!!} | 104 lemma pt qt eq = def-eq {ZFProduct} {ZFProduct} refl (cong (λ k → ord→od k) eq) pt qt |
105 lemma1 : (ord-to-∈ x) ≅ (ord-to-∈ y ) | |
106 lemma1 = lemma (ord-to-∈ x) (ord-to-∈ y ) refl | |
71 | 107 |
72 π1-cong : { p q : OD } → p ≡ q → (pt : ZFProduct ∋ p ) → (qt : ZFProduct ∋ q ) → π1 pt ≅ π1 qt | 108 π1-cong : { p q : OD } → p ≡ q → (pt : ZFProduct ∋ p ) → (qt : ZFProduct ∋ q ) → π1 pt ≅ π1 qt |
73 π1-cong {p} {q} refl s t = HE.cong (λ k → pi1 k ) (def-eq {ZFProduct} {ZFProduct} refl refl s t ) | 109 π1-cong {p} {q} refl s t = HE.cong (λ k → pi1 k ) (def-eq {ZFProduct} {ZFProduct} refl refl s t ) |
74 | 110 |
75 π1--iso : { x y : OD } → (p : ZFProduct ∋ < x , y > ) → π1 p ≅ od→ord x | 111 π1--iso : { x y : OD } → (p : ZFProduct ∋ < x , y > ) → π1 p ≅ od→ord x |