search

jonsterling / JonPRL

An proof refinement logic for computational type theory. Inspired by Nuprl. [For up-to-date development, see JonPRL's successor, RedPRL: https://github.com/redprl/sml-redprl]
http://www.jonprl.org
MIT License
109 stars 9 forks source link

Formalization of Cubical Type Theory #251

Open markfarrell opened 8 years ago

markfarrell commented 8 years ago

A project idea: replicate Mark Bickford's formalization of cubical type theory in JonPRL. See: http://www.nuprl.org/wip/Mathematics/cubical!type!theory/index.html

Thoughts?

jonsterling commented 8 years ago

I've been hoping we could do something along those lines as well...

After trying to do a category theory development in Classic JonPRL, I found our treatment of universes very frustrating—and the lack of records is a big problem (Mark uses Sigma types in the Nuprl development, which makes things fairly gnarly too).

I hope that we can try again in Red JonPRL and have a better time of it.

jonsterling commented 8 years ago

(Since our treatment of universes is corrected now, and I am thinking that it may be possible to give a nicer treatment to records than is possible in Nuprl or Classic JonPRL).