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.
I tried to brush-up the entry fundamental infinity-groupoid which had been in a rather sorry state. Some things I did:
stated the definition (!) $Sing X$
removed Ronnie’s remark that there is a problem with this definition due to lack of chosen fillers and instead added Thomas Nikolaus’s theorem that when you choose fillers to get an algebraic Kan complex $\Pi X$ there is (still) a direct proof of the homotopy hypothesis
made the statement that $Sing X$ is equivalently computed by the abstract $\infty$-topos-theoretic definition of fundamental $\infty$-groupoid a formal proposition.
That looks good. I added a comment before the definition to the effect that we’re choosing Kan complexes as a notion of $\infty$-groupoid in order to make that definition.
1 to 2 of 2