PR #2126 fix(algebra/category): avoid deprecated lemmas

fix(algebra/category): avoid deprecated lemmas #2126

mergify merged 1 commit into master from colimits_deprecated_lemmas

fix(algebra/category): avoid deprecated lemmas

3bbc0f8f

jcommelin approved these changes on 2020-03-11

jcommelin added ready-to-merge

mergify merged d909a612 into master 5 years ago

mergify deleted the colimits_deprecated_lemmas branch 5 years ago

Reviewers

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone