--- a/src/yoneda.agda	Wed Mar 10 09:06:57 2021 +0900
+++ b/src/yoneda.agda	Wed Mar 10 09:22:12 2021 +0900
@@ -345,23 +345,6 @@
 
 open CatSurjective
 
--- CatEpiR : {c : Level } (F : Functor (Sets {c}) (Sets {c}))
---     → {a a' : Obj Sets } {b : Obj Sets} (g h : Hom Sets (FObj F a') b) 
---     → ( ( f : {a a' b : Obj Sets} (g : Hom Sets (FObj F a) b) → Hom Sets a a' )
---         → (Sets [ Sets [ g o FMap F (f  g) ] ≈  Sets [ h o FMap F (f h) ] ] → Sets [ g  ≈ h ]) )
---     → CatSurjective Sets Sets F 
--- CatEpiR  F g h eq = record { sur = λ {a} {a'} g →  sur0 {a} {a'} g ;  surjective = ylem22 } where
---     sur0 : {a a' : Obj Sets} (g : Hom Sets (FObj F a) (FObj F a')) → Hom Sets a a'
---     sur0 {a} {a'} g = {!!}
---     ylem22 :  {a a' : Obj Sets} (g : Hom Sets (FObj F a) (FObj F a')) → Sets [ FMap F (sur0 g) ≈ g ]
---     ylem22 g = begin
---      FMap F (sur0 g) ≈⟨ {!!} ⟩
---      Sets [  FMap F {!!} o FMap F {!!} ]  ≈⟨ {!!} ⟩
---      Sets [ g o Sets [  FMap F {!!} o FMap F {!!} ] ] ≈⟨ {!!} ⟩
---      g ∎ 
---      where
---        open ≈-Reasoning Sets
-
 CatEpi : {c : Level} (F : Functor (Sets {c}) (Sets {c}))
     → (s : CatSurjective Sets Sets F  )
     → {a a' : Obj Sets } {b : Obj Sets} (g h : Hom Sets (FObj F a') b)