Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-21 05:12 3edb6a4a

View on Github →

fix(category_theory/concrete): access the carrier type by the coercion (#2473) This should marginally reduce the pain of using concrete categories, as the underlying types of a bundled object should more uniformly described via a coercion, rather than the projection. (There's still some separate pain involving bundled.map, but it has an orthogonal fix which I'm working on in another branch.)

Estimated changes