Interactive explorer of the library

Below is an interactive explorer of modules and definitions in agda-unimath. It displays various properties of the nodes in the dependency graph, and also allows you to determine dependencies between individual definitions. Hover over ⓘ for detailed usage instructions.

⚠ The explorer is not optimized for small screens. It may be difficult to control on mobile devices.

The interactive explorer was developed by Job Petrovčič. In addition, Vojtěch Štěpančík, Matej Petković, and Andrej Bauer contributed invaluable suggestions and offered helpful support.

Notes

The explorer is built and deployed outside of the agda-unimath repository, using a fork of Agda. For that reason the definitions in the graph may lag behind the definitions on the website by a few hours.

The explorer has a few known limitations. Most noticeably it doesn’t recognize the open import ... renaming (X to Y) public pattern of exporting definitions, so in particular the foundation.universe-levels module is not shown, and references to UU in the source code show up as references to Agda.Primitive.Set. Note that one of the consequences is that two Props appear in the search results — the first one being Agda.Primitive.Prop, which is Agda’s proof-irrelevant sort and isn’t used anywhere in the library, and the second being agda-unimath’s foundation-core.propositions.Prop, which is the type of homotopy propositions.