その2。 ホモトピー群とEckmann-Hilton argument 型がweak ∞-groupoidだということが分かったので、weak ∞-groupoidに対して、ホモトピー群というものを定義する。type theory的には、ホモトピー群を定義する動機はあまりないけど、数学にinspireされて、(意…