mathlib3
fix(category_theory): remove duplication of unitors and associators for functors
#971

Merged

fix(category_theory): remove duplication of unitors and associators for functors #971

mergify merged 1 commit into master from unitor-deduplication

remove code duplication

13efd729

kim-em requested a review 6 years ago

jcommelin added ready-to-merge

jcommelin approved these changes on 2019-05-03

mergify merged 3eb7ebca into master 6 years ago

mergify deleted the unitor-deduplication branch 6 years ago

Reviewers

jcommelin

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone