Thanks for the reply! So far indeed it is a bit of manual process and requires quite a bit of discipline so things fit, but IMO it is not as bad as it looks.
Things like effective iso transport are IMO tooling issues so indeed mathematics will depend on CS to provide solutions.
Conversation
This always surprises me as a plus for Lean since transport is so much more natural in HoTT, and UIP is incompatible with univalence. UIP gets you some help but it is still ad-hoc compared to, say, cubical. But Leo is amazing at tools for this kind of thing.
1
OTOH Leo had to hack around the lack of univalence to define congruence, and and his student recently showed that congruence is way more natural in cubical. From this you get e-graphs, from e-graphs you get type-directed search for transport.
1
1
The problem is the overlap of people who understand both cubical and e-graphs is like, one or two people. I've been trying to get Anders on board with this.
In vanilla Coq though you have my work, and you have univalent parametricity, and so on. Just all are external tools.
1
2
I've noticed that it is extremely hard to get people to use external tools. I have a few users but that's it. I tried to use UP and I struggled a lot. I think we need more of this in the standard library.
2
1
I guess I hope that at some point Coq can see better forwards compatibility, and more reproducible, easy to use package management tooling.🤞This is one of the big things that keeps me out of investing time in working with Agda, Coq, OCaml, and Haskell. 😔
1
I do realise this stuff is really hard though, and the funding for this kind of tooling stuff is scarce, and each community is doing the best they can. Just hoping it gets better. Brittle tools are scary!
1
Hoping that stuff like what you are working on could help with upgrading dependencies? Like, even in languages where semver is pervasive, versioning is *hard*! Would be cool if libraries could help you 'upgrade' your existing code at a more fine grained level! 🤩
2
2
Yeah, I saw that! Looks really cool, and I’m glad folks are looking at it! Lots of that stuff rings true as a library maintainer - I often have dilemmas about if behavioural changes are breaking or not.
1
1
Dependently typed langs seem to have even more issues here due to definitional equality exposing implementation details - often they don’t make these details private by default, leading to downstream breakages. 😔