What is the relation of HOL Light type theory and some of the intuitionistic type theories? I'm trying to understand how HOL Light deductive rules relate to mainstream intuitionistic type theories.
Here is a sample of questions that come to my mind. 

Does HOL Light derivations admit cut-elimination and what sub-formula property would mean? Is there some kind of canonicity result?

Can HOL equality be modeled with Identity types (with J axiom)?

Somewhat specific question: DEDUCT_ANTISYM_RULE axiom allows us to deduce that if you have  (entilement) both $q \vdash p$ and $p \vdash q$, we can deduce $\vdash p=q$. How can we assert that rule without a condition that the entailments are "each other inverses forming an isomorphism"?

I realize that many of these question might be wrong questions to ask. Perhaps I even am wrong to focus on the deduction rules? 
How should I be thinking when comparing theories such as HOL Light and some 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.