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

comparison cardinal.agda @ 238:a8c6239176db

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
ZFProduct
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 19 Aug 2019 11:39:46 +0900
parents 521290e85527
children b6d80eec5f9e
comparison
equal deleted inserted replaced
237:521290e85527 238:a8c6239176db
25 -- since we use p∨¬p which works only on Level n 25 -- since we use p∨¬p which works only on Level n
26 26
27 <_,_> : (x y : OD) → OD 27 <_,_> : (x y : OD) → OD
28 < x , y > = (x , x ) , (x , y ) 28 < x , y > = (x , x ) , (x , y )
29 29
30 Ord< : {x y : Ordinal } → x o< y → od→ord (Ord x) o< od→ord (Ord y) -- x o< y = Ord y ∋ x → ox o< od→ord (Ord y) 30 data ord-pair : (p : Ordinal) → Set n where
31 Ord< {x} {y} lt with trio< (od→ord (Ord x)) (od→ord (Ord y)) 31 pair : (x y : Ordinal ) → ord-pair ( od→ord ( < ord→od x , ord→od y > ) )
32 Ord< {x} {y} lt | tri< a ¬b ¬c = a 32
33 Ord< {x} {y} lt | tri≈ ¬a b ¬c = ⊥-elim ( o<¬≡ refl (def-subst {Ord y} {x} {Ord x} {x} lt -- Ord x ∋ x 33 ZFProduct : OD
34 (subst₂ (λ j k → j ≡ k) oiso oiso (cong (λ k → ord→od k )(sym b)) )refl )) -- Ord x ≡ Ord y 34 ZFProduct = record { def = λ x → ord-pair x }
35 Ord< {x} {y} lt | tri> ¬a ¬b c = ? where 35
36 lemma : ¬ ( Ord x ∋ ord→od x ) 36 π1' : { p : OD } → ZFProduct ∋ p → OD
37 lemma lt = ⊥-elim ( o<¬≡ refl ( def-subst {_} {_} {Ord x} {x} lt refl diso )) 37 π1' lt = ord→od (pi1 lt) where
38 lemma1 : od→ord (Ord y) o< od→ord (Ord x) → x o< od→ord (Ord x ) 38 pi1 : { p : Ordinal } → ord-pair p → Ordinal
39 lemma1 lt1 = ordtrans ( o<-subst (c<→o< lt ) diso refl ) {!!} 39 pi1 ( pair x y ) = x
40 40
41 --- Ord (osuc ox) ∋ x 41 π2' : { p : OD } → ZFProduct ∋ p → OD
42 --- ox o< od→ord (Ord (osuc ox)) 42 π2' lt = ord→od (pi2 lt) where
43 --- osuc ox ≡ od→ord (Ord (osuc ox)) 43 pi2 : { p : Ordinal } → ord-pair p → Ordinal
44 44 pi2 ( pair x y ) = y
45 opair : {x y : OD} → ( < x , y > ∋ x ) ∧ ( < x , y > ∋ y ) 45
46 opair {x} {y} = record { proj1 = lemma ; proj2 = {!!} } where 46 p-cons : { x y : OD } → ZFProduct ∋ < x , y >
47 ox = (od→ord x) 47 p-cons {x} {y} = def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl (
48 oy = (od→ord y) 48 let open ≡-Reasoning in begin
49 -- < x , y > ∋ x -- od→ord (Ord (omax ox ox )) 49 od→ord < ord→od (od→ord x) , ord→od (od→ord y) >
50 lemma : ox o< (omax (od→ord (x , x)) (od→ord (x , y))) 50 ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩
51 lemma with trio< ox oy 51 od→ord < x , y >
52 lemma | tri< a ¬b ¬c with omax< ox oy a | omxx ox 52 ∎ )
53 ... | eq | eq1 = {!!} 53
54 lemma | tri≈ ¬a b ¬c = {!!} 54
55 lemma | tri> ¬a ¬b c = {!!}
56 55
57 record SetProduct ( A B : OD ) : Set n where 56 record SetProduct ( A B : OD ) : Set n where
58 field 57 field
59 π1 : Ordinal 58 π1 : Ordinal
60 π2 : Ordinal 59 π2 : Ordinal