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

[Michael Shulman <shulman@sandiego.edu>]

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".  Look
for instance at appendix A.2 of the HoTT book: coercion along
judgmental equality is a rule that alters a derivation tree.  What it
doesn't alter is the *term*, and since Jon also said "In most
formalisms, definitional equality includes some combination of
alpha/beta/eta/xi" I assumed that his "proof objects" in a MLTT-like
theory would refer to the terms rather than the derivation trees.

Regardless of what Jon meant, it seems to me that insofar as
"definitional equality" is distinguished from all these other kinds of
strict equality, it should refer to pairs of terms (i.e. bits of
syntax that denote something in a model) that are *equal by
definition*.  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.  I think this is roughly the same
as what I would mean by "equality of sense", although the latter is a
primarily philosophical concept and as such cannot be pinned down with
mathematical rigor.  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".  A judgmental, strict, exact, or substitutional equality
might include only definitional equalities, as in ordinary ITT, or it
might include other non-definitional ones, as in ETT with reflection
rule.  So I would say that Andromeda with its reflection rule does not
include a "definitional equality" as a distinguished notion of the
core language.  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.

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

-- 
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.