Can We Formalise Type Theory Intrinsically without Any Compromise? A Case Study in Cubical Agda.

Liang-Ting Chen, Fredrik Nordvall Forsberg, Tzu-Chun Tsai

Browse the full CPP paper archive.