# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1565812284 -32400
# Node ID 846e0926bb89eeec474bd242e1649fdc2cf94a0c
# Parent  e06b76e5b6827904b89ba2540c4186d9e9c2d5dc
fix cardinal

diff -r e06b76e5b682 -r 846e0926bb89 OD.agda
--- a/OD.agda	Tue Aug 13 22:21:10 2019 +0900
+++ b/OD.agda	Thu Aug 15 04:51:24 2019 +0900
@@ -490,7 +490,7 @@
                  ψ : ( ox : Ordinal ) → Set (suc n)
                  ψ ox = (( x : Ordinal ) → x o< ox  → ( ¬ def X x )) ∨ choiced X
                  lemma-ord : ( ox : Ordinal  ) → ψ ox
-                 lemma-ord  ox = IsOrdinals.TransFinite (Ordinals.isOrdinal O) {ψ} induction ox where
+                 lemma-ord  ox = TransFinite {ψ} induction ox where
                     ∋-p : (A x : OD ) → Dec ( A ∋ x ) 
                     ∋-p A x with p∨¬p (Lift (suc n) ( A ∋ x ))
                     ∋-p A x | case1 (lift t)  = yes t
@@ -530,4 +530,3 @@
 Select = ZF.Select OD→ZF
 Replace = ZF.Replace OD→ZF
 isZF = ZF.isZF  OD→ZF
-TransFinite = IsOrdinals.TransFinite (Ordinals.isOrdinal O)
diff -r e06b76e5b682 -r 846e0926bb89 Ordinals.agda
--- a/Ordinals.agda	Tue Aug 13 22:21:10 2019 +0900
+++ b/Ordinals.agda	Thu Aug 15 04:51:24 2019 +0900
@@ -50,6 +50,7 @@
         ¬x<0 = IsOrdinals.¬x<0 (Ordinals.isOrdinal O)
         osuc-≡< = IsOrdinals.osuc-≡<  (Ordinals.isOrdinal O)
         <-osuc = IsOrdinals.<-osuc  (Ordinals.isOrdinal O)
+        TransFinite = IsOrdinals.TransFinite  (Ordinals.isOrdinal O)
         
         o<-dom :   { x y : Ordinal } → x o< y → Ordinal 
         o<-dom  {x} _ = x
diff -r e06b76e5b682 -r 846e0926bb89 cardinal.agda
--- a/cardinal.agda	Tue Aug 13 22:21:10 2019 +0900
+++ b/cardinal.agda	Thu Aug 15 04:51:24 2019 +0900
@@ -55,9 +55,8 @@
 
 func←od : { dom cod : OD } → {f : Ordinal }  → def (Func dom cod ) f → (Ordinal → Ordinal )
 func←od {dom} {cod} {f} lt x = sup-o ( λ y → lemma  y ) where
-   lemma1 = subst (λ k → def (Power (dom ⊗ cod)) k ) (sym {!!}) lt
    lemma : Ordinal → Ordinal
-   lemma y with IsZF.power→ isZF (dom ⊗ cod) (ord→od f) (subst (λ k → def (Power (dom ⊗ cod)) k ) {!!} lt ) | ∋-p (ord→od f) (ord→od y)
+   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 with double-neg-eilm ( p {ord→od y} f∋y ) -- p : {x : OD} → f ∋ x → ¬ ¬ (dom ⊗ cod ∋ x)
    ... | t with decp ( x  ≡ π1 t )
@@ -71,10 +70,10 @@
 -- contra position of sup-o<
 --
 
-postulate
-  -- contra-position of mimimulity of supermum required in Cardinal
-  sup-x  : ( Ordinal  → Ordinal ) →  Ordinal 
-  sup-lb : { ψ : Ordinal  →  Ordinal } → {z : Ordinal }  →  z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
+-- postulate
+--   -- contra-position of mimimulity of supermum required in Cardinal
+--   sup-x  : ( Ordinal  → Ordinal ) →  Ordinal 
+--   sup-lb : { ψ : Ordinal  →  Ordinal } → {z : Ordinal }  →  z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
 
 ------------
 --