# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1558936845 -32400
# Node ID 83b13f1f4f42273e1f7e8d49ff7585c331755037
# Parent  7cb32d22528c85cc837cce5ca96b4f3bddd6d705
...

diff -r 7cb32d22528c -r 83b13f1f4f42 ordinal-definable.agda
--- a/ordinal-definable.agda	Sat May 25 21:31:07 2019 +0900
+++ b/ordinal-definable.agda	Mon May 27 15:00:45 2019 +0900
@@ -140,21 +140,91 @@
 ord-iso : {n : Level} {y : Ordinal {n} } → record { lv = lv (od→ord (ord→od y)) ; ord = ord (od→ord (ord→od y)) } ≡ record { lv = lv y ; ord = ord y }
 ord-iso = cong ( λ k → record { lv = lv k ; ord = ord k } ) diso
 
-∅7 : {n : Level} →  ( x : OD {n} ) → od→ord x ≡ o∅ {n} →  x  == od∅ {n}
-∅7 {n} x eq = record { eq→ = e1 eq ; eq← = e2 } where
+-- avoiding lv != Zero error
+orefl : {n : Level} →  { x : OD {n} } → { y : Ordinal {n} } → od→ord x ≡ y → od→ord x ≡ y
+orefl refl = refl
+
+==-iso : {n : Level} →  { x y : OD {n} } → ord→od (od→ord x) == ord→od (od→ord y)  →  x == y
+==-iso {n} {x} {y} eq = record {
+      eq→ = λ d →  lemma ( eq→  eq (def-subst d (sym oiso) refl )) ;
+      eq← = λ d →  lemma ( eq←  eq (def-subst d (sym oiso) refl ))  }
+        where
+           lemma : {x : OD {n} } {z : Ordinal {n}} → def (ord→od (od→ord x)) z → def x z
+           lemma {x} {z} d = def-subst d oiso refl
+
+ord→== : {n : Level} →  { x y : OD {n} } → od→ord x ≡  od→ord y →  x == y
+ord→== {n} {x} {y} eq = ==-iso (lemma (od→ord x) (od→ord y) (orefl eq)) where
+   lemma : ( ox oy : Ordinal {n} ) → ox ≡ oy →  (ord→od ox) == (ord→od oy)
+   lemma ox ox  refl = eq-refl
+
+o≡→== : {n : Level} →  { x y : Ordinal {n} } → x ≡  y →  ord→od x == ord→od y
+o≡→== {n} {x} {.x} refl = eq-refl
+
+∅7 : {n : Level} →  { x : OD {n} } → od→ord x ≡ o∅ {n} →  x  == od∅ {n}
+∅7 {n} {x} eq = record { eq→ = e1 (orefl eq) ; eq← = e2 } where
    e2 : {y : Ordinal {n}} → def od∅ y → def x y 
    e2 {y} (lift ())
    e1 : {ox y : Ordinal {n}} → ox ≡ o∅ {n}  →  def x y → def od∅ y
-   e1 {ox} {y} eq x>y with lv ox
-   e1 {o∅} {y} refl x>y | Zero   = lift ( ∅8 y (o<-subst (c<→o< {n} {ord→od y} {x} (def-subst {n} {x} {y} x>y refl (sym diso))) ord-iso eq ))  
-   e1 {o∅} {y} refl x>y | Suc lx = lift ( ∅8 y (o<-subst (c<→o< {n} {ord→od y} {x} (def-subst {n} {x} {y} x>y refl (sym diso))) ord-iso eq ))  
+   e1 {o∅} {y} refl x>y = lift ( ∅8 y (o<-subst (c<→o< {n} {ord→od y} {x} (def-subst {n} {x} {y} x>y refl (sym diso))) ord-iso eq ))  
+
+=→¬< : {x : Nat  } → ¬ ( x < x )
+=→¬< {Zero} ()
+=→¬< {Suc x} (s≤s lt) = =→¬< lt
+
+>→¬< : {x y : Nat  } → (x < y ) → ¬ ( y < x )
+>→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x
+
+c≤-refl : {n : Level} →  ( x : OD {n} ) → x c≤ x
+c≤-refl x = case1 refl
+
+o<> : {n : Level } ( ox oy : Ordinal {n}) → ox o<  oy  → oy o< ox  →  ⊥
+o<> ox oy (case1 x<y) (case1 y<x) = >→¬< x<y y<x
+o<> ox oy (case1 x<y) (case2 y<x) with d<→lv  y<x
+... | refl = =→¬< x<y
+o<> ox oy (case2 x<y) (case1 y<x) with d<→lv  x<y
+... | refl = =→¬< y<x
+o<> ox oy (case2 x<y) (case2 y<x) with d<→lv  x<y
+... | refl = trio<> x<y y<x
+
+o<¬≡ : {n : Level } ( ox oy : Ordinal {n}) → ox ≡ oy  → ox o<  oy  → ⊥
+o<¬≡ ox ox refl (case1 lt) =  =→¬< lt
+o<¬≡ ox ox refl (case2 (s< lt)) = trio<≡ refl lt
+
+o<→¬== : {n : Level} →  { x y : OD {n} } → (od→ord x ) o< ( od→ord y) →  ¬ (x == y )
+o<→¬== {n} {x} {y} (case1 lt) eq = {!!}
+o<→¬== {n} {x} {y} (case2 lt) eq = {!!}
+
+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<> (od→ord x) (od→ord y) 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<¬≡ (od→ord x) (od→ord y) (orefl oeq ) (c<→o< lt) 
+
+tri-c< : {n : Level} →  Trichotomous _==_ (_c<_ {suc n})
+tri-c< {n} x y with trio< {n} (od→ord x) (od→ord y) 
+tri-c< {n} x y | tri< a ¬b ¬c = tri< (def-subst (o<→c< a) oiso diso) (o<→¬== a) ( o<→¬c> a )
+tri-c< {n} x y | tri≈ ¬a b ¬c = tri≈ (o≡→¬c< b) (ord→== b) (o≡→¬c< (sym b))
+tri-c< {n} x y | tri> ¬a ¬b c = tri>  ( o<→¬c> c) (λ eq → o<→¬== c (eq-sym eq ) ) (def-subst (o<→c< c) oiso diso)
+
+∅2 : {n : Level} →  { x : OD {n} } → o∅ {n} o<  od→ord x → ¬ ( x  == od∅ {n} )
+∅2 {n} {x} lt record { eq→ = eq→ ; eq← = eq← } with ominimal (od→ord x ) lt
+... | min with eq→ ( def-subst (o<→c< (Minimumo.min<x min)) oiso refl )
+... | ()
+       
+
+is-od∅ : {n : Level} →  ( x : OD {suc n} ) → Dec ( x == od∅ {suc n} )
+is-od∅ {n} x with trio< {n} (od→ord x) (o∅ {suc n})
+is-od∅ {n} x | tri≈ ¬a b ¬c = yes ( ∅7 (orefl b) ) 
+is-od∅ {n} x | tri< (case1 ()) ¬b ¬c
+is-od∅ {n} x | tri< (case2 ()) ¬b ¬c
+is-od∅ {n} x | tri> ¬a ¬b c = no ( ∅2 c )
 
 open _∧_
 
 ∅9 : {n : Level} → (x : OD {n} ) → ¬ x == od∅ → o∅ o< od→ord x
 ∅9 x not = ∅5 ( od→ord x) lemma where
    lemma : ¬ od→ord x ≡ o∅
-   lemma eq = not ( ∅7 x eq )
+   lemma eq = not ( ∅7  eq )
 
 OD→ZF : {n : Level} → ZF {suc n} {n}
 OD→ZF {n}  = record { 
@@ -173,7 +243,7 @@
     Replace : OD {n} → (OD {n} → OD {n} ) → OD {n}
     Replace X ψ = sup-od ψ
     Select : OD {n} → (OD {n} → Set n ) → OD {n}
-    Select X ψ = record { def = λ x → ( ( def X  x ) ∧ ψ ( ord→od x )) } 
+    Select X ψ = record { def = λ x →  def X  x → ψ ( ord→od x ) } 
     _,_ : OD {n} → OD {n} → OD {n}
     x , y = record { def = λ z → ( (z ≡ od→ord x ) ∨ ( z ≡ od→ord y )) }
     Union : OD {n} → OD {n}
@@ -203,7 +273,7 @@
        ;   power← = {!!}
        ;   extentionality = {!!}
        ;   minimul = minimul
-       ;   regularity = {!!}
+       ;   regularity = regularity
        ;   infinity∅ = {!!}
        ;   infinity = {!!}
        ;   selection = {!!}
@@ -229,17 +299,18 @@
             lemma0 : mino (minord x not)  o< (od→ord x) → def x (od→ord (ord→od (mino (minord x not))))
             lemma0 m<x = def-subst {n} {ord→od (od→ord x)} {od→ord (ord→od (mino (minord x not)))} (o<→c< m<x) oiso refl
          regularity :  (x : OD) (not : ¬ (x == od∅)) →
-            (x ∋ minimul x not) ∧ (Select (minimul x not , x) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
+            (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
          proj1 ( regularity x non ) =  minimul<x x non 
          proj2 ( regularity x non ) = reg1 where
-            reg3 : {y : Ordinal} → ((y ≡ od→ord
-                        (ord→od (mino (minord x non)))) ∨ (y ≡ od→ord x) )
-                ∧ ( def (ord→od (mino (minord x non))) (od→ord (ord→od y))
-                ∧ def x (od→ord (ord→od y))) → Lift n ⊥
-            reg3 {y} = {!!}
-            reg0 : {y : Ordinal} → def (Select (minimul x non , x)
-                     (λ z → (minimul x non ∋ z) ∧ (x ∋ z))) y → def od∅ y
-            reg0 {y} t = reg3 t
-            reg1 :  Select (minimul x non , x) (λ x₁ → (minimul x non ∋ x₁) ∧ (x ∋ x₁)) == od∅
+            reg4 : {y : Ordinal} → (y ≡ od→ord (ord→od (mino (ominimal (od→ord x) (∅5 (od→ord x) (λ eq → non (∅7 eq))))))) ∨ (y ≡ od→ord x)
+            reg4 {y} = {!!}
+            reg2 : {y : Ordinal} → ( def (minimul x non) y )
+               → ( def (minimul x non) y → (minimul x non ∋ ord→od y) ∧ (x ∋ ord→od y) ) → ⊥ 
+            reg2 {y} or t with t or
+            reg2 s t | record { proj1 = proj1 ; proj2 = proj2 } = {!!}
+            reg0 : {y : Ordinal} → def (Select (minimul x non) (λ z → (minimul x non ∋ z) ∧ (x ∋ z))) y → def od∅ y
+            reg0 {y} t with (reg2 {y}) {!!} t
+            reg0 {y} t | ()
+            reg1 :  Select (minimul x non) (λ x₁ → (minimul x non ∋ x₁) ∧ (x ∋ x₁)) == od∅
             reg1 = record { eq→ =  reg0 ; eq← = λ () }
 
diff -r 7cb32d22528c -r 83b13f1f4f42 zf.agda
--- a/zf.agda	Sat May 25 21:31:07 2019 +0900
+++ b/zf.agda	Mon May 27 15:00:45 2019 +0900
@@ -57,9 +57,9 @@
   _⊆_ : ( A B : ZFSet  ) → ∀{ x : ZFSet } →  Set m
   _⊆_ A B {x} = A ∋ x →  B ∋ x
   _∩_ : ( A B : ZFSet  ) → ZFSet
-  A ∩ B = Select (A , B) (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  )
+  A ∩ B = Select A (  λ x → ( A ∋ x ) ∧ ( B ∋ x )  )
   _∪_ : ( A B : ZFSet  ) → ZFSet
-  A ∪ B = Select (A , B) (  λ x → ( A ∋ x ) ∨ ( B ∋ x )  )
+  A ∪ B = Union (A , B) 
   infixr  200 _∈_
   infixr  230 _∩_ _∪_
   infixr  220 _⊆_