Since it interprets propositions by sets of possible worlds, the intensional logic of Montague (locus classicus 1973) does not distinguish propositions which are true in the same possible worlds. Because of this, the system does not satisfactorily interpret propositional attitude verbs, a fact which has motivated the development of ‘hyperintensional’ logics (see Fox and Lappin 2008 for a survey). I isolate a hyperintensional system, Comonadic Homotopy Type Theory (CHoTT), which naturally incorporates the intensional logic of Montague with the usual notions of homotopy type theory (see UFP 2013). This system is a fragment of Shulman (2017). From homotopy type theory, we inherit two notions of equality, ≡ and =, which we think of as expressing intensional and extensional equalities, respectively. From Montague, we inherit a syntax for intensional operators, which for us will mean operators which respect intensional but not (necessarily) extensional equality. These are used to interpret propositional attitude operators. When interpreting natural language, the intensional equality is chosen to be sufficiently ‘granular’ that the usual issues are avoided.