Maximilian Doré: Algorithmically finding cells in Kan cubical sets

Abstract

In recent years, logicians have found that identity in a proof-relevant logic is best understood in analogy to homotopy in a topological space. One combinatorial model of spaces are Kan cubical sets, which provide the foundation for cubical type theory, a logic incorporating the connection between logic and topology. A user of cubical type theory often faces the problem of constructing a cell with a given boundary. We study this problem from the point of view of automated reasoning. We give an algorithm solving the decidable problem of finding a cell in a cubical set efficiently in many cases and discuss its complexity. In contrast, in Kan cubical sets the problem of finding a cell with a given boundary is undecidable since they have a richer language for constructing cells. We present some heuristics to tackle this problem in some cases.