Skip to the content.
HoTTLean : Formalizing the Meta-Theory of HoTT in Lean
by S. Awodey, M. Carneiro, S. Hazratpour, J. Hua, W. Nawrocki, S. Woolfson, Y. Xu
Blueprint (web)
Documentation
GitHub
Useful links:
Zulip chat for Lean
for coordination
Blueprint
Blueprint as pdf
Dependency graph
Doc pages for this repository