From Cubes to Twisted Cubes via Graph Morphisms in Type Theory

Gun Pinyo, Nicolai Kraus

Cube categories are used to encode higher-dimensional categorical structures. They have recently gained significant attention in the community of homotopy type theory and univalent…