Unbounded π-finite types

[fredrik-bakke]

Defines unbounded π-finite types and repeats the proofs that are already done for π-finite types. This includes

• Unbounded π-finite types are closed under equivalences and retracts.
• Truncated π-finite types are unbounded π-finite.
• Unbounded π-finite types are types that are πₙ-finite for all $n$.
• Unbounded π-finite types are closed under coproducts.
• Unbounded π-finite types are closed under finite products.
• Unbounded π-finite types are closed under dependent sums.

[fredrik-bakke]

As far as I can tell from reading the literature, π-finiteness refers to what is called truncated π-finite in our formalizations. Does this vary depending on authors, or should I change around the naming in our formalization? If so, a potential name for types that have finite homotopy sets up to dimension n that I can think of is "π-prefinite".

[fredrik-bakke]

Another potential option is "Kuratowski $n$-finite", I suppose. @EgbertRijke

[EgbertRijke]

I'll have a look in the coming days at this pull request. I'm aware of a mismatch between our naming and the literature, and this should change at some point in another pull request.

To be pi-finite should mean that the type is k-truncated for some k and that all the homotopy groups are finite.

[fredrik-bakke]

Thanks! There's currently no rush. Another name that seems to fit with the literature is "π-finitely indexed", since it must mean a π-finite type maps onto the type by a map that is connected enough.*

[EgbertRijke]

Sorry that I left this PR hanging for so long. I'm happy with the overall PR, and just had two remarks.

[fredrik-bakke]

Thanks! I'll have a look in the morning. If it's not a bother, do you have an opinion on the "truncated pi-finite" vs. "pi-finite" question I asked about above?

[fredrik-bakke]

I mean, du you have a preferred name for types whose homotopy groups up to a finite dimension are finite?

[EgbertRijke]

I mean, du you have a preferred name for types whose homotopy groups up to a finite dimension are finite?

Probably we should align our terminology with the literature:

• pi-finite means finite homotopy groups and truncated for some unspecified truncation level (I got that wrong in my original formalization).
• If it is only required that the homotopy groups up to some level are finite and no condition otherwise, perhaps we could call that untruncated-pi-finite

That said, I don't want to impose any terminology changes in this pull request. This PR already contains valuable work that deserves to be merged.