This repository was archived by the owner on Jul 24, 2024. It is now read-only.
chore(category_theory): minor cleanup#921
Merged
mergify[bot] merged 1 commit intomasterfrom Apr 11, 2019
Merged
Commits
Commits on Apr 10, 2019
- committed
