Skip to the content.

Groupoid Model of HoTT in Lean 4

by Authors

Blueprint (web) Documentation GitHub

Useful links:

Zulip chat for Lean for coordination
Blueprint
Blueprint as pdf
Dependency graph
Doc pages for this repository

groupoid_model_in_lean4 is maintained by Authors. Visit the GitHub repository for more information.