Post #2334000
2026-05-05 15:39 UTC
And, by the way, if you really want a nice proof assistant for pure non-cubical HoTT where there is no cubical anything, I'm building it. But it will take some time.
Replies (4)
-
@5ht@mathstodon.xyz 2026-05-05 17:12
@jonmsterling@mathstodon.xyz Previous was not finished, I expect the similar destiny of followed project. The trail of not finished projects is prolongating. OK. The success story of Bauer's zoo.
-
@ToucanIan@mathstodon.xyz 2026-05-05 18:30
@jonmsterling@mathstodon.xyz looking forward to trying it as I am onboard with a lot of your goals!
-
@apostolis@social.coop 2026-05-05 18:47
@jonmsterling@mathstodon.xyz I also want non cubical hott, but I also want things to compile. Will this be possible with pterodactyl? As far as I know, the emphasis is on the theorem prover part, not the programming language part.
-
@ltchen@mathstodon.xyz 2026-05-11 08:11
@jonmsterling@mathstodon.xyz I wonder if regularity holds... 🙂