# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1558546322 -32400
# Node ID 4d64509067d03d1ed8fdc82d56eb951032c94d9e
# Parent  88b77cecaeba89fa770c42ec3857f99929ed9a9e
transitive

diff -r 88b77cecaeba -r 4d64509067d0 ordinal-definable.agda
--- a/ordinal-definable.agda	Wed May 22 19:24:11 2019 +0900
+++ b/ordinal-definable.agda	Thu May 23 02:32:02 2019 +0900
@@ -26,9 +26,7 @@
 
 postulate      
   od→ord : {n : Level} → OD {n} → Ordinal {n}
-
-ord→od : {n : Level} → Ordinal {n} → OD {n} 
-ord→od x = record { def = λ y → x ≡ y }
+  ord→od : {n : Level} → Ordinal {n} → OD {n} 
 
 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n
 _∋_ {n} a x  = def a ( od→ord x )
@@ -40,8 +38,8 @@
 a c≤ b  = (a ≡ b)  ∨ ( b ∋ a )
 
 postulate      
-  c<→o< : {n : Level} {x y : OD {n} } → x c< y → od→ord x o< od→ord x
-  o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → ord→od x c< ord→od x
+  c<→o< : {n : Level} {x y : OD {n} } → x c< y → od→ord x o< od→ord y
+  o<→c< : {n : Level} {x y : Ordinal {n} } → x o< y → ord→od x c< ord→od y
   oiso : {n : Level} {x : OD {n}} → ord→od ( od→ord x ) ≡ x
   diso : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x
   sup-od : {n : Level } → ( OD {n} → OD {n}) →  OD {n}
@@ -79,8 +77,18 @@
    ... | t with t (case2 (s< (ℵΦ< {_} {_} {Φ (Suc lx)}))) 
    c3 .(Suc lx) (ℵ lx) d not | t | ()
 
-∅2 : {n : Level} →  od→ord ( od∅ {n} ) ≡ o∅ {n}
-∅2 {n}  = {!!}
+def-subst : {n : Level } {Z : OD {n}} {X : Ordinal {n} }{z : OD {n}} {x : Ordinal {n} }→ def Z X → Z ≡ z  →  X ≡ x  →  def z x
+def-subst df refl refl = df
+
+transitive : {n : Level } { x y z : OD {n} } → y ∋ x → z ∋ y → z ∋ x
+transitive  {n} {x} {y} {z} x∋y  z∋y with  ordtrans ( c<→o< {n} {x} {y} x∋y ) (  c<→o< {n} {y} {z} z∋y ) 
+... | t = lemma0 (lemma t) where
+   lemma : ( od→ord x ) o< ( od→ord z ) → def ( ord→od ( od→ord z )) ( od→ord ( ord→od ( od→ord x )))
+   lemma xo<z = o<→c< xo<z
+   lemma0 :  def ( ord→od ( od→ord z )) ( od→ord ( ord→od ( od→ord x ))) →  def z (od→ord x)
+   lemma0 dz  = def-subst {n} { ord→od ( od→ord z )} { od→ord ( ord→od ( od→ord x))} dz (oiso) (diso)
+
+open Ordinal
 
 HOD→ZF : {n : Level} → ZF {suc n} {suc n}
 HOD→ZF {n}  = record { 
@@ -145,16 +153,11 @@
          empty : (x : OD {n} ) → ¬ Lift (suc n) (od∅ ∋ x)
          empty x (lift (lift ()))
          union→ : (X x y : OD {n} ) → Lift (suc n) (X ∋ x) → Lift (suc n) (x ∋ y) → Lift (suc n) (Union X ∋ y)
-         union→ X x y (lift X∋x) (lift x∋y) = lift lemma  where
+         union→ X x y (lift X∋x) (lift x∋y) = lift {!!}  where
             lemma : {z : Ordinal {n} } → def X z → z ≡ od→ord y
             lemma {z} X∋z = {!!}
-         -- _∋_ {n} a x  = def a ( od→ord x )
-         ¬∅ : (x : OD {n} ) → ¬ x ≡ od∅ → Ordinal {n}
-         ¬∅ = {!!}
-         ¬∅∈ : (x : OD {n} ) → (not : ¬ x ≡ od∅ ) → x ∋ (ord→od (¬∅ x not))
-         ¬∅∈ = {!!}
          minimul : OD {n} → ( OD {n} ∧ OD {n} )
-         minimul x = {!!}
+         minimul x = record { proj1 = record { def = {!!} } ; proj2 = record { def = {!!} } }
          regularity : (x : OD) → ¬ x ≡ od∅ →
                 Lift (suc n) (x ∋ proj1 (minimul x)) ∧
                 (Select (proj1 (minimul x ) , x) (λ x₁ → Lift (suc n) (proj1 ( minimul x ) ∋ x₁) ∧ Lift (suc n) (x ∋ x₁)) ≡ od∅)