# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1559380644 -32400
# Node ID dd430a95610fafc6174bc06851ea34a1eb119955
# Parent  f39f1a90d154a6fa2128893737a77bdf0087cda5
fix ordinal

diff -r f39f1a90d154 -r dd430a95610f ordinal-definable.agda
--- a/ordinal-definable.agda	Sat Jun 01 14:43:05 2019 +0900
+++ b/ordinal-definable.agda	Sat Jun 01 18:17:24 2019 +0900
@@ -358,14 +358,15 @@
          union-lemma-u {X} {z} U>z = lemma <-osuc where
              lemma : {oz ooz : Ordinal {suc n}} → oz o< ooz → def (ord→od ooz) oz
              lemma {oz} {ooz} lt = def-subst {suc n} {ord→od  ooz} (o<→c< lt) refl diso
-         union→ :  (X z u : OD) → (Union X ∋ u) ∧ (u ∋ z) → Union X ∋ z
+         union→ :  (X z u : OD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
          union→ X y u xx with trio< ( od→ord u ) ( osuc ( od→ord y ))
          union→ X y u xx | tri< a ¬b ¬c = {!!}
-         union→ X y u xx | tri≈ ¬a b ¬c = {!!}
-         union→ X y u xx | tri> ¬a ¬b c = {!!}
-            --  c<→o<  (transitive {n} {X} {x} {y} X∋x x∋y  )
+         union→ X y u xx | tri≈ ¬a b ¬c = lemma b (c<→o< (proj1 xx )) where
+             lemma : {oX ou ooy : Ordinal {suc n}} →  ou ≡ ooy  → ou o< oX   → ooy  o< oX
+             lemma refl lt = lt
+         union→ X y u xx | tri> ¬a ¬b c = ordtrans {suc n} {osuc ( od→ord y )} {od→ord u} {od→ord X} c ( c<→o< (proj1 xx )) 
          union← :  (X z : OD) (X∋z : Union X ∋ z) → (X ∋ union-u X z X∋z) ∧ (union-u X z X∋z ∋ z )
-         union← X z X∋z = record { proj1 = {!!} ; proj2 = union-lemma-u X∋z }
+         union← X z X∋z = record { proj1 = def-subst {suc n} (o<→c< X∋z) oiso refl ; proj2 = union-lemma-u X∋z } 
          ψiso :  {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y   → ψ y
          ψiso {ψ} t refl = t
          selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y)
diff -r f39f1a90d154 -r dd430a95610f ordinal.agda
--- a/ordinal.agda	Sat Jun 01 14:43:05 2019 +0900
+++ b/ordinal.agda	Sat Jun 01 18:17:24 2019 +0900
@@ -42,7 +42,8 @@
 o<-subst df refl refl = df
 
 osuc : {n : Level} ( x : Ordinal {n} ) → Ordinal {n}
-osuc record { lv = lx ; ord = (Φ lv) } = record { lv = lx ; ord = OSuc lx (Φ lv) }
+osuc record { lv = 0 ; ord = (Φ lv) } = record { lv = 0 ; ord = OSuc 0 (Φ lv) }
+osuc record { lv = Suc lx ; ord = (Φ (Suc lv)) } = record { lv = Suc lx ; ord = ℵ lv }
 osuc record { lv = lx ; ord = (OSuc lx ox ) } =  record { lv = lx ; ord = OSuc lx (OSuc lx ox) }
 osuc record { lv = Suc lx ; ord = ℵ lx } = record { lv = Suc lx ; ord = OSuc (Suc lx) (ℵ lx) }
 
@@ -63,10 +64,35 @@
 s<refl {n} {Suc lv} {ℵ lv} = ℵs<
 
 <-osuc : {n : Level} { x : Ordinal {n} } → x o< osuc x
-<-osuc {n} { record { lv = lv ; ord = (Φ .(lv)) } } = case2 Φ<
-<-osuc {n} { record { lv = lv ; ord = (OSuc lv ox ) } } = case2 ( s< s<refl )
+<-osuc {n} { record { lv = 0 ; ord = Φ 0 } } = case2 Φ<
+<-osuc {n} { record { lv = (Suc lv) ; ord = Φ  (Suc lv) } } = case2 ℵΦ<
+<-osuc {n} {record { lv = Zero ; ord = OSuc .0 ox }} = case2 ( s< s<refl )
+<-osuc {n} {record { lv = Suc lv₁ ; ord = OSuc .(Suc lv₁) ox }} = case2 ( s< s<refl )
 <-osuc {n} { record { lv = .(Suc lv₁) ; ord = (ℵ lv₁) } } =  case2 ℵs< 
 
+osuc-lveq : {n : Level} { x : Ordinal {n} } → lv x ≡ lv ( osuc x )
+osuc-lveq {n} {record { lv = 0 ; ord = Φ 0 }} = refl
+osuc-lveq {n} {record { lv = Suc lv ; ord = Φ (Suc lv) }} = refl
+osuc-lveq {n} {record { lv = Zero ; ord = OSuc .0 ord₁ }} = refl
+osuc-lveq {n} {record { lv = Suc lv₁ ; ord = OSuc .(Suc lv₁) ord₁ }} = refl
+osuc-lveq {n} {record { lv = .(Suc lv₁) ; ord = ℵ lv₁ }} = refl
+
+nat-<> : { x y : Nat } → x < y → y < x → ⊥
+nat-<>  (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x
+
+osuc-< : {n : Level} { x y : Ordinal {n} } → y o< osuc x  → x o< y → ⊥
+osuc-< {n} {record { lv = .0 ; ord = Φ .0 }} {record { lv = .(Suc _) ; ord = ord }} (case1 ()) (case1 (s≤s z≤n))
+osuc-< {n} {record { lv = .0 ; ord = OSuc .0 ord₁ }} {record { lv = .(Suc _) ; ord = ord }} (case1 ()) (case1 (s≤s z≤n))
+osuc-< {n} {record { lv = lx ; ord = xo }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) with osuc-lveq  {n} {record { lv = lx ; ord = xo }}
+osuc-< {n} {record { lv = Zero ; ord = Φ .0 }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) | eq = nat-<> lt1 lt2
+osuc-< {n} {record { lv = Suc lx ; ord = Φ .(Suc lx) }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) | eq = nat-<> lt1 lt2
+osuc-< {n} {record { lv = Zero ; ord = OSuc .0 xo }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) | eq = nat-<> lt1 lt2
+osuc-< {n} {record { lv = Suc lx ; ord = OSuc .(Suc lx) xo }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) | eq = nat-<> lt1 lt2
+osuc-< {n} {record { lv = .(Suc lv₁) ; ord = ℵ lv₁ }} {record { lv = ly ; ord = yo }} (case1 lt1) (case1 lt2) | refl = nat-<> lt1 lt2
+osuc-< {n} {x} {y} (case1 x₁) (case2 x₂) = {!!}
+osuc-< {n} {x} {y} (case2 x₁) (case1 x₂) = {!!}
+osuc-< {n} {x} {y} (case2 x₁) (case2 x₂) = {!!}
+
 open import Relation.Binary.HeterogeneousEquality using (_≅_;refl)
 
 ordinal-cong : {n : Level} {x y : Ordinal {n}}  →
diff -r f39f1a90d154 -r dd430a95610f zf.agda
--- a/zf.agda	Sat Jun 01 14:43:05 2019 +0900
+++ b/zf.agda	Sat Jun 01 18:17:24 2019 +0900
@@ -51,7 +51,7 @@
      pair : ( A B : ZFSet  ) →  ( (A , B)  ∋ A ) ∧ ( (A , B)  ∋ B  )
      -- ∀ x ∃ y ∀ z (z ∈ y ⇔ ∃ u ∈ x  ∧ (z ∈ u))
      union-u : ( X z : ZFSet  ) → Union X ∋ z → ZFSet
-     union→ : ( X z u : ZFSet ) → ((Union X ∋ u )  ∧ (u ∋ z )) → Union X ∋ z
+     union→ : ( X z u : ZFSet ) → ( X ∋ u ) ∧ (u ∋ z ) → Union X ∋ z
      union← : ( X z : ZFSet ) → (X∋z : Union X ∋ z ) → (X ∋ union-u X z X∋z)  ∧ (union-u X z X∋z ∋ z )
   _∈_ : ( A B : ZFSet  ) → Set m
   A ∈ B = B ∋ A