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

[Michael Shulman <shulman@sandiego.edu>]

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