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

[Michael Shulman <shulman@sandiego.edu>]

From a semantic point of view, I agree that judgmental equality is
about convenience and usability.  But that shouldn't be regarded as
making it any less important.  Indeed, the whole *point* of using type
theory as an internal language for a category, rather than simply
reasoning about the category directly, is... convenience and
usability.  Of course there are degrees of convenience, and even type
theory without judgmental equality might be slightly more convenient
than reasoning directly in categorical language.  But I think we need
judgmental equality if we really want to get some substantial benefit
out of type theory as an internal language.  The problem of course is
to bridge the gap between the type theory and the category theory, and
for that purpose intermediate structures may be useful: categories
that are more like type theory (such as tribes and contextual
categories) and type theories that are more like category theory (such
as ones with fewer judgmental equalities).  But I don't think I would
want to regard the intermediate structures as fundamental, rather than
tools to get from one side to another.

From an implementation point of view, I agree that in the long run we
should have proof assistants that don't hardcode a fixed set of
judgmental equalities.  But I don't think that means eliminating all
judgmental equalities; it just means making the logical framework more
flexible, such as Agda's ability to postulate new reductions or
Andromeda's framework with equality reflection.  In particular, the
new equalities that we postulate should still be *substitutive* (as
Jon says, allowing to perturb a judgment without altering the proof
object) rather than *transportive* (requiring the proof object to be
altered) -- I think Vladimir was the one who suggested words like
those.

From a computation point of view, of course some kind of reduction is
necessary, and it makes sense to consider an object to be "equal" in
some sense to the result of computing it.  This would presumably be a
stronger sense than typal equality inside the system, whether or not
it is actually substitutive.  Conversely, in order to implement a
substitutive equality it seems very useful to have some algorithm that
can at least go some part of the way towards deciding it, and
computation is likely to play an important role in such an algorithm.

From a philosophical point of view, I think definitional/substitutive
equality is very important: as Steve Awodey pointed out some time ago,
it represents the intensional "equality of sense" rather than the
extensional "equality of reference".  This explains why it is
substitutive: if two terms have the same sense, there is no
explanation necessary for why a statement about one also applies to
the other, while if they only have the same reference, then some
explanation may be required.  If I say "I saw the morning star this
morning" and you reply "yes, and I saw it last night", it sounds weird
because there is a transport necessary along the equality of reference
"morning star = evening star", in a way that doesn't happen if instead
you reply "yes, and I saw it yesterday morning".  Foundations for
mathematics based on first-order logic, like ZFC, have no ability to
talk about equality of sense; the only equality they know about is
reference.  A type theory without definitional equality would have the
same limitation.

Judgmental, definitional, substitutive, and computational equalities
are not exactly the same thing.  But the fact that there are so many
different but related points of view on similar and overlapping
concepts, and so many different but related uses and applications for
them, suggests to me that there is an important underlying
mathematical concept that should not lightly be discarded.  On the
other hand, the proof of the pudding is in the eating, and this whole
discussion would be much more concrete if we had some actual
references working out what type theory without judgmental equality
looks like, with proofs of whatever properties it may be claimed to
have, and perhaps even an implementation of it; so I don't mean to
discourage anyone from trying to develop such a thing.

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