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

Internally prove whether or not "axiom K" can be derived? #249

Closed markfarrell closed 8 years ago

markfarrell commented 8 years ago

As another exercise, I wonder if it can be proved/disproved whether "axiom K" can/cannot be derived in JonPRL, following the work in examples/identity-types.jonprl. If "axiom K" can be derived as a theorem, wouldn't that limit what can be developed in terms of higher type theory inside of JonPRL?

jozefg commented 8 years ago

It can: higher type theory is not exactly an option yet for CTT (active area of research though). In JonPRL we just have UIP as a rule so K is a pretty easy consequence to get. Remember that CTT has the policy that the standard PER model that the meaning explanation gives rise to is the type theory. This means that groupoids were never really intended nor can they be an interesting model of this formulation of CTT.

markfarrell commented 8 years ago

Ah ok, thanks.