# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1566726281 -32400
# Node ID c10048d696148702f4f7ced9b4bca57250644b96
# Parent  ccc84f289c9814130ebe5c4c2fa4aab2f9df7df3
...

diff -r ccc84f289c98 -r c10048d69614 cardinal.agda
--- a/cardinal.agda	Thu Aug 22 12:41:41 2019 +0900
+++ b/cardinal.agda	Sun Aug 25 18:44:41 2019 +0900
@@ -33,23 +33,55 @@
 ZFProduct : OD
 ZFProduct = record { def = λ x → ord-pair x }
 
+pi1 : { p : Ordinal } →   ord-pair p →  Ordinal
+pi1 ( pair x y ) = x
+
 π1 : { p : OD } → ZFProduct ∋ p → Ordinal
-π1 lt = pi1 lt where
-   pi1 : { p : Ordinal } →   ord-pair p →  Ordinal
-   pi1 ( pair x y ) = x
+π1 lt = pi1 lt 
+
+pi2 : { p : Ordinal } →   ord-pair p →  Ordinal
+pi2 ( pair x y ) = y
 
 π2 : { p : OD } → ZFProduct ∋ p → Ordinal
-π2 lt = pi2 lt where
-   pi2 : { p : Ordinal } →   ord-pair p →  Ordinal
-   pi2 ( pair x y ) = y
+π2 lt = pi2 lt 
 
-p-cons :  { x y  : OD } → ZFProduct ∋ < x , y >
-p-cons {x} {y} =  def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl (
+p-cons :  ( x y  : OD ) → ZFProduct ∋ < x , y >
+p-cons x y =  def-subst {_} {_} {ZFProduct} {od→ord (< x , y >)} (pair (od→ord x) ( od→ord y )) refl (
     let open ≡-Reasoning in begin
         od→ord < ord→od (od→ord x) , ord→od (od→ord y) >
     ≡⟨ cong₂ (λ j k → od→ord < j , k >) oiso oiso ⟩
         od→ord < x , y >
     ∎ )
+
+π1-iso :  { x y : OD } → π1 ( p-cons  x  y  ) ≡ od→ord x
+π1-iso {x} {y} = {!!} where
+   lemma : {ox oy : Ordinal} →  pi1 ( pair ox oy )  ≡ ox
+   lemma = refl
+   lemma2 : {ox oy : Ordinal} →
+      def-subst {ZFProduct} {_}  (pair (od→ord (ord→od ox)) (od→ord (ord→od oy))) refl (trans (cong₂ (λ j k → od→ord < j , k >) oiso oiso) refl) ≡ pair ox oy
+   lemma2 {ox} {oy} = let open ≡-Reasoning in begin
+        def-subst {ZFProduct} {_}  (pair (od→ord (ord→od ox)) (od→ord (ord→od oy))) refl (trans (cong₂ (λ j k → od→ord < j , k >) oiso oiso) refl) 
+      ≡⟨ ? ⟩
+        pair ox oy 
+      ∎
+   lemma1 : {ox oy : Ordinal} → π1 ( p-cons  (ord→od ox)  (ord→od oy) ) ≡ ox
+   lemma1 {ox} {oy} = let open ≡-Reasoning in begin
+         π1 ( p-cons  (ord→od ox)  (ord→od oy) )
+      ≡⟨⟩
+         pi1 (pair (pi1 (def-subst {ZFProduct} {_}  (pair (od→ord (ord→od ox)) (od→ord (ord→od oy))) refl (trans (cong₂ (λ j k → od→ord < j , k >) oiso oiso) refl)))  oy )
+      ≡⟨ cong (λ k → pi1 k) lemma2  ⟩
+         pi1 (pair ox oy )
+      ≡⟨ lemma {ox} {oy} ⟩
+         ox
+      ∎
+
+p-iso :  { x  : OD } → {p : ZFProduct ∋ x } → < ord→od (π1 p) , ord→od (π2 p) > ≡ x
+p-iso {x} {p} = pi p pc  where
+   pc : ZFProduct ∋ < ord→od (π1 p) , ord→od (π2 p) >
+   pc = p-cons (ord→od (π1 p)) (ord→od (π2 p)) 
+   pi : { prod prod1 : Ordinal } →   ord-pair prod → ord-pair prod1 → {!!}
+   pi (pair p1 p2) (pair q1 q2) = {!!}
+
     
 
 ∋-p : (A x : OD ) → Dec ( A ∋ x ) 
@@ -62,6 +94,11 @@
     checkAB : { p : Ordinal } → def ZFProduct p → Set n
     checkAB (pair x y) = def A x ∧ def B y
 
+func→od0  : (f : Ordinal → Ordinal ) → OD
+func→od0  f = record { def = λ x → def ZFProduct x ∧ ( { x : Ordinal } → (p : def ZFProduct x ) → checkfunc p ) } where
+    checkfunc : { p : Ordinal } → def ZFProduct p → Set n
+    checkfunc (pair x y) = f x ≡ y
+
 --  Power (Power ( A ∪ B )) ∋ ( A ⊗ B )
 
 Func :  ( A B : OD ) → OD
@@ -73,12 +110,12 @@
 func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD 
 func→od f dom = Replace dom ( λ x →  < x , ord→od (f (od→ord x)) > )
 
-record Func←cd { dom cod : OD } {f : Ordinal } (f<F :  def (Func dom cod ) f) : Set n where
+record Func←cd { dom cod : OD } {f : Ordinal }  : Set n where
    field
       func-1 : Ordinal → Ordinal
-      func→od∈Func-1 :  (Func dom (Ord (sup-o (λ x → func-1 x)) )) ∋  func→od func-1 dom
+      func→od∈Func-1 :  Func dom cod ∋  func→od func-1 dom
  
-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 : OD } → {f : Ordinal }  → def (Func dom cod ) f  → Func←cd {dom} {cod} {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)
@@ -88,19 +125,12 @@
            lemma2 (pair x1 y1) with decp ( x1 ≡ x)
            lemma2 (pair x1 y1) | yes p = y1
            lemma2 (pair x1 y1) | no ¬p = o∅
+   fod : OD
+   fod = Replace dom ( λ x →  < x , ord→od (sup-o ( λ y → lemma (od→ord x) y )) > )
 
 
 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 = {!!} } where
-   f<F :  def (Func dom (Ord (sup-o (λ x → f x)))) (od→ord (func→od f dom))
-   f<F = {!!}
-   odfunc : Func←cd {dom} f<F
-   odfunc = ( od→func {dom} {Ord (sup-o (λ x → f x))} {od→ord (func→od f dom)} f<F )
-   lemma :  Func dom (Ord (sup-o ( func-1 odfunc ) )) ∋  func→od (func-1 odfunc ) dom
-   lemma = func→od∈Func-1 odfunc
-
 -- contra position of sup-o<
 --
 
diff -r ccc84f289c98 -r c10048d69614 ordinal.agda
--- a/ordinal.agda	Thu Aug 22 12:41:41 2019 +0900
+++ b/ordinal.agda	Sun Aug 25 18:44:41 2019 +0900
@@ -1,4 +1,3 @@
-{-# OPTIONS --allow-unsolved-metas #-}
 open import Level
 module ordinal where