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

[Matt Oliveri <atmacen@gmail.com>]

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

On Monday, February 11, 2019 at 4:50:19 PM UTC-5, Michael Shulman wrote:
>
> Well, I can't tell exactly what Jon meant by "I have a proof object D 
> of a judgment J, if J is definitionally equal to J', then D is also 
> already a proof of J'.".  If he meant that an entire typing judgment 
> "M:A" is only "definitionally equal" to a typing judgment "N:B" if 
> *the very same derivation tree* of M:A counts also as a derivation of 
> N:B, then in the ordinary presentations of *any* ordinary type theory 
> I don't think any two judgments that differ by anything more than 
> alpha-equivalence would be considered "definitionally equal".
>

Right. So I assumed he didn't mean that. I'm pretty sure that for ITT, the 
terms are the proof objects. But it's not clear what should count as proof 
objects otherwise. This is a weakness of the definition. I guessed at what 
the proof objects were for Nuprl, but it looks like Jon had something else 
in mind.

If the proof objects are taken to be whatever notion of formal proof the 
formalizer needs to produce, then definitional equality is an important 
consideration for proof engineering. That's what I was thinking about. 
Crucially, proof automation changes the notion of proof, in practice. But 
this makes things fuzzy.

AML programs do not denote something in a model, 
> and I can't think of any sense in which two of them could be "equal by 
> definition".


You seem confused. Definitional equality is not a relation on proof 
objects, it's a relation on expressions appearing in the judgments they 
prove. AML programs don't appear in judgments. (Well, not any semantically 
relevant judgments.)

For instance, (\lambda x. x^2)(3) is equal by definition 
> to 3^2, because \lambda x. x^2 denotes by definition the function that 
> takes its argument and squares it.


This sure seems completely different from what Jon was getting at. But 
anyway, what's the difference between "denoting by definition" and regular 
denoting?

An important aspect of Jon's definition of "definitional equality", which I 
think is right, is that it doesn't have to do with models. Definitional 
equality is an intentional issue. An issue tied to implementation. ITT pins 
definitional equality to judgmental equality, which *does* have to do with 
models, and I think that's *bad*. I suspect that the discomfort or lack of 
understanding many mathematicians supposedly have with definitional 
equality stems from the fact that it is, in fact, an implementation issue.

So I would say that Andromeda with its reflection rule does not 
> include a "definitional equality" as a distinguished notion of the 
> core language.


Agree.

However, when using Andromeda as a logical framework 
> to implement some object language, one might assert a particular class 
> of substitutional equalities in the object language that are all 
> definitional.
>

How would you tell when a class of equalities is definitional?

On Mon, Feb 11, 2019 at 11:27 AM Matt Oliveri <atm...@gmail.com 
> <javascript:>> wrote: 
> > 
> > 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. 
>

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