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

comparison cardinal.agda @ 253:0446b6c5e7bc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
proudct uniquness done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 29 Aug 2019 16:08:46 +0900
parents 8a58e2cd1f55
children 2ea2a19f9cd6
comparison
equal deleted inserted replaced
252:8a58e2cd1f55 253:0446b6c5e7bc
123 123
124 124
125 p-iso1 : { ox oy : Ordinal } → ZFProduct ∋ < ord→od ox , ord→od oy > 125 p-iso1 : { ox oy : Ordinal } → ZFProduct ∋ < ord→od ox , ord→od oy >
126 p-iso1 {ox} {oy} = pair ox oy 126 p-iso1 {ox} {oy} = pair ox oy
127 127
128 postulate 128 p-iso : { x : OD } → (p : ZFProduct ∋ x ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ x
129 p-iso : { x : OD } → (p : ZFProduct ∋ x ) → < ord→od (π1 p) , ord→od (π2 p) > ≡ x 129 p-iso {x} p = ord≡→≡ (lemma2 p) where
130 lemma : { op : Ordinal } → (q : ord-pair op ) → od→ord < ord→od (pi1 q) , ord→od (pi2 q) > ≡ op
131 lemma (pair ox oy) = refl
132 lemma2 : { x : OD } → (p : ZFProduct ∋ x ) → od→ord < ord→od (π1 p) , ord→od (π2 p) > ≡ od→ord x
133 lemma2 {x} p = lemma p
130 134
131 135
132 ∋-p : (A x : OD ) → Dec ( A ∋ x ) 136 ∋-p : (A x : OD ) → Dec ( A ∋ x )
133 ∋-p A x with p∨¬p ( A ∋ x ) 137 ∋-p A x with p∨¬p ( A ∋ x )
134 ∋-p A x | case1 t = yes t 138 ∋-p A x | case1 t = yes t