Commit 2019-09-21 06:12 65bf45c9
View on Github →fix(category_theory/finite_limits): fix definition, and construct from finite products and equalizers (#1427)
- chore(category_theory): require morphisms live in Type
- move back to Type
- fix(category_theory/finite_limits): fix definition, and construct from finite products and equalizers
- fixes
- fix duplicate name
- make fin_category a mixin
- fix
- fix
- oops
- fixes
- oops missing universe change
- finish documentation
- fix namespace
- move variables to the right place
- don't repeat yourself
- update module doc-string now that the files have been merged
- inlining has_limit instances