search

RedPRL / redtt

"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
Apache License 2.0
204 stars 12 forks source link

^cooler^ invariance example #422

Closed cangiuli closed 6 years ago

cangiuli commented 6 years ago

With lots of help from @jonsterling and @ecavallo.

cangiuli commented 6 years ago

@favonia @ecavallo So, @jonsterling and I wrote a bunch of really gnarly proofs but we're still stuck and somehow I suspect there's an easier way to do all of this. Does someone want to take a look at how to prove the direct version of nat->list/is-equiv'?

cangiuli commented 6 years ago

Although it's not fully perfected, I think it might be time to merge this stuff.