--- a/src/yoneda.agda	Tue Mar 09 12:50:52 2021 +0900
+++ b/src/yoneda.agda	Tue Mar 09 13:24:20 2021 +0900
@@ -326,8 +326,7 @@
     → SetsAop [ SetsAop [ FMap YonedaFunctor f o g ] ≈ SetsAop [ FMap YonedaFunctor f o h ] ]
     → SetsAop [  g ≈ h ]
 Yoneda-injective {a} {b} {x} {y} g h f yg=yh = begin
-             TMap g _ ≈⟨  {!!} ⟩
-             -- {!!} ≈⟨  {!!} ⟩   -- Hom Sets (FObj y x₁) (FObj (FObj YonedaFunctor a) x₁)
+             TMap g _ ≈⟨ {!!}  ⟩
              TMap h _ ∎  where
      open ≈-Reasoning Sets
      hoge : (x₁ : Obj A) → FObj y x₁ -- Hom Sets (FObj y x₁) (FObj (FObj YonedaFunctor a) x₁)
@@ -343,25 +342,33 @@
        sur :        {a a' : Obj A} (g : Hom B (FObj F a) (FObj F a')) → Hom A a a'
        surjective : {a a' : Obj A} (g : Hom B (FObj F a) (FObj F a')) → B [ FMap F (sur g) ≈ g ]
 
+open CatSurjective
+
 CatEpiR : { c₁ c₂ ℓ c₁' c₂' ℓ' : Level} ( A : Category c₁ c₂ ℓ ) ( B : Category c₁' c₂' ℓ' ) (F : Functor A B)
     → {a a' : Obj A } {b : Obj B} (g h : Hom B (FObj F a') b) 
     → ( f : Hom A a a' )
     → (B [ B [ g o FMap F f ] ≈  B [ h o FMap F f ] ] → B [ g  ≈ h ])
     → CatSurjective A B F 
-CatEpiR A B F g h f eq = record { sur = {!!} ; surjective = {!!} }
+CatEpiR A B F g h f eq = record { sur = λ g → {!!}  ;  surjective = {!!} } where
+    ylem22 :  {a a' : Obj A} (i : Hom B (FObj F a) (FObj F a')) → B [ FMap F {!!} ≈ i ]
+    ylem22 i = begin
+     FMap F {!!} ≈⟨ {!!} ⟩
+     i ∎ 
+     where
+       open ≈-Reasoning B
 
 CatEpi : { c₁ c₂ ℓ c₁' c₂' ℓ' : Level} ( A : Category c₁ c₂ ℓ ) ( B : Category c₁' c₂' ℓ' ) (F : Functor A B)
-    → CatSurjective A B F
+    → (s : CatSurjective A B F )
     → {a a' : Obj A } {b : Obj B} (g h : Hom B (FObj F a') b)
-    → ( f : (g h : Hom B (FObj F a') b) → Hom A a a' )
-    → B [ B [ g o FMap F ( f g h ) ] ≈  B [ h o FMap F (f g h ) ] ] → B [ g  ≈ h ]
-CatEpi A B F s g h f gf=hf = begin
+    → (f : {a a' : Obj A } {b : Obj B} (g h : Hom B (FObj F a') b) → Hom A a a' )
+    → B [ B [ g o FMap F (f {a} {a'} g h ) ] ≈  B [ h o FMap F (f g h )] ] → B [ g  ≈ h ]
+CatEpi A B F s g h f eq = begin
      g ≈⟨ {!!} ⟩
      h ∎ 
   where
      open ≈-Reasoning B
-     sj : B [ FMap F ( CatSurjective.sur s (FMap F (f g h))) ≈ FMap F (f g h) ]
-     sj  = CatSurjective.surjective s (FMap F (f g h)) 
+     -- sj : B [ FMap F ( CatSurjective.sur s (FMap F (f g h))) ≈ FMap F (f g h) ]
+     -- sj  = CatSurjective.surjective s (FMap F (f g h)) 
 
 Yoneda-surjective : CatSurjective A SetsAop YonedaFunctor 
 Yoneda-surjective  = record { sur = λ {a} {a'} g → f g ; surjective = λ g → 
@@ -381,7 +388,7 @@
          TMap g _ ≈⟨ {!!} ⟩
          TMap h _
          ∎ where
-             open ≈-Reasoning (Sets) 
+             open ≈-Reasoning Sets
              s : CatSurjective A SetsAop YonedaFunctor 
              s = Yoneda-surjective