On fuzzy type theory

This paper is a generalization of classical (simple) type theory. We have developed a formal system of fuzzy type theory which differs from the classical one essentially in extension of truth values from two to infinitely many. The structure of truth values is assumed to be an IMTL-algebra (residuated lattice with prelinearity and double negation) extended by the Baaz delta operation. Various properties of fuzzy type theory are proved including its completeness.