From Reversible Programs to Univalent Universes and Back
- Additional Document Info
- View All
We establish a close connection between a reversible programming language
based on type isomorphisms and a formally presented univalent universe. The
correspondence relates combinators witnessing type isomorphisms in the
programming language to paths in the univalent universe; and combinator
optimizations in the programming language to 2-paths in the univalent universe.
The result suggests a simple computational interpretation of paths and of
univalence in terms of familiar programming constructs whenever the universe in
question is computable.