search

UniMath / agda-unimath

The agda-unimath library
https://unimath.github.io/agda-unimath/
MIT License
219 stars 70 forks source link

Add interactive library explorer #1138

Open VojtechStep opened 4 months ago

VojtechStep commented 4 months ago

@JobPetrovcic created an interactive graph for exploring definitions in the library. This PR embeds the explorer on our website.

Some more work is still required outside of this repository, which is why this PR is a draft.

Co-authored-by: Job Petrovčič job1.petrovcic@gmail.com

VojtechStep commented 1 month ago

Status update: we're coordinating with Job, his implementation should now be feature-complete and we're just figuring out some UX details. One of the killer features is tracking deep dependencies; for example, we can now directly see that the proof of funext from univalence doesn't cheat by using funext! The eq-htpy axiom is "observed"/"focused", and the popup says that funext-univalence doesn't contain it in its dependency closure. But it does depend on univalence, as shown in the second screenshot. 20240817 194800 screen 20240817 200026 screen

fredrik-bakke commented 2 days ago

~The WIP interactive explorer can be accessed here: https://jobpetrovcic.github.io/visualize~

EDIT: See up-to-date link below.

fredrik-bakke commented 2 days ago

@VojtechStep Can this interactive explorer tell you if a certain rewrite rule was used in the definition of an entry?

JobPetrovcic commented 2 days ago

Oops, I forgot to delete the link you mentioned, @fredrik-bakke. That one is from when we were testing stuff.

Here is the up-to-date link: https://jobpetrovcic.github.io/Unimath-Visualization-Deployment/visualize.html

fredrik-bakke commented 2 days ago

Oh, thank you!