Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-15 20:41 f953a9d1

View on Github →

feat(category_theory/limits/shapes/types): duals (#3738) Just dualising some existing material.

Estimated changes

Modified src/category_theory/limits/shapes/types.lean

added theorem category_theory.limits.types.coprod

added theorem category_theory.limits.types.coprod_desc

added theorem category_theory.limits.types.coprod_inl

added theorem category_theory.limits.types.coprod_inr

added theorem category_theory.limits.types.coprod_map

added theorem category_theory.limits.types.initial

added theorem category_theory.limits.types.sigma

added theorem category_theory.limits.types.sigma_desc

added theorem category_theory.limits.types.sigma_map

added theorem category_theory.limits.types.sigma_ι

added def category_theory.limits.types.types_has_binary_coproducts

added def category_theory.limits.types.types_has_coproducts

added def category_theory.limits.types.types_has_initial