Maximilian Doré: Algorithmically finding cells in Kan cubical sets
Tid: On 2023-03-01 kl 13.30
Plats: Albano, Kovalevsky room
Medverkande: Maximilian Doré (University of Oxford)
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.