mathlib3
feat(category_theory): finite products give a monoidal structure
#1340
Merged
Merged
feat(category_theory): finite products give a monoidal structure #1340
mergify
merged
38 commits into
master
from
monoidal_of_has_products
providing minimal API for limits of special shapes
b56eb60e
apis for special shapes
d53fbece
start
c7c566ef
fintype instances
2de84ddc
merge
025fdb6c
copy-paste from monoidal-categories-reboot
018745b7
associators, unitors, braidings for binary product
0935f0c6
merge
4b304563
minor
479ab28d
minor
fe225c33
map
7244ebc1
merge
8f5f1951
minor
762825f0
instances
4bf314f5
blah
892f39e7
blah
a8ef1ced
chore(category_theory/monoidal): monoidal_category doesn't extend cat…
d281a49f
merge
4706a069
minor
44aefd2e
minor
4e946539
assoc lemma
0ef49a42
nearly there
59008869
coprod
e122f163
merge
19c61879
done?
d97773b9
Merge branch 'master' into limits-shapes
4874a288
Merge branch 'master' into monoidal_of_has_products
3f983812
fix import
223ad515
merge
4901c104
names
5cfcddc1
merge
6305d416
cleanup
2b7ead58
kim-em
changed the title
kim-em
changed the title
merge
4212f659
fix reassoc
4eed4073
comments
c459ebf8
Merge remote-tracking branch 'origin/master' into monoidal_of_has_pro…
481ecc6b
comments
d5b7f646
jcommelin
approved these changes
on 2019-09-04
![mergify[bot]](https://avatars.githubusercontent.com/in/10562?v=4&s=60)
Merge branch 'master' into monoidal_of_has_products
d18ddc00
Reviewers
Labels
ready-to-merge
Milestone
No milestone
Login to write a write a comment.
Login via GitHub