λP2 = λC : Who Needs Type Constructors This is an attempt to prove an injective map from the Calculus of Constructions to System λP2 from the lambda cube.