chore(category_theory/limits): make fin_category_opposite an instance (…

…#12153)
leanprover-community · Feb 21, 2022 · d0fa7a8 · d0fa7a8
1 parent b04851f
commit d0fa7a8
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 3 deletions.
diff --git a/src/category_theory/fin_category.lean b/src/category_theory/fin_category.lean
@@ -91,7 +91,8 @@ open opposite
 /--
 The opposite of a finite category is finite.
 -/
-def fin_category_opposite {J : Type v} [small_category J] [fin_category J] : fin_category Jᵒᵖ :=
+instance fin_category_opposite {J : Type v} [small_category J] [fin_category J] :
+  fin_category Jᵒᵖ :=
 { decidable_eq_obj := equiv.decidable_eq equiv_to_opposite.symm,
   fintype_obj := fintype.of_equiv _ equiv_to_opposite,
   decidable_eq_hom := λ j j', equiv.decidable_eq (op_equiv j j'),

diff --git a/src/category_theory/limits/opposites.lean b/src/category_theory/limits/opposites.lean
@@ -162,8 +162,6 @@ begin
   apply_instance
 end
 
-local attribute [instance] fin_category_opposite
-
 lemma has_finite_colimits_opposite [has_finite_limits C] :
   has_finite_colimits Cᵒᵖ :=
 { out := λ J 𝒟 𝒥, by { resetI, apply_instance, }, }