mathlib3
feat(category_theory/limits): support for special shapes of (co)limits
#938
Merged
Merged
feat(category_theory/limits): support for special shapes of (co)limits #938
kim-em
merged
43 commits into
master
from
limits-shapes
feat(category_theory): working in Sort rather than Type, as far as po…
5f3f0778
missed one
416e3cdb
adding a comment about working in Type
759bcc8b
remove imax
0c54fe64
removing `props`, it's covered by `types`.
6f73dc76
fixing comment on `rel`
161bc34e
tweak comment
0621ecc2
add matching extend_π lemma
2331595b
remove unnecessary universe annotation
1a0ba295
another missing s/Type/Sort/
45f07220
feat(category_theory/shapes): basic shapes of cones and conversions
b4f017e3
Moving into src. Everything is borked.
c1586e37
investigating sparse
71518323
blech
867c5b3a
maybe working again?
628753a9
removing terrible square/cosquare names
7090d7c0
merge
4322d492
renaming
2e7ab10d
minor, mostly to make appveyor try again
368f199a
Update src/category_theory/limits/shapes/pullbacks.lean
3700b96f
namespacing, adding comment about mysterious missing simp lemma
7608185b
formnatting
a25a0b53
first cut of a tutorial on using special shapes of limits
75fd6eff
add a TODO
fee72e42
fixing the tutorial on colimits in Top
456f264c
merge
4c7e7cd0
oops
76aa5849
comment
7303838a
Merge branch 'master' into limits-shapes
ebdeab80
Merge branch 'master' into limits-shapes
7bfe26d9
various
d8228b0e
removing obsolete comment
838189ff
ugh.. there is still so much inconsistency here
83c5ae44
Update products.lean
fd1528fa
Update products.lean
403b993b
trying to make everything uniform
a9897ce6
Merge branch 'limits-shapes' of github.com:leanprover-community/mathl…
f83176c0
Merge commit '6956daa2aa90bf84de0ebce5be25ad1a8b4a9b9b' into limits-s…
23ca4b65
jcommelin
dismissed these changes
on 2019-05-03
reducing imports
0d48ab5a
jcommelin
dismissed these changes
on 2019-05-03
fix imports
0c3939d1
jcommelin
approved these changes
on 2019-05-03
Merge branch 'master' into 'limits-shapes'
f5dcb695
Merge branch 'master' into 'limits-shapes'
08e98c95
Merge branch 'master' into 'limits-shapes'
de7f228a
Login to write a write a comment.