What is the relation of HOL Light type theory and some of the intuitionistic type theories?
HOL is a simple type theory, while Martin-Löf's is a dependent type theory. That is the fundamental difference between the two.

One can embed HOL into extensional type theory, i.e., type theory with identity types and the equality reflection principle
$$\frac{\vdash p : \mathrm{Id}_A(s,t)}{\vdash s \equiv_A t}$$
You could try a less drastic principle, such as Streicher's $K$ axiom or uniqueness of identity proofs, in which case you will be interested in conservativity of intensional type theory with $K$ over extensional type theory. But perhaps you don't want to dig into such details right now.