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

proofs about HIT-style integers #469

Closed ecavallo closed 5 years ago

ecavallo commented 5 years ago

Right now I've proven that int is equivalent to biinv-int, which is generated by a point and a bi-invertible endomap (i.e., a map with a left and right inverse). This is easier than proving int is equivalent to the HIT generated by a point and a half-adjoint equivalence (the way it is typically presented), because biinv-int only has 0- and 1-dimensional generators.

However, I suspect it will be straightforward to show that biinv is equivalent to the half-adjoint version just using the standard theorems that the different definitions of equivalence are interchangeable. ETA: Maybe not.

ecavallo commented 5 years ago

Turns out I don't know how to get from the bi-invertible map integers to the half-adjoint equivalence integers, so I'm just going to merge this now.