Unbounded π-finite types

UniMath / agda-unimath

The agda-unimath library

https://unimath.github.io/agda-unimath/

MIT License

222 stars 71 forks source link

Unbounded π-finite types #1168

Open fredrik-bakke opened 2 months ago

fredrik-bakke commented 2 months ago

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 commented 2 months ago

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 commented 2 months ago

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

EgbertRijke commented 2 months ago

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 commented 2 months ago

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.*