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

[Thorsten Altenkirch <Thorsten....@nottingham.ac.uk>]

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

I didn't view it as criticism - I was just commenting on your email.

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

Ah good. :-)

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

Indeed but also type checking and scoping are solved problems.

We may as well say that parsing, that is relating strings and trees is a
fundamental issue in algebra. It isn't. By the way that isn't so far
fetched as it sounds, in (older?) text books on regular expressions you
find the rule that if E is a regular expression then so is (E). Actually,
you may find the same on lambda calculus.

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

As with the strings...

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

Neither can parsing.

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

But doesn't the same apply to beta-redeces? We don't write programs
containing beta-redeces, they only show up when we expand definitions. The
same with substitutions: we don't write them but they show up for example
when we reduced beta redeces.

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

We only write substitution normal forms as we only write beta normal terms.

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




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.