Equivalence of Horn formulas tractable?
Yes, you can check equivalence in polynomial time (in fact, in quadratic time).
By similar logic to my answer to your previous question, it suffices to test satisfiability of $\phi_1 \land \neg c$ where $c$ ranges over the clauses of $\phi_2$.  If any of these are satisfiable, then $\phi_1,\phi_2$ are inequivalent.  Otherwise, if they're all unsatisfiable, and the same for $\phi_2 \land \neg c'$ where $c'$ ranges over all clauses of $\phi_1$, then $\phi_1,\phi_2$ are equivalent.
So, let's investigate how to test satisfiability of $\phi_1 \land \neg c$ where $c$ is a clause of $\phi_2$.  By assumption, $c$ is a Horn clause, so it has the form $\neg x_1 \lor \dots \lor \neg x_k \lor x_{k+1}$.  So, $\phi_1 \land \neg c$ has the form
$$\phi_1 \land x_1 \land \dots \land x_k \land \neg x_{k+1}.$$
This turns out to be a Horn formula, so you can its test satisfiability with the standard algorithm for testing satisfiability of Horn formula.  This takes linear time per clause, and there are linearly many clauses, so the total running time is quadratic.