PR #921 chore(category_theory): minor cleanup

chore(category_theory): minor cleanup #921

mergify merged 1 commit into master from category-fixes

minor changes

670432c9

kim-em requested a review 6 years ago

rwbarton approved these changes on 2019-04-11

rwbarton added ready-to-merge

mergify merged 22fcb4e9 into master 6 years ago

mergify deleted the category-fixes branch 6 years ago

Reviewers

rwbarton

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone