Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
just to say that we have an entry pi-finite homotopy type
Added some properties of pi-finite types and a reference to the Univalent combinatorics page of the Unimath Project:
Anonymouse
I have adjusted the wording in the Definition section (here) assuming that you did not mean to say that a -finite type has finite homotopy groups (only) up to some degree .
Even so, the definition in its current informal non-type-theoretic form leaves the question why this entry is separate from the existing entry pi-finite homotopy type.
I suggest to either merge into there or else to add some genuine type-theoretic content here.
1 to 4 of 4