Commit 2021-08-25 05:54 bd9622fa

View on Github →

chore(category_theory/Fintype): Fix universe restriction in skeleton (#8855) This removes a universe restriction in the existence of a skeleton for the category Fintype. Once merged, Fintype.skeleton.{u} will be a (small) skeleton for Fintype.{u}, with u any universe parameter.

Estimated changes