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

comparison cardinal.agda @ 244:0bd498de2ef4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Product
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 26 Aug 2019 02:07:44 +0900
parents f97a2e4df451
children f0f9aede682f
comparison
equal deleted inserted replaced
243:f97a2e4df451 244:0bd498de2ef4
28 < x , y > = (x , x ) , (x , y ) 28 < x , y > = (x , x ) , (x , y )
29 29
30 data ord-pair : (p : Ordinal) → Set n where 30 data ord-pair : (p : Ordinal) → Set n where
31 pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) ) 31 pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) )
32 32
33 lemma33 : { p q : Ordinal } → p ≡ q → ord-pair p ≡ ord-pair q
34 lemma33 refl = refl
35
36
37
33 ZFProduct : OD 38 ZFProduct : OD
34 ZFProduct = record { def = λ x → ord-pair x } 39 ZFProduct = record { def = λ x → ord-pair x }
35 40
36 pi1 : { p : Ordinal } → ord-pair p → Ordinal 41 pi1 : { p : Ordinal } → ord-pair p → Ordinal
37 pi1 ( pair x y ) = x 42 pi1 ( pair x y ) = x
59 eq-pair refl refl = HE.refl 64 eq-pair refl refl = HE.refl
60 65
61 eq-prod : { x x' y y' : OD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' > 66 eq-prod : { x x' y y' : OD } → x ≡ x' → y ≡ y' → < x , y > ≡ < x' , y' >
62 eq-prod refl refl = refl 67 eq-prod refl refl = refl
63 68
69 prod<x : { x y y' : OD } → od→ord y o< od→ord y' → od→ord (< x , y > ) o< od→ord (< x , y' > )
70 prod<x {x} {y} {y'} y<y' with trio< (od→ord x) (od→ord y)
71 prod<x {x} {y} {y'} y<y' | tri≈ ¬a refl ¬c = ? where
72 lemma : ?
73 lemma = ?
74 prod<x {x} {y} {y'} y<y' | tri< a ¬b ¬c = {!!}
75 prod<x {x} {y} {y'} y<y' | tri> ¬a ¬b c = {!!}
76
77 eq-prod' : { x y y' : OD } → < x , y > ≡ < x , y' > → y ≡ y'
78 eq-prod' {x} {y} {y'} eq with trio< (od→ord y) (od→ord y')
79 eq-prod' {x} {y} {y'} eq | tri≈ ¬a b ¬c = subst₂ (λ j k → j ≡ k ) oiso oiso ( cong ( λ k → ord→od k ) b )
80 eq-prod' {x} {y} {y'} eq | tri< a ¬b ¬c = {!!}
81 eq-prod' {x} {y} {y'} eq | tri> ¬a ¬b c = {!!}
82
83 -- def-eq : { P Q p q : OD } → P ≡ Q → p ≡ q → (pt : P ∋ p ) → (qt : Q ∋ q ) → pt ≅ qt
84 -- def-eq refl refl _ _ = ?
85
86 lemma34 : { p q : Ordinal } → (x : ord-pair p ) → (y : ord-pair q ) → p ≡ q → x ≅ y
87 lemma34 {p} (pair x0 x1) (pair y0 y1) eq = {!!}
88
89 prod-eq : { p q : OD } → p ≡ q → (pt : ZFProduct ∋ p ) → (qt : ZFProduct ∋ q ) → pt ≅ qt
90 prod-eq refl s t = {!!} where
91 lemma : {P : Ordinal } → ( pt qt : ord-pair P ) → pt ≅ qt
92 lemma = {!!}
93
64 π1-cong : { p q : OD } → p ≡ q → (pt : ZFProduct ∋ p ) → (qt : ZFProduct ∋ q ) → π1 pt ≅ π1 qt 94 π1-cong : { p q : OD } → p ≡ q → (pt : ZFProduct ∋ p ) → (qt : ZFProduct ∋ q ) → π1 pt ≅ π1 qt
65 π1-cong {p} {q} refl s t = HE.cong (λ k → pi1 k ) (lemma s t refl ) where 95 π1-cong {p} {q} refl s t = HE.cong (λ k → pi1 k ) (prod-eq refl s t )
66 lemma : { op oq : Ordinal } → (P : ord-pair op ) → (Q : ord-pair oq ) → op ≡ oq → P ≅ Q
67 lemma (pair x y ) (pair x' y') eq = eq-pair {!!} {!!}
68 96
69 Tlemma : { x y x' y' : Ordinal } → (prod : ord-pair (od→ord < ord→od x , ord→od y >)) 97 Tlemma : { x y x' y' : Ordinal } → (prod : ord-pair (od→ord < ord→od x , ord→od y >))
70 → (prod' : ord-pair (od→ord < ord→od x' , ord→od y' >)) → x ≡ x' → y ≡ y' → prod ≅ prod' 98 → (prod' : ord-pair (od→ord < ord→od x' , ord→od y' >)) → x ≡ x' → y ≡ y' → prod ≅ prod'
71 Tlemma prod prod' refl refl = lemma prod prod' refl where 99 Tlemma prod prod' refl refl = lemma prod prod' refl where
72 lemma : { p q : Ordinal } → (prod : ord-pair p) → (prod1 : ord-pair q) → p ≡ q → prod ≅ prod1 100 lemma : { p q : Ordinal } → (prod : ord-pair p) → (prod1 : ord-pair q) → p ≡ q → prod ≅ prod1
73 lemma (pair x y) (pair x' y') eq = {!!} 101 lemma (pair x y) (pair x' y') eq = {!!}
102
103 π1--iso : { x y : OD } → (p : ZFProduct ∋ < x , y > ) → π1 p ≡ od→ord x
104 π1--iso {x} {y} p = {!!} where
105 lemma1 : ( ox oy op : Ordinal ) → (p : ord-pair op) → op ≡ od→ord ( < ord→od ox , ord→od oy >) → p ≅ pair ox oy
106 lemma1 ox oy op (pair x' y') eq = {!!}
107 lemma : ( ox oy op : Ordinal ) → (p : ord-pair op ) → op ≡ od→ord ( < ord→od ox , ord→od oy > ) → pi1 p ≡ ox
108 lemma ox oy op (pair ox' oy') eq = {!!}
74 109
75 p-iso : { x : OD } → {p : ZFProduct ∋ x } → < ord→od (π1 p) , ord→od (π2 p) > ≡ x 110 p-iso : { x : OD } → {p : ZFProduct ∋ x } → < ord→od (π1 p) , ord→od (π2 p) > ≡ x
76 p-iso {x} {p} with p-cons (ord→od (π1 p)) (ord→od (π2 p)) 111 p-iso {x} {p} with p-cons (ord→od (π1 p)) (ord→od (π2 p))
77 ... | t = {!!} 112 ... | t = {!!}
78 113