Skip to the content.
HoTTLean: Semantics of HoTT in Lean
by S. Awodey, M. Carneiro, S. Hazratpour, J. Hua, W. Nawrocki, S. Rong, S. Woolfson, Y. Xu
Blueprint (PDF)
Blueprint (web)
Documentation
GitHub