# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1565567931 -32400
# Node ID 1b1620e2053cfc340a4df0d63de65b9059b19b6f
# Parent  5e36744b8dcec39bd43028bbe98b3af9326ff3f2
we need ordered pair

diff -r 5e36744b8dce -r 1b1620e2053c cardinal.agda
--- a/cardinal.agda	Mon Aug 12 02:26:32 2019 +0900
+++ b/cardinal.agda	Mon Aug 12 08:58:51 2019 +0900
@@ -21,9 +21,11 @@
 open _∨_
 open Bool
 
+-- we have to work on Ordinal to keep OD Level n
+-- since we use p∨¬p which works only on Level n
 
-func : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD 
-func f dom = Replace dom ( λ x →  x , (ord→od (f (od→ord x) )))
+func→od : (f : Ordinal → Ordinal ) → ( dom : OD ) → OD 
+func→od f dom = Replace dom ( λ x →  x , (ord→od (f (od→ord x) )))
 
 record _⊗_  (A B : Ordinal) : Set n where
    field
@@ -32,17 +34,14 @@
       A∋π1 : def (ord→od A)  π1
       B∋π2 : def (ord→od B)  π2
 
+-- Clearly wrong. We need ordered pair
 Func :  ( A B : OD ) → OD
 Func A B = record { def = λ x → (od→ord A) ⊗ (od→ord B) }
 
-π1 :  { A B x : OD } → Func A B ∋ x → OD
-π1 {A} {B} {x} p = ord→od (_⊗_.π1 p)
+open  _⊗_
 
-π2 :  { A B x : OD } → Func A B ∋ x → OD
-π2 {A} {B} {x} p = ord→od (_⊗_.π2 p)
-
-Func→func : { dom cod : OD } → (f : OD )  → Func dom cod ∋ f → (Ordinal → Ordinal )
-Func→func {dom} {cod} f lt x = sup-o ( λ y → lemma  y ) where
+func←od : { dom cod : OD } → (f : OD )  → Func dom cod ∋ f → (Ordinal → Ordinal )
+func←od {dom} {cod} f lt x = sup-o ( λ y → lemma  y ) where
    lemma : Ordinal → Ordinal
    lemma y with p∨¬p ( _⊗_.π1 lt ≡ x )
    lemma y | case1 refl = _⊗_.π2 lt
@@ -69,13 +68,35 @@
        ymap : Ordinal 
        xfunc : def (Func X Y) xmap 
        yfunc : def (Func Y X) ymap 
-       onto-iso   : {y :  Ordinal  } → (lty : def Y y ) → Func→func (ord→od xmap) xfunc ( Func→func (ord→od ymap) yfunc y )  ≡ y
+       onto-iso   : {y :  Ordinal  } → (lty : def Y y ) → func←od (ord→od xmap) xfunc ( func←od (ord→od ymap) yfunc y )  ≡ y
+
+open Onto
+
+onto-restrict : {X Y Z : OD} → Onto X Y → ({x : OD} → _⊆_ Z Y {x}) → Onto X Z
+onto-restrict {X} {Y} {Z} onto  Z⊆Y = record {
+     xmap = xmap1
+   ; ymap = zmap
+   ; xfunc = xfunc1
+   ; yfunc = zfunc
+   ; onto-iso = onto-iso1
+  } where
+       xmap1 : Ordinal 
+       xmap1 = od→ord (Select (ord→od (xmap onto)) {!!} ) 
+       zmap : Ordinal 
+       zmap = {!!}
+       xfunc1 : def (Func X Z) xmap1
+       xfunc1 = {!!}
+       zfunc : def (Func Z X) zmap 
+       zfunc = {!!}
+       onto-iso1   : {z :  Ordinal  } → (ltz : def Z z ) → func←od (ord→od xmap1) xfunc1 ( func←od (ord→od zmap) zfunc z )  ≡ z
+       onto-iso1   = {!!}
+
 
 record Cardinal  (X  : OD ) : Set n where
    field
        cardinal : Ordinal 
-       conto : Onto (Ord cardinal) X 
-       cmax : ( y : Ordinal  ) → cardinal o< y → ¬ Onto (Ord y) X 
+       conto : Onto X (Ord cardinal)  
+       cmax : ( y : Ordinal  ) → cardinal o< y → ¬ Onto X (Ord y)  
 
 cardinal :  (X  : OD ) → Cardinal X
 cardinal  X = record {
@@ -83,27 +104,30 @@
      ; conto = onto
      ; cmax = cmax
    } where
-    cardinal-p : (x  : Ordinal ) →  ( Ordinal  ∧ Dec (Onto (Ord x) X) )
-    cardinal-p x with p∨¬p ( Onto (Ord x) X ) 
-    cardinal-p x | case1 True = record { proj1 = x ; proj2 = yes True }
+    cardinal-p : (x  : Ordinal ) →  ( Ordinal  ∧ Dec (Onto X (Ord x) ) )
+    cardinal-p x with p∨¬p ( Onto X (Ord x)  ) 
+    cardinal-p x | case1 True  = record { proj1 = x  ; proj2 = yes True }
     cardinal-p x | case2 False = record { proj1 = o∅ ; proj2 = no False }
     S = sup-o (λ x → proj1 (cardinal-p x))
-    lemma1 :  (x : Ordinal) → ((y : Ordinal) → y o< x → Lift (suc n) (y o< (osuc S) → Onto (Ord y) X)) →
-                    Lift (suc n) (x o< (osuc S) → Onto (Ord x) X)
+    lemma1 :  (x : Ordinal) → ((y : Ordinal) → y o< x → Lift (suc n) (y o< (osuc S) → Onto X (Ord y))) →
+                    Lift (suc n) (x o< (osuc S) → Onto X (Ord x) )
     lemma1 x prev with trio< x (osuc S)
     lemma1 x prev | tri< a ¬b ¬c with osuc-≡< a
-    lemma1 x prev | tri< a ¬b ¬c | case1 x=S = {!!}
-    lemma1 x prev | tri< a ¬b ¬c | case2 x<S = {!!}
+    lemma1 x prev | tri< a ¬b ¬c | case1 x=S = lift ( λ lt → {!!} )
+    lemma1 x prev | tri< a ¬b ¬c | case2 x<S = lift ( λ lt → lemma2 ) where
+         lemma2 : Onto X (Ord x) 
+         lemma2 with prev {!!} {!!}
+         ... | lift t = t {!!}
     lemma1 x prev | tri≈ ¬a b ¬c = lift ( λ lt → ⊥-elim ( o<¬≡ b lt ))
     lemma1 x prev | tri> ¬a ¬b c = lift ( λ lt → ⊥-elim ( o<> c lt ))
-    onto : Onto (Ord S) X
-    onto with TransFinite {λ x → Lift (suc n) ( x o< osuc S → Onto (Ord x) X ) } lemma1 S 
-    ... | lift t = t <-osuc  where
-    cmax : (y : Ordinal) → S o< y → ¬ Onto (Ord y) X
+    onto : Onto X (Ord S) 
+    onto with TransFinite {λ x → Lift (suc n) ( x o< osuc S → Onto X (Ord x) ) } lemma1 S 
+    ... | lift t = t <-osuc  
+    cmax : (y : Ordinal) → S o< y → ¬ Onto X (Ord y) 
     cmax y lt ontoy = o<> lt (o<-subst  {_} {_} {y} {S}
        (sup-o<  {λ x → proj1 ( cardinal-p x)}{y}  ) lemma refl ) where
           lemma : proj1 (cardinal-p y) ≡ y
-          lemma with  p∨¬p ( Onto (Ord y) X )
+          lemma with  p∨¬p ( Onto X (Ord y) )
           lemma | case1 x = refl
           lemma | case2 not = ⊥-elim ( not ontoy )