--- a/src/Polynominal.agda	Sun May 16 22:01:28 2021 +0900
+++ b/src/Polynominal.agda	Sun May 16 23:38:00 2021 +0900
@@ -235,14 +235,12 @@
                f' ∙  id1 A _ ≈⟨ idR ⟩
                f' ∎  )  where
                    --  (phi : φ x f) → xnef x phi
-                   xf :  (g : Hom A b a) → (fp : φ x g) → g ≅ (x ∙ ○ b) → xnef x fp
-                   xf .((A Category.o x) (CCC.○ C b)) (i .((A Category.o x) (CCC.○ C b))) _≅_.refl = {!!} -- x ≅ x ∙ (○ b) → ⊥
-                   xf g ii eq = lift tt
-                   xf g (iii fp fp₁) eq = {!!}
-                   xf g (iv fp fp₁) eq = {!!}
-                   xf g (v fp) eq = {!!}
+                   xff :  ((fp : φ x f) → xnef x fp)  → (g : Hom A b a)  → (gp : φ x g)  → xnef x gp
+                   xff = {!!}
+                   xf :  (fp : φ x (x ∙ ○ b)) → xnef x fp
+                   xf = {!!}
                    u2 : k x {x ∙ ○ b} (i _) ≈ k x {x} ii ∙ < π , k x {○ b} (i _) > 
-                   u2 = ki x (x ∙ ○ b) (iv ii (i _)) (λ gp  → xf (x ∙ ○ b) gp HE.refl )
+                   u2 = ki x (x ∙ ○ b) (iv ii (i _)) xf
 
   -- functional completeness ε form
   --