--- a/src/PFOD.agda	Sat Jun 22 11:39:35 2024 +0900
+++ b/src/PFOD.agda	Sat Jun 22 12:39:58 2024 +0900
@@ -191,24 +191,22 @@
      f01 : (x y : HOD) (ltx : odef (Omega ho<) (& x)) (lty : odef (Omega ho<) (& y)) → x =h= y →  f (ω→nat x ltx) ≡ i1  → f (ω→nat y lty) ≡ i1
      f01 x y ltx lty x=y feq = subst (λ k → f k ≡ i1 ) (ω→nato-cong ltx lty (==→o≡ x=y) ) feq
      f00 :  (x y : HOD) → x =h= y → (fω→2-sel f x ) ⇔ (fω→2-sel f y)
-     proj1 (f00 x y x=y) fs = ⟪ subst (λ k → odef (Omega ho<)  k) (==→o≡ x=y)       (proj1 fs)  , (λ lt → f01 x y (proj1 fs) lt x=y (proj2 fs (f02 _ _ lt))) ⟫ where
-         f02 : (y x : Ordinal ) → odef (Omega ho<) y → Omega-d x
-         f02 _ x OD.iφ = ?
-         f02 _ x (OD.isuc lt) = ?
-     proj2 (f00 x y x=y) fs = ⟪ subst (λ k → odef (Omega ho<)  k) (sym (==→o≡ x=y)) (proj1 fs)  , (λ lt → f01 y x (proj1 fs) lt (==-sym x=y) (proj2 fs ?)) ⟫
+     proj1 (f00 x y x=y) fs = ⟪ subst (λ k → odef (Omega ho<)  k) (==→o≡ x=y)       (proj1 fs)  , (λ lt → f01 x y (proj1 fs) lt x=y (f02 fs)) ⟫ where
+         f02 : (fs : fω→2-sel f x ) →  f (ω→nat x (proj1 fs)) ≡ i1   -- work around for cubical bug?
+         f02 ⟪ wx , wx→eq ⟫ = wx→eq wx
+     proj2 (f00 x y x=y) fs = ⟪ subst (λ k → odef (Omega ho<)  k) (sym (==→o≡ x=y)) (proj1 fs)  , (λ lt → f01 y x (proj1 fs) lt (==-sym x=y) (f02 fs)) ⟫ where
+         f02 : (fs : fω→2-sel f y ) →  f (ω→nat y (proj1 fs)) ≡ i1
+         f02 ⟪ wy , wy→eq ⟫ = wy→eq wy
 
 fω→2 : (Nat → Two) → HOD
 fω→2 f = Select (Omega ho<) (fω→2-sel f) (fω→2-wld f) 
 
--- import Axiom.Extensionality.Propositional
--- postulate f-extensionality : { n m : Level}  → Axiom.Extensionality.Propositional.Extensionality n m
-
 ω2∋f : (f : Nat → Two) → ω→2 ∋ fω→2 f
-ω2∋f f = ? -- power← (Omega ho<) (fω→2 f) (λ {x} lt →  proj1 ((proj2 (selection {fω→2-sel f} {(Omega ho<)} )) lt))
+ω2∋f f = power← (Omega ho<) (fω→2 f) (λ {x} lt →  proj1 ((proj2 (selection {fω→2-sel f} {fω→2-wld f} {Omega ho<} {x} )) lt))
 
 ω→2f≡i1 : (X i : HOD) → (iω : (Omega ho<) ∋ i) → (lt : ω→2 ∋ X ) → ω2→f X lt (ω→nat i iω)  ≡ i1 → X ∋ i
 ω→2f≡i1 X i iω lt eq with ∋-p X (nat→ω (ω→nat i iω))
-ω→2f≡i1 X i iω lt eq | yes p = ? -- subst (λ k → X ∋ k ) (nat→ω-iso iω) p
+ω→2f≡i1 X i iω lt eq | yes p = subst (λ k → odef X k) (==→o≡ (nat→ω-iso iω )) p
 
 ω2→f-iso : (X : HOD) → ( lt : ω→2 ∋ X ) → fω→2 ( ω2→f X lt )  =h= X
 eq→ (ω2→f-iso X lt) {x} ⟪ ωx , ⟪ ωx1 , iso ⟫ ⟫ = le00 where
@@ -222,21 +220,22 @@
     ... | yes p  = refl
     ... | no ¬p  = ⊥-elim ( ¬p (subst (λ k → odef X k ) le03 Xx )) where
         le03 :  x ≡ & (nat→ω (ω→nato wx))
-        le03 = ? -- subst₂ (λ j k → j ≡ k ) &iso refl (cong (&) (sym ( nat→ω-iso wx ) ) )
+        le03 = trans (sym &iso) (sym (==→o≡ ( nat→ω-iso wx ) ))
 
-¬i1→i0 : ?
-¬i1→i0 = ?
+¬i1→i0 : {x : Two} → ¬ (x ≡ i1 ) → x ≡ i0 
+¬i1→i0 {i0} ne = refl
+¬i1→i0 {i1} ne = ⊥-elim ( ne refl )
 
-fω→2-iso : (f : Nat → Two) → ω2→f ( fω→2 f ) (ω2∋f f) ≡ f
-fω→2-iso f = ? where -- f-extensionality (λ x → le01 x ) where
+fω→2-iso : (f : Nat → Two) → (x : Nat ) → ω2→f ( fω→2 f ) (ω2∋f f) x ≡  f x
+fω→2-iso f x = le01 x  where
     le01 : (x : Nat) → ω2→f (fω→2 f) (ω2∋f f) x ≡ f x
     le01 x with  ∋-p (fω→2 f) (nat→ω x) 
-    le01 x | yes p = subst (λ k → i1 ≡ f k ) (ω→nat-iso0 x (proj1 (proj2 p)) ?) (sym ((proj2 (proj2 p)) le02)) where
+    le01 x | yes p = subst (λ k → i1 ≡ f k ) (ω→nat-iso0 x (proj1 (proj2 p)) (==-trans *iso *iso)) (sym ((proj2 (proj2 p)) le02)) where
         le02 :  Omega-d (& (* (& (nat→ω x))))
         le02 = proj1 (proj2 p )
     le01 x | no ¬p = sym ( ¬i1→i0 le04 ) where
         le04 : ¬ f x ≡ i1
         le04 fx=1 = ¬p ⟪ ω∋nat→ω {x} , ⟪ subst (λ k → Omega-d k) (sym &iso) (ω∋nat→ω {x})  , le05 ⟫ ⟫ where
             le05 : (lt : Omega-d (& (* (& (nat→ω x))))) → f (ω→nato lt) ≡ i1
-            le05 lt = trans (cong f (ω→nat-iso0 x lt ?)) fx=1
+            le05 lt = trans (cong f (ω→nat-iso0 x lt (==-trans *iso *iso))) fx=1