Are Dependent Types in Set Theory Feasible?

Yunsong Yang, Simon Guilloud, Viktor Kunčak

Following the types-as-sets paradigm, we present a mechanized embedding of dependent function types with a hierarchy of universes into schematic first-order logic with equality, wi…