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.