--- a/ordinal.agda	Sat Apr 25 15:09:17 2020 +0900
+++ b/ordinal.agda	Sat May 09 09:02:52 2020 +0900
@@ -233,62 +233,3 @@
             ψ (record { lv = lx ; ord = OSuc lx x₁ })
         caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev 
 
-module C-Ordinal-with-choice {n : Level} where
-
-  import OD 
-  -- open inOrdinal C-Ordinal 
-  open OD (C-Ordinal {n})
-  open OD.OD
-  open _⊆_
-
-  o<→c< :  {x y : Ordinal } → x o< y →   Ord x ⊆ Ord y 
-  o<→c< lt = record { incl = λ lt1 → ordtrans lt1 lt }
-
-  ⊆→o< :  {x y : Ordinal } →  Ord x ⊆ Ord y →  x o< osuc y
-  ⊆→o< {x} {y}  lt with trio< x y 
-  ⊆→o< {x} {y}  lt | tri< a ¬b ¬c = ordtrans a <-osuc
-  ⊆→o< {x} {y}  lt | tri≈ ¬a b ¬c = subst ( λ k → k o< osuc y) (sym b) <-osuc
-  ⊆→o< {x} {y}  lt | tri> ¬a ¬b c with incl lt  (o<-subst c (sym diso) refl )
-  ... | ttt = ⊥-elim ( o<¬≡ refl (o<-subst ttt diso refl ))
-
-  -- ZFSubset : (A x : OD  ) → OD 
-  -- ZFSubset A x =  record { def = λ y → def A y ∧  def x y }  
-
-  -- Def :  (A :  OD ) → OD 
-  -- Def  A = Ord ( sup-o  ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )   
-
-  Ord-lemma : (a : Ordinal)  →  ord→od a ⊆ Ord a
-  Ord-lemma a  = record { incl = λ lt → o<-subst (c<→o< lt ) refl diso }
-
-  ⊆-trans :  {a b c x : OD}  →  a ⊆ b  →   b ⊆ c  → a ⊆ c     
-  ⊆-trans a⊆b b⊆c = record { incl = λ a∋x →  incl b⊆c (incl a⊆b a∋x) }
-
-  _∩_ = IsZF._∩_ isZF
-
--- 
---   ord-power-lemma : {a : Ordinal} → Power (Ord a) == Def (Ord a)
---   ord-power-lemma {a} = record { eq→ = left ; eq← = right } where
---        left : {x : Ordinal} → def (Power (Ord a)) x → def (Def (Ord a)) x
---        left {x} lt = lemma1 where
---           lemma : od→ord ((Ord a) ∩ (ord→od x)) o< sup-o ( λ y → od→ord ((Ord a) ∩ (ord→od y)))
---           lemma = sup-o< { λ y → od→ord ((Ord a) ∩ (ord→od y))} {x} 
---           lemma1 : x o<  sup-o  ( λ x → od→ord ( ZFSubset (Ord a) (ord→od x ))) 
---           lemma1 = {!!}
---        right : {x : Ordinal } → def (Def (Ord a)) x → def (Power (Ord a)) x
---        right {x} lt = def-subst {_} {_} {Power (Ord a)} {x} (IsZF.power← isZF (Ord a) (ord→od x) {!!}) refl diso
--- 
---   uncountable : (a y : Ordinal) →  Ord (osuc a) ∋ ZFSubset (Ord a) (ord→od y) 
---   uncountable a y = ⊆→o<  lemma  where
---        lemma-a :  (x : OD ) → _⊆_ (ZFSubset (Ord a) (ord→od y)) (Ord a) {x}
---        lemma-a x lt = proj1 lt
---        lemma :  (x : OD ) → _⊆_ (Ord ( od→ord (ZFSubset (Ord a) (ord→od y)))) (Ord a) {x}
---        lemma x = {!!}
--- 
---   continuum-hyphotheis : (a : Ordinal) → (x : OD) → _⊆_  (Power (Ord a)) (Ord (osuc a)) {x}
---   continuum-hyphotheis a x = lemma2 where
---        lemma1 : sup-o (λ x₁ → od→ord (ZFSubset (Ord a) (ord→od x₁))) o< osuc a
---        lemma1 = {!!}
---        lemma : _⊆_ (Def (Ord a))  (Ord (osuc a)) {x}
---        lemma = o<→c< lemma1
---        lemma2 : _⊆_ (Power (Ord a))  (Ord (osuc a)) {x}
---        lemma2 = subst ( λ k → _⊆_ k (Ord (osuc a)) {x} ) (sym (==→o≡ ord-power-lemma)) lemma