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

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

Thanks for your response Thorsten!  I did not intend my original email
as a criticism or alternative proposal to your work, only an
informational question as to where the difficulty is in getting from
the "tautological" initiality theorem in your work to the "hard"
initiality theorem that various other people are working on proving
(whatever one's opinion may be about which of them is more important).

That said, I suppose I may as well pick up that gauntlet you left on
the floor...  (-:O

On Wed, May 23, 2018 at 9:26 AM, Thorsten Altenkirch
<Thorsten....@nottingham.ac.uk> wrote:
> It seems to me that a lot in Mathematics can be described as convenience.
> Sometimes a good (but equivalent) choice of representation can make all
> the difference.

I agree entirely; I didn't mean the word "convenience" to be at all perjorative.

> (5) and (7) introduce preterms which I think shouldn't be considered
> fundamental in the definition of type theory.

I have to disagree here.  In my view, we have to eventually connect
things back to untyped syntax, because untyped syntax is what we write
on the page, and what we enter into a proof assistant.  (We don't need
to go all the way back to character strings -- parsing and lexing are
essentially solved problems in any language -- but we do need to get
back to some kind of untyped *abstract* syntax such as in (5).)  The
various kinds of typed syntax are useful and important intermediate
objects, but at some point there has to be a step that formally
explains how to produce "typed syntax" from untyped syntax.

I suppose you could play word games and call the typed syntax the
"definition of type theory" and the untyped syntax a "technical tool
for presenting terms in type theory" or something like that, but the
point is that the untyped syntax has to be there at some point, or
else our metatheory is incomplete.  And the fact that the initiality
theorem for your typed syntax is trivial while the initiality theorem
for untyped syntax is hard means that this gap has real mathematical
content and can't be dismissed as obvious or not worth worrying about.

> Substitution is a defined metatheoretic operation. Once you take these
> choices you spend a lot of time proving things which should be obvious.
> Now, obviously there is not one "best" way to define type theory but I
> think we have made a lot of progress. The basic ingredients of this
> progress are:
>
> 1. Substitution is a term constructor

I have to disagree here too.  Substitution should *not* be a term
constructor (at least, not in the fundamental definition of type
theory), because *in practice* the terms we write do not contain
explicit substitutions.  When I tell my calculus students to
substitute g(x) for y in f'(y) in the chain rule, I expect them to
write f'(g(x)), not f'(y)[g(x)/y].  Using explicit substitutions in
the syntax makes the semantics easier, but at the expense of "changing
the question" away from the one we wanted to ask in the first place.
In the end we want to interpret the *actual* syntax we write down on
the page.

Of course, in an intermediate step like QIIT typed syntax, we are free
to choose to make substitution explicit; but eventually we need to
make the connection back to a syntax in which substitution is
implicit.

> Just to comment on the h-level problem you don't want to discuss yet: it
> seems to me that if we want to use something along the line of (6) to
> define normal forms for dependent types we face the problem that we need
> to define normalisation at the same time as the terms. This is
> induction-recursion which on it's own shouldn't be a problem.

I actually think it's better to define the graph of hereditary
substitution inductive-inductively along with the terms, but that may
be largely aesthetic; in general I prefer induction-induction over
induction-recursion.

> However, it
> seems to me that we have to prove properties of normalisation (e.g.
> substitution laws) at the same time which again give rise to coherence
> problems.

I agree, both approaches will have to deal with coherence, since they
are essentially proving the same theorem in two different ways.  The
advantage I envision for (6) is that the coherence is all encapsulated
in the *operation* of hereditary substitution and corresponding
"higher operations": the actual *equality* on normal forms coincides
with the metatheoretic equality *without* the need to impose
equality-constructors.  It seems to me that this may be useful when we
come to interpret the untyped syntax into the typed syntax, because it
means there is no "coercion rule" in the typed syntax to worry about
having to apply.

I agree that non-normal forms are important, for the same reason that
untyped syntax is important, namely that we actually write them on the
page.  But since the typed syntax is just an intermediate step between
what we write on the page and its semantic interpretation, I don't see
a problem with performing the normalization in the same step that
interprets untyped syntax into typed syntax.

> It would be interesting to see a way to avoid these issues, but
> then wouldn't we be able to solve the problem to define semi-simlicial
> sets (or more general reedy limits) in plain HoTT?
>
>
> Thorsten
>
> On 22/05/2018, 06:46, "homotopyt...@googlegroups.com on behalf of
> Michael Shulman" <homotopyt...@googlegroups.com on behalf of
> shu...@sandiego.edu> wrote:
>
>>Thorsten gave a very nice HoTTEST talk a couple weeks ago about his
>>work with his collaborators on intrinsic syntax as a Quotient
>>Inductive-Inductive Type.  Since then I have been trying to fit
>>together a mental picture of exactly how all the different approaches
>>to syntax are related, but I am still kind of confused.
>>
>>In an attempt to clarify what I mean by "all the different
>>approaches", let me describe all the approaches I can think of in the
>>case of a very simple type theory: non-dependent unary type theory
>>with product types.  Unary means that the judgments have exactly one
>>type in the context, x:A |- t:B, and the only type constructor is a
>>product type A x B, with pairing for an introduction rule and
>>projections for elimination.  The semantics should be a category with
>>finite products.  Here are all the ways I can think of to describe
>>such a type theory:
>>
>>
>>1. A QIIT that mirrors the semantics, with all the categorical
>>operations as point-constructors and their axioms as
>>equality-constructors.
>>
>>data Ty : Set where
>> _x_ : Ty -> Ty -> Ty
>>[This will be the same in all cases, so I henceforth omit it.]
>>
>>data Tm : Ty -> Ty -> Set where
>>  id : {A} -> Tm A A
>>  _o_ : Tm A B -> Tm B C -> Tm A C
>>  assoc : h o (g o f) = (h o g) o f
>>  lid : id o f = f
>>  rid : f o id = f
>>  (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
>>  pr1 : Tm (A x B) A
>>  pr2 : Tm (A x B) B
>>  beta1 : pr1 o (f , g) = f
>>  beta2 : pr2 o (f , g) = g
>>  eta : p = (pr1 o p , pr2 o p)
>>
>>
>>2. An Inductive-Inductive family of setoids that similarly mirrors the
>>categorical semantics, with judgmental equality an inductive type
>>family rather than coinciding with the metatheoretic equality.
>>
>>data Tm : Ty -> Ty -> Set where
>>  id : {A} -> Tm A A
>>  _o_ : Tm A B -> Tm B C -> Tm A C
>>  (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
>>  pr1 : Tm (A x B) A
>>  pr2 : Tm (A x B) B
>>
>>data Eq : Tm A B -> Tm A B -> Set where
>>  assoc : Eq (h o (g o f)) ((h o g) o f)
>>  lid : Eq (id o f) f
>>  rid : Eq 9f o id) f
>>  beta1 : Eq (pr1 o (f , g)) f
>>  beta2 : Eq (pr2 o (f , g)) g
>>  eta : Eq p (pr1 o p , pr2 o p)
>>
>>
>>3. A QIIT that instead mirrors the usual type-theoretic syntax, with
>>operations like composition being admissible rather than primitive.
>>In our simple case it looks like this:
>>
>>data Tm : Ty -> Ty -> Set where
>>  id : {A} -> Tm A A
>>  (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
>>  pr1 : Tm A (B x C) -> Tm A B
>>  pr2 : Tm A (B x C) -> Tm A C
>>  beta1 : pr1 (f , g) = f
>>  beta2 : pr2 (f , g) = g
>>  eta : p = (pr1 p , pr2 p)
>>
>>
>>4. Combining 2 and 3, an II family of setoids that mirrors
>>type-theoretic syntax.
>>
>>data Tm : Ty -> Ty -> Set where
>>  id : {A} -> Tm A A
>>  (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
>>  pr1 : Tm A (B x C) -> Tm A B
>>  pr2 : Tm A (B x C) -> Tm A C
>>
>>data Eq : Tm A B -> Tm A B -> Set where
>>  beta1 : Eq (pr1 (f , g)) f
>>  beta2 : Eq (pr2 (f , g)) g
>>  eta : Eq p (pr1 p , pr2 p)
>>
>>
>>5. A single inductive type of raw terms, together with inductive
>>predicates over it for the typing judgment and equality judgments.
>>
>>data Tm : Set where
>>  var : Tm
>>  (_,_) : Tm -> Tm -> Tm
>>  pr1 : Tm -> Tm
>>  pr2 : Tm -> Tm
>>
>>data Of : Ty -> Tm -> Ty -> Set where
>>  of-var : Of A var A
>>  of-pair : Of A t B -> Of A s C -> Of A (t , s) (B x C)
>>  of-pr1 : Of A t (B x C) -> Of A (pr1 t) B
>>  of-pr2 : Of A t (B x C) -> Of A (pr2 t) C
>>
>>data Eq : Ty -> Tm -> Tm -> Ty -> Set where
>>  beta1 : Of A t B -> Of A s C -> Eq A (pr1 (t , s)) t B
>>  beta2 : Of A t B -> Of A s C -> Eq A (pr2 (t , s)) t C
>>  eta : Of A t (B x C) -> Eq A (pr1 t , pr2 t) t (B x C)
>>
>>
>>6. An II family that defines only the normal forms, via a separate
>>judgment for "atomic" terms that prevents us from writing down any
>>beta-redexes, thereby eliminating the need for any equality judgment
>>(though substitution then becomes more complicated, as it must
>>essentially incorporate beta-reduction).
>>
>>data Atom : Ty -> Ty -> Set where
>>  id : {A} -> Atom A A
>>  pr1 : Atom A (B x C) -> Atom A B
>>  pr2 : Atom A (B x C) -> Atom A C
>>
>>data Tm : Ty -> Ty -> Set where
>>  atom : Atom A B -> Tm A B
>>  (_,_) : Tm A B -> Tm A C -> Tm A (B x C)
>>
>>
>>7. Combining 5 and 6, an inductive type of raw terms and predicates
>>over it that type only the normal forms.
>>
>>data Tm : Set where
>>  var : Tm
>>  (_,_) : Tm -> Tm -> Tm
>>  pr1 : Tm -> Tm
>>  pr2 : Tm -> Tm
>>
>>data Atom : Ty -> Tm -> Ty -> Set where
>>  atom-var : Atom A var A
>>  atom-pr1 : Atom A t (B x C) -> Atom A (pr1 t) B
>>  atom-pr2 : Atom A t (B x C) -> Atom A (pr2 t) C
>>
>>data Of : Ty -> Tm -> Ty -> Set where
>>  of-atom : Atom A t B -> Of A t B
>>  of-pair : Of A t B -> Of A s C -> Of A (t , s) (B x C)
>>
>>
>>This is all I can think of right now.  Are there others?  Are there
>>other choices we can make in the case of dependent type theory that
>>are not visible in this simple case?
>>
>>In the above simple case of unary type theory with products, it should
>>be easy to show that all these definitions construct the initial
>>category with products.  (There should be some generating/axiomatic
>>types and terms too, to make the result nontrivial, but I've left them
>>out for brevity.)  My main question is, where do things become hard in
>>the case of dependent type theory?
>>
>>It seems to me that the main difference between (1) and (2), and
>>between (3) and (4), is convenience; is that right?  Type theory has
>>no infinitary constructors, so there shouldn't be axiom-of-choice
>>issues with descending algebraic operations to a quotient; it's just
>>that the bookkeeping involved in dealing with setoids everywhere
>>becomes unmanageable in the case of DTT.  Right?
>>
>>Thorsten said that (1) in the case of dependent type theory is
>>tautologically the initial CwF, which seems eminently plausible.  I
>>don't think this solves the "initiality conjecture", but where is the
>>sticking point?  Is it between (1) and (3), or between (3) and (5)?
>>
>>(Note that I'm not talking at all about the "h-level problem" that
>>these QIITs are by definition sets but that for HoTT to "eat itself"
>>we would want to eliminate out of them into the universe which is not
>>a set.  I'm only talking about initiality of syntax among *strict*
>>CwFs; coherence/strictification theorems can wait.  Personally,
>>though, I like (6)-(7) as potential approaches to coherence.)
>>
>>--
>>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 HomotopyTypeThe...@googlegroups.com.
>>For more options, visit https://groups.google.com/d/optout.
>
>
>
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment.
>
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.
>
>
>
>
> --
> 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 HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.