Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-06-26 07:16 3cfc0e73

View on Github →

chore(category/*): linting (#3178) Some linting work on category_theory/.

Estimated changes

Modified src/algebra/category/Group/basic.lean

Modified src/category_theory/category/Cat.lean

Modified src/category_theory/concrete_category/bundled.lean

Modified src/category_theory/conj.lean

Modified src/category_theory/const.lean

modified theorem category_theory.functor.const.op_obj_unop_hom_app

modified theorem category_theory.functor.const.op_obj_unop_inv_app

Modified src/category_theory/core.lean

Modified src/category_theory/currying.lean

Modified src/category_theory/elements.lean

Modified src/category_theory/eq_to_hom.lean

Modified src/category_theory/full_subcategory.lean

Modified src/category_theory/fully_faithful.lean

Modified src/category_theory/functor.lean

deleted def category_theory.functor.ulift_down

deleted def category_theory.functor.ulift_up

Modified src/category_theory/functor_category.lean

Modified src/category_theory/isomorphism.lean

Modified src/category_theory/natural_isomorphism.lean

deleted def category_theory.functor.ulift_down_up

deleted def category_theory.functor.ulift_up_down

Modified src/category_theory/natural_transformation.lean

modified structure category_theory.nat_trans

Modified src/category_theory/products/associator.lean

modified def category_theory.prod.associator

modified def category_theory.prod.inverse_associator

Modified src/category_theory/punit.lean

Modified src/category_theory/single_obj.lean

Modified src/category_theory/sums/associator.lean

modified def category_theory.sum.associator

modified def category_theory.sum.inverse_associator