Unique inhabitants

This project is joint work with Gabriel Scherer 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 beta-eta-equivalence. See the ICFP paper and its extended version