UniMath
Coqライブラリで、
Univalent Foundations
を用いて定理を形式化しているライブラリ。
「形式化」とは、定理の証明の各ステップで、どの推論規則や公理が使われたかを例外なく全て記録すること
GitHub:
GitHub - UniMath/UniMath: This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
Learning Material for Univalent Mathematics and the UniMath library | UniMath School Materials (2022)
確認用
Q. UniMath
参考
関連
Univalent Foundations
Homotopy Type Theory(HoTT)
#GitHub
#Coq
#数学