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