Titouan Leclercq: Oracle modalities for higher dimensional types

Titouan Leclercq – École Normale Supérieure de Lyon (joint work with Andrew Swan)

Abstract: Based on Andrew Swan’s work on oracle modalities, cubical type theory is suited to work synthetically on Turing degrees. However, Turing degrees are focused on sets, while cubical type theory can talk about higher dimensional types. This work aims to give a more general construction of oracles that allows computation on types with nontrivial homotopical data, and study an adapted notion of computably enumerable sets, for which we prove that it is the expected notion on propositions.