Synthetic computability can be traced back to Hyland's work on the Effective topos: in this structure, every function is computable, and as such the computability theory can be considered as an internal theory. This also gives an interpretation of oracles for computability as subtoposes of the effective topos. As synthetic computability is based on topos notions, it is also well suited to type theoretic formalism, which will be our framework. In parallel, Homotopy Type Theory (HoTT) emerged to give a type theoretical notion of synthetic homotopy theory. Inside this theory, the notion of space up to path equivalence is primitive (in opposition to set theory, where sets are the primitive notion). A lot of work has been done in recent years to developp this theory, which leads to the work this talk is based on: a paper by Andrew W. Swan describing an adaptation of synthetic computability in HoTT, and the interpretation of oracles as higher modalities. We will see how these notions arise and how they can be generalized to higher types.