Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-27 04:07 86d686cc

View on Github →

feat(category_theory/category/Groupoid): Add coercion to sort (#12324) Use coercion to type instead of .α

Estimated changes

Modified src/category_theory/category/Groupoid.lean

added theorem category_theory.Groupoid.coe_of

Modified src/topology/homotopy/fundamental_groupoid.lean

modified def fundamental_groupoid.from_top

modified def fundamental_groupoid.to_path

modified def fundamental_groupoid.to_top

Modified src/topology/homotopy/product.lean

modified def fundamental_groupoid_functor.pi_iso

modified def fundamental_groupoid_functor.pi_to_pi_Top

modified def fundamental_groupoid_functor.prod_iso

modified def fundamental_groupoid_functor.prod_to_prod_Top

modified def fundamental_groupoid_functor.proj

modified def fundamental_groupoid_functor.proj_left

modified theorem fundamental_groupoid_functor.proj_left_map

modified theorem fundamental_groupoid_functor.proj_map

modified def fundamental_groupoid_functor.proj_right

modified theorem fundamental_groupoid_functor.proj_right_map