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

diff -r d088eb66564e -r f39f1a90d154 ordinal-definable.agda
--- a/ordinal-definable.agda	Sat Jun 01 10:23:53 2019 +0900
+++ b/ordinal-definable.agda	Sat Jun 01 14:43:05 2019 +0900
@@ -331,9 +331,9 @@
     isZF = record {
            isEquivalence  = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
        ;   pair  = pair
-       ;   union-u = {!!}
-       ;   union→ = {!!}
-       ;   union← = {!!}
+       ;   union-u = union-u
+       ;   union→ = union→
+       ;   union← = union←
        ;   empty = empty
        ;   power→ = {!!}
        ;   power← = {!!}
@@ -353,19 +353,19 @@
          empty : (x : OD {suc n} ) → ¬  (od∅ ∋ x)
          empty x ()
          union-u : (X z : OD {suc n}) → Union X ∋ z → OD {suc n}
-         union-u X z U>z with od→ord X | osuc (od→ord z )
-         union-u X z (case1 (s≤s z≤n)) | record { lv = .(Suc _) ; ord = ord₁ } | record { lv = .0 ; ord = ord₂ } = {!!}
-         union-u X z (case1 (s≤s (s≤s x))) | record { lv = .(Suc (Suc _)) ; ord = ord₁ } | record { lv = .(Suc _) ; ord = ord₂ } = {!!}
-         union-u X z (case2 Φ<) | record { lv = lv₁ ; ord = .(OSuc lv₁ _) } | record { lv = .lv₁ ; ord = .(Φ lv₁) } = {!!}
-         union-u X z (case2 (s< x)) | record { lv = lv₁ ; ord = .(OSuc lv₁ _) } | record { lv = .lv₁ ; ord = .(OSuc lv₁ _) } = {!!}
-         union-u X z (case2 ℵΦ<) | record { lv = .(Suc _) ; ord = .(ℵ _) } | record { lv = .(Suc _) ; ord = .(Φ (Suc _)) } = {!!}
-         union-u X z (case2 (ℵ< x)) | record { lv = .(Suc _) ; ord = .(ℵ _) } | record { lv = .(Suc _) ; ord = .(OSuc (Suc _) _) } = {!!}
-         union-u X z (case2 ℵs<) | record { lv = .(Suc _) ; ord = .(OSuc (Suc _) (ℵ _)) } | record { lv = .(Suc _) ; ord = .(ℵ _) } = {!!}
-         union-u X z (case2 (ℵss< x)) | record { lv = .(Suc _) ; ord = .(OSuc (Suc _) _) } | record { lv = .(Suc _) ; ord = .(ℵ _) } = {!!}
-         union→ :  (X x y : OD {suc n}) → X ∋ x → x ∋ y → Union X ∋ y
-         union→ X x y X∋x x∋y = {!!} --  c<→o<  (transitive {n} {X} {x} {y} X∋x x∋y  )
-         union← :  (X z : OD {suc n}) → (X∋z : Union X ∋ z) → ((Union X ∋ union-u X z X∋z) ∧ (union-u X z X∋z ∋ z))
-         union← = {!!}
+         union-u X z U>z = ord→od ( osuc ( od→ord z ) )
+         union-lemma-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → union-u X z U>z  ∋ z
+         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 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 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 }
          ψ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 d088eb66564e -r f39f1a90d154 ordinal.agda
--- a/ordinal.agda	Sat Jun 01 10:23:53 2019 +0900
+++ b/ordinal.agda	Sat Jun 01 14:43:05 2019 +0900
@@ -43,7 +43,7 @@
 
 osuc : {n : Level} ( x : Ordinal {n} ) → Ordinal {n}
 osuc record { lv = lx ; ord = (Φ lv) } = record { lv = lx ; ord = OSuc lx (Φ lv) }
-osuc record { lv = lx ; ord = (OSuc lx ox ) } =  record { lv = lx ; ord = OSuc lx ox }
+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) }
 
 open import Data.Nat.Properties 
@@ -62,6 +62,11 @@
 s<refl {n} {lv} {OSuc lv x}  = s< s<refl 
 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 = .(Suc lv₁) ; ord = (ℵ lv₁) } } =  case2 ℵs< 
+
 open import Relation.Binary.HeterogeneousEquality using (_≅_;refl)
 
 ordinal-cong : {n : Level} {x y : Ordinal {n}}  →
diff -r d088eb66564e -r f39f1a90d154 zf.agda
--- a/zf.agda	Sat Jun 01 10:23:53 2019 +0900
+++ b/zf.agda	Sat Jun 01 14:43:05 2019 +0900
@@ -52,7 +52,7 @@
      -- ∀ 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 : ZFSet ) → (X∋z : Union X ∋ z ) → (Union X ∋ union-u X z X∋z)  ∧ (union-u X z X∋z ∋ 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
   _⊆_ : ( A B : ZFSet  ) → ∀{ x : ZFSet } →  Set m