Formalizing Type Operations Using the "Image" Type Constructor