ホモトピー型理論は既にLeanにもライブラリがある