There are a number of ways to see HOL as an instance of a "dependent" type theory, in a way that is reasonable, that is there is a pure type system (https://en.wikipedia.org/wiki/Pure_type_system) $\mathrm{\lambda HOPL}$ which contains an embedding
$$ [\!| \_\mid\!] :\mathrm{HOL}\rightarrow \mathrm{\lambda HOPL}$$
Which is both sound and complete, that is:
$$\Gamma\vdash_{\mathrm{HOL}}P\quad \mbox{iff}\quad [\!|\Gamma|\!]\vdash_{\mathrm{\lambda HOPL}} [\!| P|\!]$$
But this is without any axioms, in particular without $$\mathrm{PROPEXT}: (P \leftrightarrow Q)\ \rightarrow\ P=Q$$ for every $P$ and $Q$.
This is explained in some detail by Tonino and Fujita in On the adequacy of representing higher order intuitionistic logic as a pure type system. I think the proof can also be found in Herman Geuvers' dissertation, but I'm a bit lazy to check at the moment.
With PROPEXT, this stops being true, I believe, however, the rule
$$ (P\leftrightarrow Q)\quad \rightarrow\quad C\ P \rightarrow C\ Q$$
is admissible for any closed predicate transformer $C:\mathrm{Prop}\rightarrow\mathrm{Prop}$, by a pretty straightforward induction on (normal forms of) $C$, so in some weaker sense, PROPEXT is justified in such a system (we can define equality to be $P=Q\ :=\ \forall C, C\ P \rightarrow C\ Q$).
Note that this breaks down if you identify $\mathrm{Prop}$ and $\mathrm{Type}$, as explained by Geuvers in The Calculus of Constructions and Higher Order Logic (i.e. CoC with this axiom is not conservative over HOL). In this sense, PROPEXT is not justified by the Martin-Löf propositions-as-types viewpoint.
I think you can form a similar story with the $J$-axiom. I'm not certain equality reflection needs to come into it, since you don't have that many dependent shenanigans resulting from the embedding.
In response to your other questions:
There is definitely some kind of canonicity result, which gets more subtle as you add classical axioms. Certainly the axiom-free system with only the $\forall$, $\rightarrow$ and equality rules admits cut-elimination.
I'm less sure about the sub-formula properties, but I'm pretty sure they hold in the usual manner, once one has correctly formulated them in the higher order setting. They're a bit less satisfying though, since one may need to take instances of formulae quantifying over propositions themselves. I don't see a lot of use for such theorems in the meta-theory of HOL.