Leibniz is probably unnecessarily non-intuitive. In type theory this concept is usually more often refereed as "propositional equality" or "type equality" (as in "propositions as types").
I took the name from scalaz but thinking of it, the term "Leibniz equality" is maybe best left in the javadoc.
Also this would be more in line with Haskell built-in type equality (also it may be worth having a look at the combinators provided by this package).
@clinuxrulz, @gneuvill, WDYT? (originally, @clinuxrulz, I think you also used TypeEq).
Alternative could be TypeEquals (used in purescript).
Leibniz
is probably unnecessarily non-intuitive. In type theory this concept is usually more often refereed as "propositional equality" or "type equality" (as in "propositions as types").I took the name from scalaz but thinking of it, the term "Leibniz equality" is maybe best left in the javadoc.
Also this would be more in line with Haskell built-in type equality (also it may be worth having a look at the combinators provided by this package).
@clinuxrulz, @gneuvill, WDYT? (originally, @clinuxrulz, I think you also used
TypeEq
).Alternative could be
TypeEquals
(used in purescript).