mathlib3

65bf45c9 - fix(category_theory/finite_limits): fix definition, and construct from finite products and equalizers (#1427)

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