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
returning to filtered colimits
db2d0b0f
colimits in Mon
9a15a413
rename
b56c42df
actually jump through the final hoop
07a5e844
experiments
f7139591
fixing use of ext
6758c01f
feat(colimits): colimits in Mon and CommRing
ca28a04d
merge
f35a28aa
fixes
d516ffe8
removing stuff I didn't mean to have in here
227ff21e
minor
b46295d7
fixes
4ac62ff6
merge
2755951e
merge
89a914d0
update after merge
b4384898
fix import
01da3604
Merge branch 'master' into colimits
9da9ec6f
jcommelin
commented
on 2019-05-02
jcommelin
approved these changes
on 2019-05-04
Merge branch 'master' into 'colimits'
a9ed733d
Login to write a write a comment.
Login via GitHub