Commit 2023-11-16 11:33 7c434b46

View on Github →

chore(CategoryTheory): universe polymorphic CategoryTheory.Limits.Types.coproductIso (#8421) Fixes a typo requiring matching universe levels in CategoryTheory.Limits.Types.coproductIso.

Estimated changes

Modified Mathlib/CategoryTheory/GlueData.lean

modified theorem CategoryTheory.GlueData.types_ι_jointly_surjective

Modified Mathlib/CategoryTheory/Limits/Shapes/Types.lean

modified def CategoryTheory.Limits.Types.coproductColimitCocone

modified theorem CategoryTheory.Limits.Types.coproductIso_mk_comp_inv

modified theorem CategoryTheory.Limits.Types.coproductIso_ι_comp_hom