# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1566373409 -32400
# Node ID c76c812de3950db8cfee1040c2b9b8ba2f55cf60
# Parent  b6d80eec5f9e23f33978d153c26e70396a2ece37
fix

diff -r b6d80eec5f9e -r c76c812de395 cardinal.agda
--- a/cardinal.agda	Tue Aug 20 10:36:37 2019 +0900
+++ b/cardinal.agda	Wed Aug 21 16:43:29 2019 +0900
@@ -78,29 +78,24 @@
       func-1 : Ordinal → Ordinal
       func→od∈Func-1 :  (Func dom (Ord (sup-o (λ x → func-1 x)) )) ∋  func→od func-1 dom
  
-od→func : { dom cod : OD } → {f : Ordinal }  → def (Func dom cod ) f → (Ordinal → Ordinal )
-od→func {dom} {cod} {f} lt x = sup-o ( λ y → lemma  y ) where
-   lemma2 : {p : Ordinal} → ord-pair p  → Ordinal
-   lemma2 (pair x1 y1) with decp ( x1 ≡ x)
-   lemma2 (pair x1 y1) | yes p = y1
-   lemma2 (pair x1 y1) | no ¬p = o∅
-   lemma : Ordinal → Ordinal
-   lemma y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → def (Power (dom ⊗ cod)) k ) (sym diso) lt ) | ∋-p (ord→od f) (ord→od y)
-   lemma y | p | no n  = o∅
-   lemma y | p | yes f∋y = lemma2 (proj1 (double-neg-eilm ( p {ord→od y} f∋y ))) -- p : {y : OD} → f ∋ y → ¬ ¬ (dom ⊗ cod ∋ y)
-
-func←od1 : { dom cod : OD } → {f : Ordinal }  → (f<F : def (Func dom cod ) f ) → Func←cd {dom} {cod} {f} f<F
-func←od1 {dom} {cod} {f} lt = record { func-1 = λ x → sup-o ( λ y → lemma x y ) ; func→od∈Func-1 = {!!} } where
+od→func : { dom cod : OD } → {f : Ordinal }  → (f<F : def (Func dom cod ) f ) → Func←cd {dom} {cod} {f} f<F
+od→func {dom} {cod} {f} lt = record { func-1 = λ x → sup-o ( λ y → lemma x y ) ; func→od∈Func-1 = record { proj1 = {!!} ; proj2 = {!!} } } where
    lemma : Ordinal → Ordinal → Ordinal
    lemma x y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → def (Power (dom ⊗ cod)) k ) (sym diso) lt ) | ∋-p (ord→od f) (ord→od y)
    lemma x y | p | no n  = o∅
-   lemma x y | p | yes f∋y with double-neg-eilm ( p {ord→od y} f∋y ) -- p : {x : OD} → f ∋ x → ¬ ¬ (dom ⊗ cod ∋ x)
-   ... | t with decp ( x  ≡ π1 {!!} )
-   ... | yes _ = π2 {!!}
-   ... | no _ = o∅
+   lemma x y | p | yes f∋y = lemma2 (proj1 (double-neg-eilm ( p {ord→od y} f∋y ))) where -- p : {y : OD} → f ∋ y → ¬ ¬ (dom ⊗ cod ∋ y) 
+           lemma2 : {p : Ordinal} → ord-pair p  → Ordinal
+           lemma2 (pair x1 y1) with decp ( x1 ≡ x)
+           lemma2 (pair x1 y1) | yes p = y1
+           lemma2 (pair x1 y1) | no ¬p = o∅
+
+
+open Func←cd
 
 func→od∈Func :  (f : Ordinal → Ordinal ) ( dom : OD ) → (Func dom (Ord (sup-o (λ x → f x)) )) ∋  func→od f dom 
-func→od∈Func f dom  = record { proj1 = {!!} ; proj2 = {!!} }
+func→od∈Func f dom  = record { proj1 = {!!} ; proj2 = {!!} } where
+   lemma :  (Func dom (Ord (sup-o (λ x → f x)) )) ∋  func→od f dom 
+   lemma = {!!} -- func→od∈Func-1 ( od→func {dom} {{!!}} {od→ord (func→od f {!!} )} {!!} )
 
 -- contra position of sup-o<
 --
@@ -124,7 +119,7 @@
        xfunc : def (Func X Y) xmap 
        yfunc : def (Func Y X) ymap 
        onto-iso   : {y :  Ordinal  } → (lty : def Y y ) →
-          od→func {X} {Y} {xmap} xfunc ( od→func  yfunc y )  ≡ y
+          func-1 ( od→func {X} {Y} {xmap} xfunc ) ( func-1 (od→func  yfunc) y )  ≡ y 
 
 open Onto
 
@@ -144,7 +139,7 @@
        xfunc1 = {!!}
        zfunc : def (Func Z X) zmap 
        zfunc = {!!}
-       onto-iso1   : {z :  Ordinal  } → (ltz : def Z z ) → od→func  xfunc1 ( od→func  zfunc z )  ≡ z
+       onto-iso1   : {z :  Ordinal  } → (ltz : def Z z ) → func-1 (od→func  xfunc1 )  (func-1 (od→func  zfunc ) z )  ≡ z
        onto-iso1   = {!!}