UniMath/agda-unimath

Show that the type of Ferrers diagrams of any finite type is π-finite

fredrik-bakke opened this issue · 0 comments

fredrik-bakke commented

The following is waiting to be formalized in univalent-combinatorics.ferrers-diagrams:

  • The type of Ferrers diagrams of any finite type is π-finite