mortberg / cubicaltt

Experimental implementation of Cubical Type Theory
https://arxiv.org/abs/1611.02108
MIT License
571 stars 76 forks source link

Fast normalization algorithm for Brunerie number 😎 #99

Closed cangiuli closed 6 years ago

cangiuli commented 6 years ago

A straightforward extension of the cubical group's current hacking projects at Dagstuhl...

favonia commented 6 years ago

I did a simple profiling of this optimization and it finished even before I ran it! It's so fast that it created some time-space paradox.

martinescardo commented 6 years ago

The correct terminology should be "Brunerie's constant" and you need a Greek letter for it, such as β.

mortberg commented 6 years ago

Thank you Carlo! (closing :))