search

mortberg / cubicaltt

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

Implement girard's paradox to show impredicativity of cubicaltt #40

Closed abooij closed 7 years ago

abooij commented 8 years ago

it's not 100% clean (the types in the lambdas aren't expressed cleanly), so if you'd prefer that please let me know.

mortberg commented 8 years ago

This is not really using any cubical features, so maybe it should go into experiments instead of examples?

mortberg commented 7 years ago

I'll merge, but then move to experiments.