--- a/OD.agda	Mon Jul 27 15:11:54 2020 +0900
+++ b/OD.agda	Mon Jul 27 16:20:14 2020 +0900
@@ -266,8 +266,6 @@
 odmax<od→ord  : { x y : HOD } → x ∋ y →  Set n
 odmax<od→ord {x} {y} x∋y = odmax x o< od→ord x
 
--- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n (suc n)
-
 in-codomain : (X : HOD  ) → ( ψ : HOD  → HOD  ) → OD 
 in-codomain  X ψ = record { def = λ x → ¬ ( (y : Ordinal ) → ¬ ( odef X y ∧  ( x ≡ od→ord (ψ (ord→od y )))))  }
 
@@ -455,14 +453,19 @@
 x =h= y  = od x == od y
 
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+postulate f-extensionality : { n m : Level}  → HE.Extensionality n m
 
-ord∋eq : {n : Level } {A i : HOD } → { f : (x : HOD ) → A ∋ x → Set n}
+
+ord∋eq :  {A i : HOD } → { f : (x : HOD ) → A ∋ x → Set (suc n)}
     → ( ( x : Ordinal ) → ( lx : odef A x ) → f (ord→od x) (d→∋ A lx) )
     → ( lt : A ∋ i ) → f i lt 
-ord∋eq {n} {A} {i} {f} of lt = subst (λ k → odef A k ) ?  (of (od→ord i) ?)
+ord∋eq {A} {i} {f} of lt with of (od→ord i) lt
+... | t = HE.subst₂ (λ j k → f j (k j)) (HE.≡-to-≅  oiso) (f-extensionality (λ _ → refl ) lemma ) t where
+   lemma : (i : HOD) → ? ≅ ?
+   lemma = {!!}
 
 nat→ω-iso : {i : HOD} → (lt : infinite ∋ i ) → nat→ω ( ω→nat i lt ) ≡ i
-nat→ω-iso  {i} lt = ord∋eq {_} {infinite} {i} (λ x lx → lemma lx ) lt where
+nat→ω-iso  {i} lt = ord∋eq {infinite} {i} (λ x lx → lemma lx ) lt where
    lemma : {x : Ordinal} → (lx : infinite-d x ) → nat→ω ( ω→nat (ord→od x) (d→∋ infinite lx) ) ≡ ord→od x
    lemma = {!!}