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

[Michael Shulman <shulman@sandiego.edu>]

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 <atmacen@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.
>
> On Monday, February 11, 2019 at 8:04:35 AM UTC-5, Michael Shulman wrote:
>>
>> On Mon, Feb 11, 2019 at 4:17 AM Matt Oliveri <atm...@gmail.com> wrote:
>> > 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.
>>
>> Well, after many years I still have not managed to figure out how
>> NuPRLites use words, so it's possible that I misinterpreted what Jon
>> meant by "proof object".  But if you interpret what I meant in ITT,
>> where I know what I am talking about, then it makes sense.  In ITT the
>> relevant sort of "witness of a proof" is just a term, so "not
>> perturbing the proof object" means the same thing as "not causing
>> coercions".
>>
>> > You seem to be downplaying the differences between these notions. Why?
>>
>> Maybe things are different in computer science, but in mathematics it
>> often happens that there are things called "ideas" that are, in fact,
>> vaguer than anything that can be written down precisely, and can be
>> realized precisely by a variety of different formal definitions with
>> different formal properties.  The differences -- even conceptual
>> differences -- between these definitions are not unimportant or
>> ignorable, but do not detract from the importance of the idea or our
>> ability to think about it.  Indeed, the presence of multiple formal
>> approaches to the idea with different connections to different
>> subjects make it *more* important and provide us *more* options to
>> work with it formally.  I am thinking of for instance all the
>> different constructions of a highly structured category of spectra, or
>> all the different definitions of (oo,1)-category.
>
> --
> 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.