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

[Matt Oliveri <atmacen@gmail.com>]

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

Jon's definitional equality is based on proof objects. The Andromeda terms 
aren't proof objects, since you can't check just a term. So the fact that 
Andromeda terms don't have coercions for strict equality doesn't do 
anything for definitional equality. I would guess AML programs should be 
considered the relevant proof objects. I'd say definitional equality in 
Andromeda is pretty interesting, since algebraic effect handlers let you 
locally add new automation for equality. But it can't be as rich as strict 
equality (if you have e.g. induction on nats). And globally, it sounds like 
it's just alpha conversion.

On Monday, February 11, 2019 at 12:20:46 PM UTC-5, Michael Shulman wrote:
>
> FWIW, I think the only thing I have against NuPRL "in principle" is 
> that it seems to be closely tied to one particular model, which is the 
> opposite of what I want my type theories to achieve.  I say "seems" 
> because then someone says something like Jon's "Nuprl's underlying 
> objects are untyped -- but that is not an essential part of the idea", 
> providing an instance of the problem I have with NuPRL "in practice", 
> which is that every time I think I understand it someone proves me 
> wrong.  (-:O 
>
> Can you explain the difference between "definitional" (whatever that 
> means) and "strict" equality in Andromeda?  Of course there is the 
> technical difference between judgmental equality and the equality 
> type, but that doesn't seem to me to be a "real" difference in the 
> presence of equality reflection, particularly at the purely 
> philosophical level at which a phrase like "equality of sense" has to 
> be interpreted.  As far as I know, even beta-reduction has no 
> privileged status in the Andromeda core -- although I suppose 
> alpha-conversion probably does. 
>
>
> On Mon, Feb 11, 2019 at 7:09 AM Matt Oliveri <atm...@gmail.com 
> <javascript:>> wrote: 
> > 
> > It looks like Jon is with you regarding definitional/substitutive 
> equality, since he considers Nuprl's subtitutive equality to be alpha 
> conversion. From the old discussion about it, I had figured Nuprl's 
> substitutive equality was the equality type. I guess I'll avoid that term. 
> > 
> > So I'll ask a more concrete question. You seem to be more open to 
> Andromeda than Nuprl. It has a difference between definitional equality (in 
> Jon's sense) and the (strict/exact) equality type for approximately the 
> same reason as Nuprl. If the theory you're using is HTS, then there's also 
> path types. So I gather path types are what you want to take as equality of 
> reference. Which is equality of sense? 
> > 
> > Regarding the paragraph I said was vague, my complaint really is that I 
> don't know what you're getting at. I recommended strict or exact equality 
> as possible (informal) interpretations. This doesn't mean there needs to be 
> something called "strict equality" in the system definition, for example, 
> it means you recognize a strict equality notion when you see one. I don't 
> know how to recognize the kind of equality you were getting at in that 
> paragraph. 
>

-- 
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: 4135 bytes --]