--- a/src/yoneda.agda	Tue Mar 09 14:18:06 2021 +0900
+++ b/src/yoneda.agda	Tue Mar 09 14:51:17 2021 +0900
@@ -346,29 +346,29 @@
 
 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 = λ g → {!!}  ;  surjective = {!!} } where
-    ylem22 :  {a a' : Obj A} (i : Hom B (FObj F a) (FObj F a')) → B [ FMap F {!!} ≈ i ]
+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 : Hom Sets a a' )
+    → (Sets [ Sets [ g o FMap F f ] ≈  Sets [ h o FMap F f ] ] → Sets [ g  ≈ h ])
+    → CatSurjective Sets Sets F 
+CatEpiR  F g h f eq = record { sur = λ g → {!!}  ;  surjective = {!!} } where
+    ylem22 :  {a a' : Obj Sets} (i : Hom Sets (FObj F a) (FObj F a')) → Sets [ FMap F {!!} ≈ i ]
     ylem22 i = begin
      FMap F {!!} ≈⟨ {!!} ⟩
      i ∎ 
      where
-       open ≈-Reasoning B
+       open ≈-Reasoning Sets
 
-CatEpi : { c₁ c₂ ℓ c₁' c₂' ℓ' : Level} ( A : Category c₁ c₂ ℓ ) ( B : Category c₁' c₂' ℓ' ) (F : Functor A B)
-    → (s : CatSurjective A B F )
-    → {a a' : Obj A } {b : Obj B} (g h : Hom B (FObj F a') b)
-    → (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
+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)
+    → (f : {a a' : Obj Sets } {b : Obj Sets} (g h : Hom Sets (FObj F a') b) → Hom Sets a a' )
+    → Sets [ Sets [ g o FMap F (f {a} {a'} g h ) ] ≈  Sets [ h o FMap F (f g h )] ] → Sets [ g  ≈ h ]
+CatEpi F s g h f eq = begin
      g ≈⟨ {!!} ⟩
      h ∎ 
   where
-     open ≈-Reasoning B
+     open ≈-Reasoning Sets
      -- 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))