Post #2334004

@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.