We propose a talk about runtime system that exploits path structures in HITs to implement a more efficient garbage collection mechanism, capable of replacing equivalent object representations in memory to reduce allocation overhead.

Our proof-of-concept is based on Cubical Type Theory and its implementation in cubicaltt, and the proposed runtime system is integrated into the normalization engine of the typechecker.