# Tag Info

5

DEDUCT_ANTISYM_RULE only applies to propositions, while REFL applies to all terms of all types. Your suggestion only shows that every propositions is equal (equivalent) to itself, but it could not be used to show that ever number equals itself.

2

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: ...

2

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 ...

Only top voted, non community-wiki answers of a minimum length are eligible