successor on biinv-int which cancels pred exactly

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

Closed ecavallo closed 5 years ago

ecavallo commented 5 years ago

@mortberg

Turns out it is entirely possible, just requires some IH-strengthening. I did suc, but pred wouldn't be any harder.

mortberg commented 5 years ago

Woah! And you convinced me that it wasn't possible today...

mortberg commented 5 years ago

Can you use these integers in the proof that Omega(S1) = Int ? If I remember correctly I think it will simplify the loop case of https://github.com/RedPRL/redtt/blob/master/library/paths/s1.red#L106

mortberg commented 5 years ago

I think my idea was that you don't need to compose with pred-isuc as it's definitional

ecavallo commented 5 years ago

Well, you would have to rewrite everything that does case analysis on int first...

mortberg commented 5 years ago

Yeah, my prediction is that that will be quite a nightmare with these integers...