Homotopy Type Theory in Lean

被引：12

作者：

van Doorn, Floris ^{[1
]}

von Raumer, Jakob ^{[2
]}

Buchholtz, Ulrik ^{[3
]}

机构：

[1] Carnegie Mellon Univ, Pittsburgh, PA 15213 USA

[2] Univ Nottingham, Nottingham, England

[3] Tech Univ Darmstadt, Darmstadt, Germany

来源：

INTERACTIVE THEOREM PROVING (ITP 2017) | 2017年 / 10499卷

关键词：

Homotopy type theory; Formalized mathematics; Lean; Proof assistants;

D O I：

10.1007/978-3-319-66107-0_30

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We discuss the homotopy type theory library in the Lean proof assistant. The library is especially geared toward synthetic homotopy theory. Of particular interest is the use of just a few primitive notions of higher inductive types, namely quotients and truncations, and the use of cubical methods.

引用

页码：479 / 495

页数：17

共 22 条

[1] Univalent categories and the Rezk completion
Ahrens, Benedikt
Kapulkin, Krzysztof
Shulman, Michael
[J]. MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2015, 25 (05) : 1010 - 1039
[2] Angiuli C., 2017, P 44 ANN ACM SIGPLAN
[3] Homotopy theoretic models of identity types
Awodey, Steve
Warren, Michael A.
[J]. MATHEMATICAL PROCEEDINGS OF THE CAMBRIDGE PHILOSOPHICAL SOCIETY, 2009, 146 : 45 - 55
[4] Bauer Andrej., 2016, The HoTT Library: A formalization of homotopy type theory in Coq
[5] Brunerie G., 2017, HOMOTOPY TYPE THEORY
[6] Buchholtz U., 2016, CAYLEY DICKSON CONST
[7] Cohen C., CUBICAL TYPE THEORY
[8] Cohen Cyril, 2016, 21 INT C TYP PROOFS
[9] de Moura L., 2017, SLIDES
[10] The Lean Theorem Prover (System Description)
de Moura, Leonardo
Kong, Soonho
Avigad, Jeremy
van Doorn, Floris
von Raumer, Jakob
[J]. AUTOMATED DEDUCTION - CADE-25, 2015, 9195 : 378 - 388

← 1 2 3 →