KnowledgeBase » 
PUBLICATION
» ID = 774
Formalization of Cubical Type Theory in Nuprl
by Mark Bickford
2020
We report on the results of a two year project to formalize the semantics of cubical type theory in Nuprl. We were able to interpret cubical type theory (without higher inductive types) in Nuprl's extensional constructive type theory, thus verifying that a univalent higher dimensional type theory can be given a purely constructive interpretation.The univalence axiom is provable in cubical type theory from the rules for the Glue type. Verifying the rules for the Glue type led to the largest proofs ever done in Nuprl. We also began an investigation into how to relate synthetic higher dimensional type theory with constructive analysis and discovered that the intuitionistic theory of analysis (using the FAN theorem and the continuity principle) makes building a connection between the two theories much easier.