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.
<style> .sidetoc { display: none; } @media(max-width:1100px) { #small-display-notice { display: block !important; } } </style>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.
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.