feat(category_theory/limits): special shapes #1339
mergify
merged
41 commits into
master
from
limits-shapes
providing minimal API for limits of special shapes
b56eb60e
apis for special shapes
d53fbece
fintype instances
2de84ddc
associators, unitors, braidings for binary product
0935f0c6
map
7244ebc1
instances
4bf314f5
assoc lemma
0ef49a42
coprod
e122f163
kim-em
changed the title
Merge branch 'master' into limits-shapes
4874a288
fix import
223ad515
names
5cfcddc1
adding some docs
493b4813
updating tutorial on limits
edde84b9
minor
79d79760
uniqueness of morphisms to terminal object
3b225b95
better treatment of has_terminal
e5fa7e20
various
3be27860
not there yet
44fa640a
deleting a dumb file
e940511c
remove constructions for a later PR
e4a4e810
Merge branch 'master' into limits-shapes
b591907c
use @[reassoc]
3aa49a8a
Update src/category_theory/limits/shapes/finite_products.lean
5e6cd69b
improving the colimits tutorial
2df8e635
Merge branch 'limits-shapes' of github.com:leanprover-community/mathl…
3b831f4b
minor
cfda2ac6
notation for `prod_obj` and `sigma_obj`.
f45fc6b1
reverting to `condition`
fab6db3c
implicit arguments
3ba05dcf
more implicit arguments
062cb671
minor
8b4a8b71
notational for initial and terminal objects
b912f497
various
aaf29f1d
fix notation priorities
e0eaedaa
Merge branch 'master' into limits-shapes
a26949f3
remove unused case bash tactic
681e4553
fix whitespace
0b299c20
comment
eac02644
Merge branch 'limits-shapes' of github.com:leanprover-community/mathl…
2dacdd1e
notations
62bad6f5
Merge branch 'master' into limits-shapes
21e02a0a
jcommelin
approved these changes
on 2019-08-30
Reviewers
Assignees
Labels
ready-to-merge
Milestone
No milestone
Login to write a write a comment.
Login via GitHub