On Saturday, February 9, 2019 at 3:34:22 PM UTC-5, Michael Shulman wrote:
From an implementation point of view, I agree that in the long run we
should have proof assistants that don't hardcode a fixed set of
judgmental equalities. But I don't think that means eliminating all
judgmental equalities; it just means making the logical framework more
flexible, such as Agda's ability to postulate new reductions or
Andromeda's framework with equality reflection. In particular, the
new equalities that we postulate should still be *substitutive* (as
Jon says, allowing to perturb a judgment without altering the proof
object) rather than *transportive* (requiring the proof object to be
altered) -- I think Vladimir was the one who suggested words like
those.
I first heard those terms was on this list:
https://groups.google.com/forum/#!topic/homotopytypetheory/1bUtH8CLGQg
It seems from that discussion that they were associated with Vladimir Voevodsky's proposal for HTS. As a form of extensional type theory without any "built-in" implementation proposal, it seems like HTS has no notion of "proof object" in Jon's sense, which seems to be formal, checkable proofs. It's not that you couldn't come up with one, it just isn't specified. So I don't think HTS has any "definitional equality", in Jon's sense. But it seems like HTS' exact equality was considered substitutive nonetheless. In fact, it seems to me like what Vladimir meant by "substitutional" was that it doesn't cause coercions. Either because it's definitional, or because it's subsumptive (my term, from another message in this thread).
So I think you're misusing those terms.
Judgmental, definitional, substitutive, and computational equalities
are not exactly the same thing. But the fact that there are so many
different but related points of view on similar and overlapping
concepts, and so many different but related uses and applications for
them, suggests to me that there is an important underlying
mathematical concept that should not lightly be discarded.
This is too vague. I wouldn't know whether I'm discarding it or not. You seem to be downplaying the differences between these notions. Why? If you don't care about the difference, why don't you just deal with strict or exact equality, and leave the implementation details to someone else? Coherence issues don't penetrate to a lower level than strict equality. Judgmental, definitional, and substitutive equality are special cases of strict equality that differ in their implementation properties.