--- a/generic-filter.agda	Sat Dec 19 21:58:32 2020 +0900
+++ b/generic-filter.agda	Sun Dec 20 12:37:07 2020 +0900
@@ -5,7 +5,7 @@
 import filter 
 open import zf
 open import logic
-open import partfunc {n} O
+-- open import partfunc {n} O
 import OD 
 
 open import Relation.Nullary 
@@ -54,23 +54,6 @@
 import OPair
 open OPair O
 
-open PFunc
-
-_f∩_ : (f g : PFunc (Lift n Nat) (Lift n Two) ) →  PFunc (Lift n Nat) (Lift n Two)
-f f∩ g = record { dom = λ x → (dom f x ) ∧ (dom g x ) ∧ ((fr : dom f x ) → (gr : dom g x ) → pmap f x fr ≡ pmap g x gr)
-              ; pmap = λ x p →  pmap f x (proj1  p) ; meq = meq f }
-
-_↑_ :  (Nat → Two) → Nat →  PFunc (Lift n Nat) (Lift n Two)
-_↑_  f i = record { dom = λ x → Lift n (lower x ≤ i) ; pmap = λ x _ → lift (f (lower x)) ; meq = λ {x} {p} {q} → refl }
-
-record _f⊆_ (f g : PFunc (Lift n Nat) (Lift n Two)  ) : Set (suc n) where
-  field
-     extend : {x : Nat} → (fr : dom f (lift x) ) →  dom g (lift x  )
-     feq : {x : Nat} → {fr : dom f (lift x) } →  pmap f (lift x) fr ≡ pmap g (lift x) (extend fr)
-
-open _f⊆_ 
-open import Data.Nat.Properties
-
 ODSuc : (y : HOD) → infinite ∋ y → HOD
 ODSuc y lt = Union (y , (y , y)) 
 
@@ -153,12 +136,9 @@
 open _⊆_
 
 -- someday ...
-postulate 
-   ω→2f-iso : (X : HOD) → ( lt : ω→2 ∋ X ) → fω→2 ( ω→2f X lt )  =h= X
-   fω→2-iso : (f : Nat → Two) → ω→2f ( fω→2 f ) (ω2∋f f) ≡ f
-
-↑n : (f n : HOD) → ((ω→2 ∋ f ) ∧ (infinite ∋ n)) → HOD
-↑n f n lt = 3→Hω2 ( ω→2f f (proj1 lt) 3↑ (ω→nat n (proj2 lt) ))
+-- postulate 
+--    ω→2f-iso : (X : HOD) → ( lt : ω→2 ∋ X ) → fω→2 ( ω→2f X lt )  =h= X
+--    fω→2-iso : (f : Nat → Two) → ω→2f ( fω→2 f ) (ω2∋f f) ≡ f
 
 record CountableOrdinal : Set (suc (suc n)) where
    field

--- a/ordinal.agda	Sat Dec 19 21:58:32 2020 +0900
+++ b/ordinal.agda	Sun Dec 20 12:37:07 2020 +0900
@@ -6,6 +6,7 @@
 open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ ) 
 open import Data.Empty
 open import Relation.Binary.PropositionalEquality
+open import Relation.Binary.Definitions
 open import Data.Nat.Properties 
 open import Relation.Nullary
 open import Relation.Binary.Core
@@ -109,7 +110,7 @@
       osuc-≡< {n} {record { lv = la ; ord = oa }} {record { lv = la ; ord = ox }} (case2 lt )
 ... | case1 refl = case1 refl
 ... | case2 (case2 x) = case2 (case2( s< x) )
-... | case2 (case1 x) = ⊥-elim (¬a≤a  x) where
+... | case2 (case1 x) = ⊥-elim (¬a≤a  x) 
 
 osuc-< : {n : Level} { x y : Ordinal {n} } → y o< osuc x  → x o< y → ⊥
 osuc-< {n} {x} {y} y<ox x<y with osuc-≡< y<ox
@@ -199,6 +200,26 @@
       lemma y lt | case1 refl = proj1 ( TransFinite1 lx ox ) 
       lemma y lt | case2 lt1 = proj2 ( TransFinite1 lx ox ) y lt1
 
+--  record CountableOrdinal {n : Level} : Set (suc (suc n)) where
+--     field
+--         ctl→ : Nat → Ordinal {suc n}
+--         ctl← : Ordinal → Nat
+--         ctl-iso→ : { x : Ordinal } → ctl→ (ctl← x ) ≡ x
+--         ctl-iso← : { x : Nat }  → ctl← (ctl→ x ) ≡ x
+--  
+--  is-C-Ordinal : {n : Level} → CountableOrdinal {n}
+--  is-C-Ordinal {n} = record {
+--         ctl→ = {!!} 
+--      ;  ctl← = λ x → TransFinite {n} (λ lx lt → Zero ) ctl01 x
+--      ;  ctl-iso→ = {!!}
+--      ;  ctl-iso← = {!!}
+--    } where
+--        ctl01 : (lx : Nat) (x : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x) → Nat) → Nat
+--        ctl01 Zero (Φ Zero) prev = Zero 
+--        ctl01 Zero (OSuc Zero x) prev = Suc ( prev (ordinal Zero x) (ordtrans <-osuc <-osuc )) 
+--        ctl01 (Suc lx) (Φ (Suc lx)) prev = Suc ( prev (ordinal lx {!!}) {!!})
+--        ctl01 (Suc lx) (OSuc (Suc lx) x) prev = Suc ( prev (ordinal (Suc lx) x) (ordtrans <-osuc <-osuc ))
+
 open import Ordinals 
 
 C-Ordinal : {n : Level} →  Ordinals {suc n}