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

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

Hi Michael,

thank you for your nice summary. You say that

"It seems to me that the main difference between (1) and (2), and
between (3) and (4), is convenience; is that right?"

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. 

And I may add that there are cases where we don't want to stick to
finitary constructors. For example Ambrus and Andras proposed a theory of
codes to describe QIITs which does use infinitary constructors to allow
indexing by external sets. In this case the setoid approach wouldn't work.

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

Defining normal forms (6),(7) is an important tool but it shouldn't be the
basic definition of the type theory.

Historically we have used (5) even with the variation that equality is
defined on untyped terms and using only a small step reduction relation.
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 and works on the whole context
(parallel substitution). This issue isn't visible in your examples because
of the restriction to unary.
2. Equality is typed and not derived form small-step reduction.
3. Equality is defined at the same time as typing. (this is especially
relevant for dependent types).
4. We only define typed entities (no preterms).

Being able to do these things relied on developments in type theory
itself. It was clear that we needed inductive-inductive definitions to be
able to avoid preterms but a lot of boilerplate was eliminated by using
QITs. And as I said this also opens the way to have well behaved type
theories with infinitary constructors.

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