colimits): avoid explicit `infer_instance` (#1430)

Commit

6 years ago

fix(algebra/*/colimits): avoid explicit `infer_instance` (#1430) With an explicit universe level Lean can do it automatically.

References

Author

urkud

Committer

mergify[bot]

Parents