This project is joint work with
The project is to answer the question of whether a give type T has a unique
inhabitant modulo a notion of program equivalence.
The question has been answer for the simply typed
lambda-calculus in the presence of sum types and modulo