Re: [HoTT] Re: Where is the problem with initiality?

[Michael Shulman <shu...@sandiego.edu>]

Thanks, Jon, for that very detailed and thoughtful response.

I agree that there are significant differences between the Homotopy
Hypothesis spectrum and the Initiality Hypothesis spectrum -- how
could there not be?  But I don't think those differences invalidate
the analogy.  The gap in the homotopy hypothesis is not uniform
either: for instance, in addition to algebraic vs nonalgebraic, it
comprises cell shape (globular vs simplicial), and there are other
dimensions too such as whether a definition can be phrased in an
ambient homotopy theory or whether it has to be built out of sets.  In
other words, the "spectrum" is actually multidimensional in both
cases.  And non-algebraic notions of higher category were not alien to
category theorists either; indeed, the very first proposed general
definition of omega-category (due to Ross Street) was non-algebraic!

I'm grateful to you, Thorsten, and others, for trying to help me get
over my hangups about explicit substitution.  I guess that
fundamentally what matters is the existence of normal forms and of a
terminating normalization algorithm, and that applies to
beta-reduction as well as to substitution-reduction.  I personally
find it more elegant to regard the normal forms as the "fundamental"
objects with things like application and substitution as defined
operations on them, rather than regarding application and substitution
as term constructors and then having to quotient by beta-reduction and
substitution reduction -- why introduce flab only to quotient it out
later?  And I have an easier time with explicit applications than with
explicit substitutions, because I see the former but not the latter
all the time in everyday mathematics.  But I can see that the other
approach has advantages as well.

On Tue, May 29, 2018 at 7:00 AM, Jon Sterling <j...@jonmsterling.com> wrote:
> Far from being a result which might hold or fail about "type theories" (what are those, specifically?),

I take it that your parenthetical refers to the lack of a general
definition of "type theory".  But to me, such a lack is itself a gap
in the literature -- how can we really consider "type theory" a
respectable mathematical subject if we don't even have definitions of
the things it studies?  The lack of such a definition is not a reason
not to study type theories in general, rather the opposite -- studying
type theories in general will help move us towards being able to
formulate such definitions (note the plural -- I don't necessarily
expect there to ever be *one* definition encompassing *all* type
theories).

> I think that initiality is a purely definitive principle by which we can measure any attempt at formulating an algebraic notion of type theory (and there is no reason a priori to expect this to explain type theory as it exists in the wild, because the latter kind of type theory was never intended to be algebraic).

I don't think the fact that "wild type theories" (interesting
associativity there with the biological notion of "wild type") were
"never intended to be algebraic" is a reason not to study their
algebraicity.  In fact it's *more* exciting when something that wasn't
*intended* to be algebraic turns out nevertheless to be (equivalent
to) something algebraic!  Such unintended coincidences are what
mathematics thrives on; indeed HoTT itself arose from a gigantic
unintended coincidence between intensional type theory and homotopy
theory.

> The gap between algebraic type theory and the pre-term-presented version of type theory which still has unique types etc. is a purely bureaucratic gap

I don't think that's a fair characterization, because it seems
(likely) to depend on fundamental features of a particular type
theory.  In his talk Thorsten mentioned that the proof of decidability
of equality for QIIT syntax uses a normalization, and the alternative
argument I proposed using hereditary substitution also depends on the
existence of the latter, which is essentially a normalization
property.  I wouldn't call something "bureaucratic" if it depends on
essential features of a particular situation and doesn't generalize to
slightly modified situations.

> I believe that the interesting gap that we should study (using tools from the study of elaboration, coercions, coherence, etc.) is the one between "wild" type theory (where you you have subtyping, implicit coercion, etc.) and algebraic type theory.

I agree that elaboration is an important problem that we should study,
but I don't think it is "the" problem we should study -- other
problems can also be interesting and important!

Thanks again for the interesting discussion!

Best,
Mike