Maximilian Doré : Searching for Kan fillers with poset maps
Time: Wed 2022-09-28 11.00 - 12.00
Location: Albano house 1, floor 3, Room U (Kovalevsky)
Lecturer: Maximilian Doré (University of Oxford)
A central reasoning principle in cubical type theories is the notion Kan composition: In order to construct a filler with a certain boundary, one constructs a higher-dimensional box whose open side has the boundary under question. Since types in cubical type theories are Kan complexes, we will then have a term which acts as Kan composition of that box. We explore this reasoning principle from the point of view of computational logic and present strategies to search for boxes systematically. Using constraint satisfaction, we can solve most examples in lower dimensions. In higher dimensions, the number of degeneracies increases superexponentially. We present work in progress which uses the correspondence of degeneracies of De Morgan cubes with poset maps to represent the search space efficiently. This opens up the possibility to also search for boxes in higher dimensions.