Abstract
The present paper is a commentary on O.A. Domanov’s paper devoted to the use of modern type theory in the analysis of quantification in opaque contexts (e. g., propositional attitudes and believe reports). The article briefly mentions several recent attempts to use type theory to solve a number of philosophical problems. The paper suggests that the use of modern type theory, which has a number of significant advantages over classical logic and set theory, is a very promising direction in the development of philosophical problems in the spirit of analytic philosophy. In addition, the paper indicates a number of questions on which it would be desired to receive a clarification from the author of the paper being commented.