该库旨在以单值视角来形式化大量数学内容。
This rocq library aims to formalize a substantial body of mathematics using the univalent point of view.
