Mercurial > hg > Members > kono > Proof > ZF-in-agda

changeset 105:ec6235ce0215

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
power set
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 16 Jun 2019 11:37:00 +0900
parents d92411bed18c
children c31ac67e9ecb
files ordinal-definable.agda
diffstat 1 files changed, 70 insertions(+), 151 deletions(-) [+]
line wrap: on
line diff
--- a/ordinal-definable.agda	Sun Jun 16 02:06:09 2019 +0900
+++ b/ordinal-definable.agda	Sun Jun 16 11:37:00 2019 +0900
@@ -43,7 +43,7 @@
 eq-trans x=y y=z = record { eq→ = λ t → eq→ y=z ( eq→ x=y  t) ; eq← = λ t → eq← x=y ( eq← y=z t) }
 
 od∅ : {n : Level} → OD {n} 
-od∅ {n} = record { def = λ _ → Lift n ⊥ }
+od∅ {n} = record { def = λ x → x o< o∅ }
 
 postulate      
   -- OD can be iso to a subset of Ordinal ( by means of Godel Set )
@@ -66,11 +66,11 @@
 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n
 _∋_ {n} a x  = def a ( od→ord x )
 
-Ord : { n : Level } → ( a : Ordinal {suc n} ) → OD {suc n}
+Ord : { n : Level } → ( a : Ordinal {n} ) → OD {n}
 Ord {n} a = record { def = λ y → y o< a } 
 
 _c<_ : { n : Level } → ( x a : Ordinal {n} ) → Set n
-x c< a = Ord a ∋ Ord x
+_c<_ {n} x  a = Ord {n} a ∋ Ord x
 
 c<→o< : { n : Level } → { x a : OD {n} } → record { def = λ y → y o< od→ord a } ∋ x → od→ord x o< od→ord a
 c<→o< lt = lt
@@ -78,39 +78,39 @@
 o<→c< : { n : Level } → { x a : OD {n} } → od→ord x o< od→ord a → record { def = λ y → y o< od→ord a } ∋ x 
 o<→c< lt = lt
 
-==→o≡' : {n : Level} →  { x y : Ordinal {suc n} } →  Ord x == Ord y →  x ≡ y 
-==→o≡' {n} {x} {y} eq with trio< {n} x y
-==→o≡' {n} {x} {y} eq | tri< a ¬b ¬c with eq← eq {x} a
+==→o≡ : {n : Level} →  { x y : Ordinal {suc n} } →  Ord x == Ord y →  x ≡ y 
+==→o≡ {n} {x} {y} eq with trio< {n} x y
+==→o≡ {n} {x} {y} eq | tri< a ¬b ¬c with eq← eq {x} a
 ... | t = ⊥-elim ( o<¬≡ x x refl t )
-==→o≡' {n} {x} {y} eq | tri≈ ¬a refl ¬c = refl
-==→o≡' {n} {x} {y} eq | tri> ¬a ¬b c  with eq→ eq {y} c
+==→o≡ {n} {x} {y} eq | tri≈ ¬a refl ¬c = refl
+==→o≡ {n} {x} {y} eq | tri> ¬a ¬b c  with eq→ eq {y} c
 ... | t = ⊥-elim ( o<¬≡ y y refl t )
 
-∅∨ : { n : Level } → { x y : Ordinal {suc n} } → ( Ord {n} x == Ord y ) ∨ ( ¬ ( Ord x == Ord y ) )
+∅∨ : { n : Level } → { x y : Ordinal {suc n} } → ( Ord {suc n} x == Ord y ) ∨ ( ¬ ( Ord x == Ord y ) )
 ∅∨ {n} {x} {y} with trio< x y
-∅∨ {n} {x} {y} | tri< a ¬b ¬c = case2 ( λ eq → ¬b ( ==→o≡' eq ) )
+∅∨ {n} {x} {y} | tri< a ¬b ¬c = case2 ( λ eq → ¬b ( ==→o≡ eq ) )
 ∅∨ {n} {x} {y} | tri≈ ¬a refl ¬c = case1 ( record { eq→ =  id ; eq← = id } ) 
-∅∨ {n} {x} {y} | tri> ¬a ¬b c = case2 ( λ eq → ¬b ( ==→o≡' eq ) )
+∅∨ {n} {x} {y} | tri> ¬a ¬b c = case2 ( λ eq → ¬b ( ==→o≡ eq ) )
 
-¬x∋x' : { n : Level } → { x  : Ordinal {n} } → ¬ ( record { def = λ y → y o< x } ∋ record { def = λ y → y o< x } )
-¬x∋x' {n} {record { lv = Zero ; ord = ord }} (case1 ())
-¬x∋x' {n} {record { lv = Suc lx ; ord = Φ .(Suc lx) }} (case1 (s≤s x)) = ¬x∋x' {n} {record { lv = lx ; ord = Φ lx }} (case1 {!!}) 
-¬x∋x' {n} {record { lv = Suc lx ; ord = OSuc (Suc lx) ox }} (case1 (s≤s x)) = ¬x∋x' {n} {record { lv = Suc lx ; ord = ox}}  (case1 {!!}) 
-¬x∋x' {n} {record { lv = lv ; ord = Φ (lv) }} (case2 ())
-¬x∋x' {n} {record { lv = lv ; ord = OSuc (lv) ox }} (case2 x) = 
-   ¬x∋x' {n} {record { lv = lv ; ord = ox }} (case2 {!!}) 
+-- ¬x∋x' : { n : Level } → { x  : Ordinal {n} } → ¬ ( record { def = λ y → y o< x } ∋ record { def = λ y → y o< x } )
+-- ¬x∋x' {n} {record { lv = Zero ; ord = ord }} (case1 ())
+-- ¬x∋x' {n} {record { lv = Suc lx ; ord = Φ .(Suc lx) }} (case1 (s≤s x)) = ¬x∋x' {n} {record { lv = lx ; ord = Φ lx }} (case1 {!!}) 
+-- ¬x∋x' {n} {record { lv = Suc lx ; ord = OSuc (Suc lx) ox }} (case1 (s≤s x)) = ¬x∋x' {n} {record { lv = Suc lx ; ord = ox}}  (case1 {!!}) 
+-- ¬x∋x' {n} {record { lv = lv ; ord = Φ (lv) }} (case2 ())
+-- ¬x∋x' {n} {record { lv = lv ; ord = OSuc (lv) ox }} (case2 x) = 
+--    ¬x∋x' {n} {record { lv = lv ; ord = ox }} (case2 {!!}) 
 
-¬x∋x : { n : Level } → { x  : OD {n} } → ¬ x ∋ x
-¬x∋x = {!!}
+-- ¬x∋x : { n : Level } → { x  : OD {n} } → ¬ x ∋ x
+-- ¬x∋x = {!!}
 
 oc-lemma : { n : Level } → { x : OD {n} } → { oa : Ordinal {n} } → def (record { def = λ y → y o< oa }) oa → ⊥
 oc-lemma {n} {x} {oa} lt = o<¬≡ oa oa refl lt
 
-oc-lemma1 : { n : Level } → { x : OD {n} } → { oa : Ordinal {n} } → od→ord (record { def = λ y → y o< oa }) o< oa → ⊥
-oc-lemma1 {n} {x} {oa} lt = ¬x∋x' {n}   lt -- lt : def (record { def = λ y → y o< oa }) (record { def = λ y → y o< oa })
+-- oc-lemma1 : { n : Level } → { x : OD {n} } → { oa : Ordinal {n} } → od→ord (record { def = λ y → y o< oa }) o< oa → ⊥
+-- oc-lemma1 {n} {x} {oa} lt = ¬x∋x' {n}   lt -- lt : def (record { def = λ y → y o< oa }) (record { def = λ y → y o< oa })
 
-oc-lemma2 : { n : Level } → { x a : OD {n} } → { oa : Ordinal {n} } → oa o< od→ord (record { def = λ y → y o< oa }) → ⊥
-oc-lemma2 {n} {x} {oa} lt = {!!} 
+-- this one cannot be proved because if we have this OD and Ordinal has one to one corespondence
+-- oc-lemma2 : { n : Level } → { x a : OD {n} } → { oa : Ordinal {n} } → oa o< od→ord (record { def = λ y → y o< oa }) → ⊥
 
 _c≤_ : {n : Level} →  OD {n} →  OD {n} → Set (suc n)
 a c≤ b  = (a ≡ b)  ∨ ( b ∋ a )
@@ -125,22 +125,28 @@
 def-o< x<y = x<y
 
 sup-od : {n : Level } → ( OD {n} → OD {n}) →  OD {n}
-sup-od ψ = ord→od ( sup-o ( λ x → od→ord (ψ (ord→od x ))) )
+sup-od ψ = record { def = λ y → y o< ( sup-o ( λ x → od→ord (ψ (ord→od x ))) ) }
 
 sup-c< : {n : Level } → ( ψ : OD {n} →  OD {n}) → ∀ {x : OD {n}} → def ( sup-od ψ ) (od→ord ( ψ x ))
-sup-c< {n} ψ {x} = def-subst {n} {_} {_} {sup-od ψ} {od→ord ( ψ x )}
-        {!!} refl (cong ( λ k → od→ord (ψ k) ) oiso)
+sup-c< {n} ψ {x} = def-subst {n} {_} {_} {record { def = λ y → y o< ( sup-o ( λ x → od→ord (ψ (ord→od x ))) ) }} {od→ord ( ψ x )}
+        lemma refl (cong ( λ k → od→ord (ψ k) ) oiso) where
+    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<→c< (o<-subst sup-o< refl (sym diso) ) )
 
-od∅' : {n : Level} →  OD {n}
-od∅' = record { def = λ x → x o< o∅ }
-
-∅0 : {n : Level} →  od∅ {suc n} == record { def = λ x → x o< o∅ }
+∅0 : {n : Level} →  record { def = λ x →  Lift n ⊥ } == od∅ {n} 
 eq→ ∅0 {w} (lift ())
 eq← ∅0 {w} (case1 ())
 eq← ∅0 {w} (case2 ())
 
 ∅1 : {n : Level} →  ( x : Ordinal {n} )  → ¬ ( x c< o∅ {n} )
-∅1 {n} x lt = {!!}
+∅1 {n} record { lv = Zero ; ord = (Φ .0) } (case1 ())
+∅1 {n} record { lv = Zero ; ord = (Φ .0) } (case2 ())
+∅1 {n} record { lv = Zero ; ord = (OSuc .0 ox) } (case1 ())
+∅1 {n} record { lv = Zero ; ord = (OSuc .0 ox) } (case2 ())
+∅1 {n} record { lv = (Suc lx) ; ord = (Φ .(Suc lx)) } (case1 ())
+∅1 {n} record { lv = (Suc lx) ; ord = (Φ .(Suc lx)) } (case2 ())
+∅1 {n} record { lv = (Suc lx) ; ord = (OSuc .(Suc lx) ox) } (case1 ())
+∅1 {n} record { lv = (Suc lx) ; ord = (OSuc .(Suc lx) ox) } (case2 ())
 
 ∅3 : {n : Level} →  { x : Ordinal {n}}  → ( ∀(y : Ordinal {n}) → ¬ (y o< x ) ) → x ≡ o∅ {n}
 ∅3 {n} {x} = TransFinite {n} c2 c3 x where
@@ -196,89 +202,20 @@
 c≤-refl : {n : Level} →  ( x : OD {n} ) → x c≤ x
 c≤-refl x = case1 refl
 
-o<→o> : {n : Level} →  { x y : OD {n} } →  (x == y) → (od→ord x ) o< ( od→ord y) → ⊥
-o<→o> {n} {x} {y} record { eq→ = xy ; eq← = yx } (case1 lt) with
-     yx (def-subst {n} {ord→od (od→ord y)} {od→ord x} {!!} oiso refl )
-... | oyx with o<¬≡ (od→ord x) (od→ord x) refl {!!}
-... | ()
-o<→o> {n} {x} {y} record { eq→ = xy ; eq← = yx } (case2 lt) with
-     yx (def-subst {n} {ord→od (od→ord y)} {od→ord x} {!!} oiso refl )
-... | oyx with o<¬≡ (od→ord x) (od→ord x) refl {!!}
-... | ()
-
-==→o≡ : {n : Level} →  { x y : Ordinal {suc n} } → ord→od x == ord→od y →  x ≡ y 
-==→o≡ {n} {x} {y} eq with trio< {n} x y
-==→o≡ {n} {x} {y} eq | tri< a ¬b ¬c = ⊥-elim ( o<→o> eq (o<-subst a (sym ord-iso) (sym ord-iso )))
-==→o≡ {n} {x} {y} eq | tri≈ ¬a b ¬c = b
-==→o≡ {n} {x} {y} eq | tri> ¬a ¬b c = ⊥-elim ( o<→o> (eq-sym eq) (o<-subst c (sym ord-iso) (sym ord-iso )))
-
-≡-def : {n : Level} →  { x : Ordinal {suc n} } → x ≡ od→ord (record { def = λ z → z o< x } )
-≡-def {n} {x} = ==→o≡ {n} (subst (λ k → ord→od x == k ) (sym oiso) lemma ) where
-    lemma :  ord→od x == record { def = λ z → z o< x }
-    eq→ lemma {w} lt = {!!}
-        -- ?subst₂ (λ k j → k o< j ) diso refl (subst (λ k → (od→ord ( ord→od w)) o< k ) diso t ) where 
-        --t : (od→ord ( ord→od w)) o< (od→ord (ord→od x))
-        --t = o<-subst lt ? ?
-    eq← lemma {w} lt = def-subst {suc n} {_} {_} {ord→od x} {w} {!!} refl refl
-
-od≡-def : {n : Level} →  { x : Ordinal {suc n} } → ord→od x ≡ record { def = λ z → z o< x } 
-od≡-def {n} {x} = subst (λ k  → ord→od x ≡ k ) oiso (cong ( λ k → ord→od k ) (≡-def {n} {x} ))
-
-==→o≡1 : {n : Level} →  { x y : OD {suc n} } → x == y →  od→ord x ≡ od→ord y 
-==→o≡1 eq = ==→o≡ (subst₂ (λ k j → k == j ) (sym oiso) (sym oiso) eq )
-
-==-def-l : {n : Level } {x y : Ordinal {suc n} } { z : OD {suc n} }→ (ord→od x == ord→od y) → def z x → def z y
-==-def-l {n} {x} {y} {z} eq z>x = subst ( λ k → def z k ) (==→o≡ eq) z>x
-
-==-def-r : {n : Level } {x y : OD {suc n} } { z : Ordinal {suc n} }→ (x == y) → def x z → def y z
-==-def-r {n} {x} {y} {z} eq z>x = subst (λ k → def k z ) (subst₂ (λ j k → j ≡ k ) oiso oiso (cong (λ k → ord→od k) (==→o≡1 eq))) z>x  
+o<→o> : {n : Level} →  { x y : Ordinal {suc n} } →  (Ord x == Ord y) → x o< y → ⊥
+o<→o> {n} {x} {y} eq lt with   ==→o≡ {n} eq 
+... | refl = o<¬≡ _ _ refl lt
 
-∋→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 = {!!}
 
-o<∋→ : {n : Level} →  { a x : OD {suc n} } → od→ord x o< od→ord a → a ∋ x 
-o<∋→ {n} {a} {x} lt = subst₂ (λ k j → def k j ) oiso refl t  where
-         t : def (ord→od (od→ord a)) (od→ord x)
-         t = {!!}
-
-o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅' {suc n}
-o∅≡od∅ {n} with trio< {n} (o∅ {suc n}) (od→ord (od∅' {suc n} ))
-o∅≡od∅ {n} | tri< a ¬b ¬c = ⊥-elim (lemma a) where
-    lemma :  o∅ {suc n } o< (od→ord (od∅' {suc n} )) → ⊥
-    lemma lt with  def-subst {suc n} {_} {_} {_} {_} ( o<→c< ( o<-subst lt (sym diso) refl ) ) refl diso
-    lemma lt | t = {!!}
-o∅≡od∅ {n} | tri≈ ¬a b ¬c = trans (cong (λ k → ord→od k ) b ) oiso
-o∅≡od∅ {n} | tri> ¬a ¬b c = ⊥-elim (¬x<0 c)
-
-o<→¬== : {n : Level} →  { x y : OD {n} } → (od→ord x ) o< ( od→ord y) →  ¬ (x == y )
-o<→¬== {n} {x} {y} lt eq = o<→o> eq lt
-
-o<→¬c> : {n : Level} →  { x y : Ordinal {n} } → x o< y →  ¬ (y c< x )
-o<→¬c> {n} {x} {y} olt clt = o<> olt {!!} where
-
-o≡→¬c< : {n : Level} →  { x y : Ordinal {n} } →  x ≡ y →   ¬ x c< y
-o≡→¬c< {n} {x} {y} oeq lt  = o<¬≡ x y {!!} {!!}  
-
-tri-c< : {n : Level} →  Trichotomous _≡_ (_c<_ {suc n})
-tri-c< {n} x y with trio< {n} x y 
-tri-c< {n} x y | tri< a ¬b ¬c = tri< (def-subst {!!} oiso refl) {!!} ( o<→¬c> a )
-tri-c< {n} x y | tri≈ ¬a b ¬c = tri≈ (o≡→¬c< b) {!!} (o≡→¬c< (sym b))
-tri-c< {n} x y | tri> ¬a ¬b c = tri>  ( o<→¬c> c) (λ eq → {!!} ) (def-subst {!!} oiso refl)
-
-c<> : {n : Level } { x y : Ordinal {suc n}} → x c<  y  → y c< x  →  ⊥
-c<> {n} {x} {y} x<y y<x with tri-c< x y
-c<> {n} {x} {y} x<y y<x | tri< a ¬b ¬c = ¬c y<x
-c<> {n} {x} {y} x<y y<x | tri≈ ¬a b ¬c = o<→o> {!!} {!!}
-c<> {n} {x} {y} x<y y<x | tri> ¬a ¬b c = ¬a x<y
+o<→¬== : {n : Level} →  { x y : Ordinal {suc n} } → x o< y →  ¬ (Ord x == Ord y )
+o<→¬== {n} {x} {y} lt eq = o<→o> {n} eq lt
 
 ∅< : {n : Level} →  { x y : OD {n} } → def x (od→ord y ) → ¬ (  x  == od∅ {n} )
-∅< {n} {x} {y} d eq with eq→ eq d
+∅< {n} {x} {y} d eq with eq→ (eq-trans eq (eq-sym ∅0) ) d
 ∅< {n} {x} {y} d eq | lift ()
        
-∅6 : {n : Level} →  { x : OD {suc n} }  → ¬ ( x ∋ x )    --  no Russel paradox
-∅6 {n} {x} x∋x = c<> {n} {{!!}} {{!!}} {!!} {!!}
+-- ∅6 : {n : Level} →  { x : OD {suc n} }  → ¬ ( x ∋ x )    --  no Russel paradox
+-- ∅6 {n} {x} x∋x = c<> {n} {{!!}} {{!!}} {!!} {!!}
 
 def-iso : {n : Level} {A B : OD {n}} {x y : Ordinal {n}} → x ≡ y  → (def A y → def B y)  → def A x → def B x
 def-iso refl t = t
@@ -290,15 +227,14 @@
 
 open _∧_
 
-¬∅=→∅∈ :  {n : Level} →  { x : OD {suc n} } → ¬ (  x  == od∅ {suc n} ) → x ∋ od∅ {suc n} 
-¬∅=→∅∈  {n} {x} ne = def-subst (lemma (od→ord x) (subst (λ k → ¬ (k == od∅ {suc n} )) (sym oiso) ne )) oiso refl where
-     lemma : (ox : Ordinal {suc n}) →  ¬ (ord→od  ox  == od∅ {suc n} ) → ord→od ox ∋ od∅ {suc n}
-     lemma ox ne with is-o∅ ox
-     lemma ox ne | yes refl with ne ( ord→== lemma1 ) where
-         lemma1 : od→ord (ord→od o∅) ≡ od→ord od∅
-         lemma1 = cong ( λ k → od→ord k ) {!!}
-     lemma o∅ ne | yes refl | ()
-     lemma ox ne | no ¬p = subst ( λ k → def (ord→od ox) (od→ord k) ) {!!} {!!}
+ord-od∅ :  {n : Level} → o∅ {n} ≡ od→ord (Ord (o∅ {n}))
+ord-od∅ = ==→o≡  {!!}
+
+
+¬∅=→∅∈ :  {n : Level} →  { x : Ordinal {suc n} } → ¬ (  Ord x  == od∅ {suc n} ) → Ord x ∋ od∅ {suc n} 
+¬∅=→∅∈  {n} {x} ne with is-o∅ x
+¬∅=→∅∈ {n} {x} ne | yes refl = ⊥-elim ( ne (eq-sym (eq-refl) ))
+¬∅=→∅∈ {n} {x} ne | no ¬p = o<-subst (∅5 ¬p) ord-od∅ refl
 
 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 -- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality (suc n) (suc (suc n))
@@ -321,6 +257,9 @@
 L {n}  record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α )
        record { def = λ y → osuc y o< (od→ord (L {n}  (record { lv = lx ; ord = Φ lx }) )) }
 
+omega :  {n : Level} →  Ordinal {n}
+omega = record { lv = Suc Zero ; ord = Φ 1 }
+
 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
 OD→ZF {n}  = record { 
     ZFSet = OD {suc n}
@@ -332,7 +271,7 @@
     ; Power = Power
     ; Select = Select
     ; Replace = Replace
-    ; infinite = ord→od ( record { lv = Suc Zero ; ord = Φ 1 } )
+    ; infinite = Ord omega
     ; isZF = isZF 
  } where
     Replace : OD {suc n} → (OD {suc n} → OD {suc n} ) → OD {suc n}
@@ -360,7 +299,7 @@
     infixr  200 _∈_
     -- infixr  230 _∩_ _∪_
     infixr  220 _⊆_
-    isZF : IsZF (OD {suc n})  _∋_  _==_ od∅ _,_ Union Power Select Replace (ord→od ( record { lv = Suc Zero ; ord = Φ 1} ))
+    isZF : IsZF (OD {suc n})  _∋_  _==_ od∅ _,_ Union Power Select Replace (Ord omega)
     isZF = record {
            isEquivalence  = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
        ;   pair  = pair
@@ -383,7 +322,8 @@
          proj1 (pair A B ) = omax-x {n} (od→ord A) (od→ord B)
          proj2 (pair A B ) = omax-y {n} (od→ord A) (od→ord B)
          empty : (x : OD {suc n} ) → ¬  (od∅ ∋ x)
-         empty x ()
+         empty x (case1 ())
+         empty x (case2 ())
          ---
          --- ZFSubset A x =  record { def = λ y → def A y ∧  def x y }                   subset of A
          --- Power X = ord→od ( sup-o ( λ x → od→ord ( ZFSubset A (ord→od x )) ) )       Power X is a sup of all subset of A
@@ -412,7 +352,7 @@
               eq← lemma-eq {z} w = record { proj2 = w  ;
                  proj1 = def-subst {suc n} {_} {_} {A} {z} ( t→A (def-subst {suc n} {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso  }
               lemma1 : od→ord (ZFSubset A (ord→od (od→ord t))) ≡ od→ord t
-              lemma1 = subst (λ k → od→ord (ZFSubset A k) ≡ od→ord t ) (sym oiso) (==→o≡1 (lemma-eq))
+              lemma1 = subst (λ k → od→ord (ZFSubset A k) ≡ od→ord t ) (sym oiso) {!!}
               lemma :  od→ord (ZFSubset A (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset A (ord→od x)))
               lemma = sup-o<   
          union-lemma-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → csuc z ∋ z
@@ -443,46 +383,25 @@
          regularity :  (x : OD) (not : ¬ (x == od∅)) →
             (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
          proj1 (regularity x not ) = x∋minimul x not
-         proj2 (regularity x not ) = record { eq→ = reg ; eq← = λ () } where
+         proj2 (regularity x not ) = record { eq→ = reg ; eq← = {!!} } where
             reg : {y : Ordinal} → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) y → def od∅ y
             reg {y} t  with minimul-1 x not (ord→od y) (proj2 t ) 
-            ... | t1 = lift t1
+            ... | t1 = {!!}
          extensionality : {A B : OD {suc n}} → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
          eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d  
          eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d  
-         xx-union : {x  : OD {suc n}} → (x , x) ≡ record { def = λ z → z o< osuc (od→ord x) }
-         xx-union {x} = cong ( λ k → record { def = λ z → z o< k } ) (omxx (od→ord x))
-         xxx-union : {x  : OD {suc n}} → (x , (x , x)) ≡ record { def = λ z → z o< osuc (osuc (od→ord x))}
-         xxx-union {x} = cong ( λ k → record { def = λ z → z o< k } ) lemma where
-             lemma1 : {x  : OD {suc n}} → od→ord x o< od→ord (x , x)
-             lemma1 {x} = {!!}
-             lemma2 : {x  : OD {suc n}} → od→ord (x , x) ≡ osuc (od→ord x)
-             lemma2 = trans ( cong ( λ k →  od→ord k ) xx-union ) (sym ≡-def)
-             lemma : {x  : OD {suc n}} → omax (od→ord x) (od→ord (x , x)) ≡ osuc (osuc (od→ord x))
-             lemma {x} = trans ( sym ( omax< (od→ord x) (od→ord (x , x)) lemma1 ) ) ( cong ( λ k → osuc k ) lemma2 )
-         uxxx-union : {x  : OD {suc n}} → Union (x , (x , x)) ≡ record { def = λ z → osuc z o< osuc (osuc (od→ord x)) }
-         uxxx-union {x} = cong ( λ k → record { def = λ z → osuc z o< k } ) lemma where
-             lemma : od→ord (x , (x , x)) ≡ osuc (osuc (od→ord x))
-             lemma = trans ( cong ( λ k → od→ord k ) xxx-union ) (sym ≡-def )
-         uxxx-2 : {x  : OD {suc n}} → record { def = λ z → osuc z o< osuc (osuc (od→ord x)) } == record { def = λ z → z o< osuc (od→ord x) }
-         eq→ ( uxxx-2 {x} ) {m} lt = proj1 (osuc2 m (od→ord x)) lt
-         eq← ( uxxx-2 {x} ) {m} lt = proj2 (osuc2 m (od→ord x)) lt
-         uxxx-ord : {x  : OD {suc n}} → od→ord (Union (x , (x , x))) ≡ osuc (od→ord x)
-         uxxx-ord {x} = trans (cong (λ k →  od→ord k ) uxxx-union) (==→o≡ (subst₂ (λ j k → j == k ) (sym oiso) (sym od≡-def ) uxxx-2 )) 
-         omega = record { lv = Suc Zero ; ord = Φ 1 }
          infinite : OD {suc n}
-         infinite = ord→od ( omega )
-         infinity∅ : ord→od ( omega ) ∋ od∅ {suc n}
-         infinity∅ = def-subst {suc n} {_} {o∅} {infinite} {od→ord od∅}
-              {!!}  refl (subst ( λ k → ( k ≡ od→ord od∅ )) diso (cong (λ k →  od→ord k) {!!} ))
+         infinite = Ord omega 
+         infinity∅ : Ord omega  ∋ od∅ {suc n}
+         infinity∅ = {!!}
          infinite∋x : (x : OD) → infinite ∋ x → od→ord x o< omega
          infinite∋x x lt = subst (λ k → od→ord x o< k ) diso t where
               t  : od→ord x o< od→ord (ord→od (omega))
-              t  = ∋→o< {n} {infinite} {x} lt
+              t  = {!!}
          infinite∋uxxx : (x : OD) → osuc (od→ord x) o< omega → infinite ∋ Union (x , (x , x ))
-         infinite∋uxxx x lt = o<∋→ t where
+         infinite∋uxxx x lt = {!!} where
               t  :  od→ord (Union (x , (x , x))) o< od→ord (ord→od (omega))
-              t  = subst (λ k →  od→ord (Union (x , (x , x))) o< k ) (sym diso ) ( subst ( λ k → k o< omega ) ( sym  (uxxx-ord {x} ) ) lt ) 
+              t  = subst (λ k →  od→ord (Union (x , (x , x))) o< k ) (sym diso ) ( subst ( λ k → k o< omega ) {!!} lt ) 
          infinity : (x : OD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
          infinity x lt = infinite∋uxxx x ( lemma (od→ord x) (infinite∋x x lt ))   where
               lemma : (ox : Ordinal {suc n} ) → ox o< omega → osuc ox o< omega