# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1563847704 -32400
# Node ID ac872f6b86927387912da10397cc50c458283a76
# Parent  914cc522c53a4b279bb12befd7fbf7afcfa93597
add Todo

diff -r 914cc522c53a -r ac872f6b8692 OD.agda
--- a/OD.agda	Mon Jul 22 18:49:38 2019 +0900
+++ b/OD.agda	Tue Jul 23 11:08:24 2019 +0900
@@ -70,12 +70,11 @@
   -- contra-position of mimimulity of supermum required in Power Set Axiom
   -- sup-x  : {n : Level } → ( Ordinal {n} → Ordinal {n}) →  Ordinal {n}
   -- sup-lb : {n : Level } → { ψ : Ordinal {n} →  Ordinal {n}} → {z : Ordinal {n}}  →  z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
-  -- sup-lb : {n : Level } → ( ψ : Ordinal {n} →  Ordinal {n}) → ( ∀ {x : Ordinal {n}} →  ψx  o<  z ) →  z o< osuc ( sup-o ψ ) 
   -- mimimul and x∋minimul is an Axiom of choice
   minimul : {n : Level } → (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n} 
   -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox  ( minimum of x )
   x∋minimul : {n : Level } → (x : OD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimul x ne ) )
-  -- 
+  -- minimulity (may proved by ε-induction )
   minimul-1 : {n : Level } → (x : OD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → (y : OD {suc n}) → ¬ ( def (minimul x ne) (od→ord y)) ∧ (def x (od→ord  y) )
 
 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n
@@ -102,8 +101,8 @@
     lemma : od→ord (ψ (ord→od (od→ord x))) o< sup-o (λ x → od→ord (ψ (ord→od x)))
     lemma = subst₂ (λ j k → j o< k ) refl diso (o<-subst sup-o< refl (sym diso)  )
 
-otrans : {n : Level} {a x : Ordinal {n} } → def (Ord a) x → { y : Ordinal {n} } → y o< x → def (Ord a) y
-otrans {n} {a} {x} x<a {y} y<x = ordtrans y<x x<a
+otrans : {n : Level} {a x y : Ordinal {n} } → def (Ord a) x → def (Ord x) y → def (Ord a) y
+otrans x<a y<x = ordtrans y<x x<a
 
 ∅3 : {n : Level} →  { x : Ordinal {n}}  → ( ∀(y : Ordinal {n}) → ¬ (y o< x ) ) → x ≡ o∅ {n}
 ∅3 {n} {x} = TransFinite {n} c2 c3 x where
@@ -159,11 +158,6 @@
 c≤-refl : {n : Level} →  ( x : OD {n} ) → x c≤ x
 c≤-refl x = case1 refl
 
-∋→o< : {n : Level} →  { a x : OD {suc n} } → a ∋ x → od→ord x o< od→ord a
-∋→o< {n} {a} {x} lt = t where
-         t : (od→ord x) o< (od→ord a)
-         t = c<→o< {suc n} {x} {a} lt 
-
 o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n}
 o∅≡od∅ {n} = ==→o≡ lemma where
      lemma0 :  {x : Ordinal} → def (ord→od o∅) x → def od∅ x
@@ -177,12 +171,6 @@
 ord-od∅ : {n : Level} → od→ord (od∅ {suc n}) ≡ o∅ {suc n}
 ord-od∅ {n} = sym ( subst (λ k → k ≡  od→ord (od∅ {suc n}) ) diso (cong ( λ k → od→ord k ) o∅≡od∅ ) )
 
-o<→¬c> : {n : Level} →  { x y : OD {n} } → (od→ord x ) o< ( od→ord y) →  ¬ (y c< x )
-o<→¬c> {n} {x} {y} olt clt = o<> olt (c<→o< clt ) where
-
-o≡→¬c< : {n : Level} →  { x y : OD {n} } →  (od→ord x ) ≡ ( od→ord y) →   ¬ x c< y
-o≡→¬c< {n} {x} {y} oeq lt  = o<¬≡  (orefl oeq ) (c<→o< lt) 
-
 ∅0 : {n : Level} →  record { def = λ x →  Lift n ⊥ } == od∅ {n} 
 eq→ ∅0 {w} (lift ())
 eq← ∅0 {w} (case1 ())
@@ -311,8 +299,6 @@
          empty x (case1 ())
          empty x (case2 ())
 
-         ord-⊆ : ( t x : OD {suc n} ) → _⊆_ t (Ord (od→ord t )) {x}
-         ord-⊆ t x lt = c<→o< lt
          o<→c< :  {x y : Ordinal {suc n}} {z : OD {suc n}}→ x o< y → _⊆_  (Ord x) (Ord y) {z}
          o<→c< lt lt1 = ordtrans lt1 lt
          
diff -r 914cc522c53a -r ac872f6b8692 Todo
--- a/Todo	Mon Jul 22 18:49:38 2019 +0900
+++ b/Todo	Tue Jul 23 11:08:24 2019 +0900
@@ -1,3 +1,13 @@
+Tue Jul 23 11:02:50 JST 2019
+
+    define cardinals 
+    prove CH in OD→ZF
+    define Ultra filter
+    define L M : ZF ZFSet = M is an OD
+    define L N : ZF ZFSet = N = G M (G is a generic fitler on M )
+    prove ¬ CH on L N
+    prove no choice function on L N
+
 Mon Jul  8 19:43:37 JST 2019
 
     ordinal-definable.agda assumes all ZF Set are ordinals, that it too restrictive