# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1561464307 -32400
# Node ID 89204edb71fab1f927e5926ac9b48d72c39821ba
# Parent  5f97ebaeb89ba88f49fcbb63d4f07ae3d1e9b266
f x d

diff -r 5f97ebaeb89b -r 89204edb71fa HOD.agda
--- a/HOD.agda	Tue Jun 25 16:04:31 2019 +0900
+++ b/HOD.agda	Tue Jun 25 21:05:07 2019 +0900
@@ -17,7 +17,7 @@
 record HOD {n : Level}  : Set (suc n) where
   field
     def : (x : Ordinal {n} ) → Set n
-    otrans : {x y : Ordinal {n} } → def x → y o< x → def y
+    otrans : {x : Ordinal {n} } → def x → { y : Ordinal {n} } → y o< x → def y
 
 open HOD
 open import Data.Unit
@@ -46,8 +46,8 @@
 -- Ordinal in HOD ( and ZFSet )
 Ord : { n : Level } → ( a : Ordinal {n} ) → HOD {n}
 Ord {n} a = record { def = λ y → y o< a ; otrans = lemma }  where
-   lemma : {x y : Ordinal} → x o< a → y o< x → y o< a
-   lemma {x} {y} x<a y<x = ordtrans {n} {y} {x} {a} y<x x<a
+   lemma : {x : Ordinal} → x o< a → {y : Ordinal} → y o< x → y o< a
+   lemma {x}  x<a {y} y<x = ordtrans {n} {y} {x} {a} y<x x<a
 
 -- od∅ : {n : Level} → HOD {n} 
 -- od∅ {n} = record { def = λ _ → Lift n ⊥ }
@@ -83,8 +83,8 @@
 
 cseq : {n : Level} →  HOD {n} →  HOD {n}
 cseq x = record { def = λ y → osuc y o< (od→ord x) ; otrans = lemma } where
-   lemma : {ox oy : Ordinal} → osuc ox o< od→ord x → oy o< ox → osuc oy o< od→ord x
-   lemma {ox} {oy} oox<Ox oy<ox  = ordtrans (osucc oy<ox ) oox<Ox 
+   lemma : {ox : Ordinal} → osuc ox o< od→ord x → { oy : Ordinal}→ oy o< ox → osuc oy o< od→ord x
+   lemma {ox}  oox<Ox {oy} oy<ox  = ordtrans (osucc oy<ox ) oox<Ox 
 
 def-subst : {n : Level } {Z : HOD {n}} {X : Ordinal {n} }{z : HOD {n}} {x : Ordinal {n} }→ def Z X → Z ≡ z  →  X ≡ x  →  def z x
 def-subst df refl refl = df
@@ -247,17 +247,11 @@
     Replace : HOD {suc n} → (HOD {suc n} → HOD {suc n} ) → HOD {suc n}
     Replace X ψ = sup-od ψ
     Select : (X : HOD {suc n} ) → ((x : HOD {suc n} ) → X ∋ x → Set (suc n) ) → HOD {suc n}
-    Select X ψ = record { def = λ x → (d : def X x ) → f x d ; otrans = ftrans }  where
+    Select X ψ = record { def = λ x → (d : def X x)  → f x d ; otrans = λ {x} g {y} d1 → {!!} }  where
        f : (x : Ordinal {suc n}) → (d : def X x ) → Set (suc n) 
        f x d = ψ (ord→od x)  (subst (λ k → def X k ) (sym diso) d)
-       ftrans : {x y : Ordinal} → ((d : def X x) → f x d) → y o< x → (d : def X y) → f y d
-       ftrans {x} {y} g  = TransFinite {suc n} {λ y1 → (y1<x : y1 o< x)  → (d1 : def X y1)  → f y1 d1} lemma1 lemma2 y where
-          lemma1 :  (lx : Nat) → record { lv = lx ; ord = Φ lx } o< x → (d1 : def X (record { lv = lx ; ord = Φ lx })) → f (record { lv = lx ; ord = Φ lx }) d1
-          lemma1 = {!!}
-          lemma2 : (lx : Nat) (x₁ : OrdinalD lx) → (record { lv = lx ; ord = x₁ } o< x →
-             (d1 : def X (record { lv = lx ; ord = x₁ })) → f (record { lv = lx ; ord = x₁ }) d1) → record { lv = lx ; ord = OSuc lx x₁ } o< x →
-             (d1 : def X (record { lv = lx ; ord = OSuc lx x₁ })) → f (record { lv = lx ; ord = OSuc lx x₁ }) d1
-          lemma2 = {!!}
+       ftrans' : {x : Ordinal} ( g : (x : Ordinal {suc n} ) (d : def X x ) → f x d ) → {y : Ordinal} → y o< x → (d : def X y) → f y d
+       ftrans' {x} g {y} y<x d = g y d
     _,_ : HOD {suc n} → HOD {suc n} → HOD {suc n}
     x , y = Ord (omax (od→ord x) (od→ord y))
     Union : HOD {suc n} → HOD {suc n}