Re: [HoTT] Re: Why do we need judgmental equality?

[Matt Oliveri <atmacen@gmail.com>]

[-- Attachment #1.1: Type: text/plain, Size: 2904 bytes --]

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.

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[-- Attachment #1.2: Type: text/html, Size: 3541 bytes --]