Skip to content

Commit

Permalink
chore(category_theory/limits): remove an unnecessary import (#3357)
Browse files Browse the repository at this point in the history
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
  • Loading branch information
semorrison and semorrison committed Jul 10, 2020
1 parent 699c915 commit d1e63f3
Showing 1 changed file with 0 additions and 1 deletion.
1 change: 0 additions & 1 deletion src/category_theory/limits/shapes/biproducts.lean
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,6 @@ Copyright (c) 2019 Scott Morrison. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Scott Morrison
-/
import category_theory.epi_mono
import category_theory.limits.shapes.finite_products
import category_theory.limits.shapes.binary_products
import category_theory.preadditive
Expand Down

0 comments on commit d1e63f3

Please sign in to comment.