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