chore(category_theory/cones): make functor argument of forget explicit (

#2128)

src/category_theory/limits/cones.lean

@@ -249,8 +249,13 @@ begin
   { refine (postcompose_comp _ _).symm.trans _, rw [iso.inv_hom_id], exact postcompose_id }
 end
 
-@[simps] def forget : cone F ⥤ C :=
+section
+variable (F)
+
+@[simps]
+def forget : cone F ⥤ C :=
 { obj := λ t, t.X, map := λ s t f, f.hom }
+end
 
 section
 variables {D : Type u'} [𝒟 : category.{v} D]
@@ -307,8 +312,13 @@ begin
   { refine (precompose_comp _ _).symm.trans _, rw [iso.hom_inv_id], exact precompose_id }
 end
 
-@[simps] def forget : cocone F ⥤ C :=
+section
+variable (F)
+
+@[simps]
+def forget : cocone F ⥤ C :=
 { obj := λ t, t.X, map := λ s t f, f.hom }
+end
 
 section
 variables {D : Type u'} [𝒟 : category.{v} D]

src/category_theory/limits/shapes/equalizers.lean

@@ -328,7 +328,7 @@ def limit_cone_parallel_pair_self_is_iso (c : cone (parallel_pair f f)) (h : is_
   is_iso (c.π.app zero) :=
   let c' := cone_parallel_pair_self f,
     z : c ≅ c' := is_limit.unique_up_to_iso h (is_limit_cone_parallel_pair_self f) in
-  is_iso.of_iso (functor.map_iso cones.forget z)
+  is_iso.of_iso (functor.map_iso (cones.forget _) z)
 
 /-- The equalizer of (f, f) is an isomorphism -/
 def equalizer.ι_of_self [has_limit (parallel_pair f f)] : is_iso (equalizer.ι f f) :=
@@ -422,7 +422,7 @@ def colimit_cocone_parallel_pair_self_is_iso (c : cocone (parallel_pair f f)) (h
   is_iso (c.ι.app one) :=
   let c' := cocone_parallel_pair_self f,
     z : c' ≅ c := is_colimit.unique_up_to_iso (is_colimit_cocone_parallel_pair_self f) h in
-  is_iso.of_iso $ functor.map_iso cocones.forget z
+  is_iso.of_iso $ functor.map_iso (cocones.forget _) z
 
 /-- The coequalizer of (f, f) is an isomorphism -/
 def coequalizer.π_of_self [has_colimit (parallel_pair f f)] : is_iso (coequalizer.π f f) :=

src/category_theory/limits/shapes/kernels.lean

@@ -103,7 +103,7 @@ def kernel.is_limit_cone_zero_cone [mono f] : is_limit (kernel.zero_cone f) :=
 
 /-- The kernel of a monomorphism is isomorphic to the zero object -/
 def kernel.of_mono [has_limit (parallel_pair f 0)] [mono f] : kernel f ≅ 0 :=
-functor.map_iso cones.forget $ is_limit.unique_up_to_iso
+functor.map_iso (cones.forget _) $ is_limit.unique_up_to_iso
   (limit.is_limit (parallel_pair f 0)) (kernel.is_limit_cone_zero_cone f)
 
 /-- The kernel morphism of a monomorphism is a zero morphism -/
@@ -169,7 +169,7 @@ def cokernel.is_colimit_cocone_zero_cocone [epi f] : is_colimit (cokernel.zero_c
 
 /-- The cokernel of an epimorphism is isomorphic to the zero object -/
 def cokernel.of_epi [has_colimit (parallel_pair f 0)] [epi f] : cokernel f ≅ 0 :=
-functor.map_iso cocones.forget $ is_colimit.unique_up_to_iso
+functor.map_iso (cocones.forget _) $ is_colimit.unique_up_to_iso
   (colimit.is_colimit (parallel_pair f 0)) (cokernel.is_colimit_cocone_zero_cocone f)
 
 /-- The cokernel morphism if an epimorphism is a zero morphism -/
@@ -196,12 +196,12 @@ local attribute [instance] zero_of_zero_object
 local attribute [instance] has_zero_object.zero_morphisms_of_zero_object
 
 /-- The kernel of the cokernel of an epimorphism is an isomorphism -/
-def kernel.of_cokernel_of_epi [has_colimit (parallel_pair f 0)]
+instance kernel.of_cokernel_of_epi [has_colimit (parallel_pair f 0)]
   [has_limit (parallel_pair (cokernel.π f) 0)] [epi f] : is_iso (kernel.ι (cokernel.π f)) :=
 equalizer.ι_of_self' _ _ $ cokernel.π_of_epi f
 
 /-- The cokernel of the kernel of a monomorphism is an isomorphism -/
-def cokernel.of_kernel_of_mono [has_limit (parallel_pair f 0)]
+instance cokernel.of_kernel_of_mono [has_limit (parallel_pair f 0)]
   [has_colimit (parallel_pair (kernel.ι f) 0)] [mono f] : is_iso (cokernel.π (kernel.ι f)) :=
 coequalizer.π_of_self' _ _ $ kernel.ι_of_mono f