Josh Chen

Just to provide a data point, I'm working on things that use HoTT in non-cubical Agda, mostly relying on the core library. I'm grateful for the up-to-date fork!

Looks like this comes from changes to the substitution tactics in Isabelle2021. See - https://isabelle.in.tum.de/dist/Isabelle2021/doc/NEWS.html on "proof method `subst`", as well as - `$ISABELE_HOME/src/Tools/eqsubst.ML`). This results in altered computation behavior...

This is more of a question of how much we want to be able to do metatheory of HoTT inside Isabelle/HoTT. At some point this might be interesting to take...

Yes I did consider this, as you say the two are geared at slightly different approaches :) I'm myself definitely doing things more in the "blog post"/"online standalone paper draft"...

Thanks for the pointers! As Jon suggested, my current use case is more "quickly iterate writeups" than "encyclopedic database"---standalone articles that are meant to be presented more traditionally as a...