Commit 2019-09-02 12:18 57d4b411
View on Github →feat(category_theory/limits): construct limits from products and equalizers (#1362)
- providing minimal API for limits of special shapes
- apis for special shapes
- fintype instances
- associators, unitors, braidings for binary product
- map
- instances
- assoc lemma
- coprod
- fix import
- names
- adding some docs
- updating tutorial on limits
- minor
- uniqueness of morphisms to terminal object
- better treatment of has_terminal
- various
- not there yet
- deleting a dumb file
- remove constructions for a later PR
- getting there
- oops
- of_nat_iso
- feat(category_theory/limits/of_nat_isp)
- progress on limits from products and equalizers
- Update src/category_theory/limits/limits.lean Co-Authored-By: Johan Commelin johan@commelin.net
- Update src/category_theory/limits/limits.lean Co-Authored-By: Johan Commelin johan@commelin.net
- use @[reassoc]
- fixing after rename
- use @[reassoc]
- fix renaming
- complete construction of limits from products and equalizers
- cleanup
- cleanup
- name instance
- whitespace
- Update src/category_theory/limits/limits.lean Co-Authored-By: Johan Commelin johan@commelin.net
- use simpa