changeset 246:3506f53c7d83

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 26 Aug 2019 02:50:16 +0900
parents f0f9aede682f
children d09437fcfc7c
files cardinal.agda
diffstat 1 files changed, 4 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/cardinal.agda	Mon Aug 26 02:34:14 2019 +0900
+++ b/cardinal.agda	Mon Aug 26 02:50:16 2019 +0900
@@ -72,12 +72,12 @@
 π1-cong :  { p q : OD } →  p ≡ q → (pt : ZFProduct ∋ p ) → (qt : ZFProduct ∋ q ) → π1 pt ≅ π1 qt
 π1-cong {p} {q} refl s t = HE.cong (λ k → pi1 k ) (def-eq {ZFProduct} {ZFProduct} refl refl s t ) 
 
-π1--iso :  { x y : OD } → (p : ZFProduct ∋ < x , y > )  →  π1 p ≡ od→ord x
-π1--iso {x} {y} p  = {!!} where
+π1--iso :  { x y : OD } → (p : ZFProduct ∋ < x , y > )  →  π1 p ≅  od→ord x
+π1--iso {x} {y} p  = lemma (od→ord x) (od→ord y) {!!} {!!} refl where
    lemma1 : ( ox oy op : Ordinal ) → (p : ord-pair op) → op ≡  od→ord ( < ord→od ox , ord→od oy >)  → p ≅ pair ox oy
    lemma1 ox oy op (pair x' y')  eq = lemma34 {!!} {!!} {!!}
-   lemma : ( ox oy op : Ordinal ) → (p : ord-pair op ) → op ≡ od→ord ( < ord→od ox , ord→od oy > )  → pi1 p ≡ ox
-   lemma ox oy op (pair ox' oy') eq  = {!!}
+   lemma : ( ox oy op : Ordinal ) → (p : ord-pair op ) → op ≡ od→ord ( < ord→od ox , ord→od oy > )  → pi1 p ≅ ox
+   lemma ox oy op p eq  = {!!} -- HE.cong (λ k → pi1 k ) (lemma1 ox oy op p eq  )
 
 p-iso :  { x  : OD } → {p : ZFProduct ∋ x } → < ord→od (π1 p) , ord→od (π2 p) > ≡ x
 p-iso {x} {p} with p-cons (ord→od (π1 p)) (ord→od (π2 p))