Commit 2023-03-17 16:27 530cf1f3

View on Github →

feat: port CategoryTheory.ConcreteCategory.BundledHom (#2740)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/ConcreteCategory/BundledHom.lean

added def CategoryTheory.BundledHom.MapHom

added def CategoryTheory.BundledHom.map

added def CategoryTheory.BundledHom.mkHasForget₂

added structure CategoryTheory.BundledHom