That's not an application of category theory. The important theorem here is that the fundamental group is a functor, plus computations of the fundamental group of the disc and the circle. But that's a theorem from topology, not a theorem from category theory. Category theory is merely used as a language, to give the proof a structure.

By that I don't want to say category theory is useless. But regarding the video it's neither necessary, nor an application of category theory.

> Proceed to link to a non-constructive proof

Why are mathematicians like this?