Re: [HoTT] Re: Canonical forms for initiality

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

On Tue, Oct 17, 2017 at 9:00 AM, Matt Oliveri <atm...@gmail.com> wrote:
> Could you explain why you want to use normal forms and hereditary
> substitution--rather than more typical typing rules--if you expect to need
> an infinite tower of coherences anyway? Needing the coherence tower seems
> like it will make the definition dramatically more complicated, so wouldn't
> it be best to base it on the most simple and familiar typing rules?

The advantage of canonical forms and hereditary substitution is that
the object-language judgmental equality automatically coincides with
the metatheoretic equality, and the inductive-inductive syntax should
simultaneously automatically form a set.  If we instead build a
coherence tower of judgmental equalities and higher judgmental
equalities, then we not only need to decide what that coherence
structure should be (whereas I think the coherence structure for
hereditary substitution should be fairly straightforward in
principle), but prove that it is "coherent" in some sense, in order to
enable the interpretation of raw syntax into inductive-inductive
syntax.

The rules of canonical-form type theory are the simple and familiar
ones, they're just annotated with "directionality" or "atomicity"
information.