diff cardinal.agda @ 235:846e0926bb89

fix cardinal
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 15 Aug 2019 04:51:24 +0900
parents e06b76e5b682
children 650bdad56729
line wrap: on
line diff
--- 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 ψ))
 
 ------------
 --