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

[Jon Sterling <j...@jonmsterling.com>]

Hi all,

The point about the homotopy hypothesis is well-taken, but I cannot help but think that there is something of quite a different nature going on with the initiality conjecture. I hope to be corrected by those who know more than I, but it seems like the gap between the "definitional solution" and the full sequence of mathematical practice which the homotopy hypothesis hopes to account for must be vastly greater than the gap between type theory qua preterms + raw judgments, and type theory qua the generalized algebraic theory (for which the initiality conjecture is essentially something that one observes, rather than proves AFAICT).

Somehow for the last 50 years what we type theorists were doing was not so far away from the 'definitional solution'---there is definitely a gap, but ever since Lawvere's devastating and decisive rectification campaign of algebra in the 1960s, preceding the development of modern type theory, it has not been the case that a more abstract notion of syntax has been alien to type theorists; the development of logical frameworks (in the tradition of De Bruijn and Martin-Loef) reflects this. [Ask me sometime what I think about the claim that using the logical framework is "defining away" the question!]

Because I don't know much about homotopy theory, I can't go into depth there, but as a type theorist, I would like to say that this gap (between preterms and the generalized algebraic theory) is not uniform, but comprises multiple distinct components, not limited to the following:

1. There is the question of implicit vs explicit substitution. Mathematical accounts of type theory usually use explicit substitution, because it is the most natural, and it can be phrased without reference to preterms or set-theoretic hacking. Explicit substitution is superior, because it is more abstract, but on the other hand there is indeed a question of whether we have 'solved the problem' if we have not explained implicit substitutions. I would argue that this is in some sense not a significant problem, because if you are "inside" type theory / using type theory to do mathematics, there is really no way to observe whether you are using implicit or explicit substitutions: the question is analogous to the matter of allowing beta redexes vs forcing a canonical-forms representation as in modern LF. It is in some sense an implementation detail.

2. There is the fact that type theories "in the wild" are generally not algebraic. That is to say, they do not have unique types (consider universe cumulativity), and even in cases where it would be possible to achieve uniqueness of typing, it is actually highly undesirable from a practical perspective---the unique typing calculi contain so many unnecessary annotations, and to check types in such a setting is highly inefficient. It can of course be argued that implementation is a different matter from the mathematics, but I want to argue that to a certain extent, we should expect practice to be the leading aspect, and that theory should somehow reflect it.

If "wild" type theories are not algebraic, what do we mean by "model" and "initiality"? Surely we can come up with answers to these questions, but I think somehow it is not the right question.

There is a desire for the mathematics to explain in one fell swoop exactly the full gamut of type theories that we use in daily life, but I think that this apparently 'down to earth' point of view actually forces us to give short shrift on one of the most interesting and under-studied parts of type theory, which is the matter of elaboration and of coherence.

To phrase initiality in terms of an already-suitably-algebraic notion of type theory is not, in my opinion, to "define away" the problem; instead, it is to resist drawing the problem outside its range of significance.

Far from being a result which might hold or fail about "type theories" (what are those, specifically?), 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).

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, and of course we can make it appear as though it has more and more scientific content by choosing to use a less and less structured representation of syntax. For instance, we can say "Aha, we are hardly solving the problem if we use de bruijn indices instead of fixing an infinite set of names, like our grandparents taught us to!" And then, we can increase the appearance of difficulty by threading through the entire construction the bureaucratic issues of name binding which were resolved decades ago. We can also increase the appearance of difficulty, as Thorsten satirically argues, by threading through the construction the *parsing* of sequences of tokens into structured syntax; we could take a step further and thread through the construction the *lexing* of sequences of characters into tokens... But to me this is all beside the point.

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. 

[Cubical type theory brings up numerous other analogous questions; for instance, in cubical type theory one constructs a partial element of a type by going under a "restriction", but another possible representation which is more structured and somehow more type-theoretically natural (but less strict) is to actually pattern match on the "proof" of a cofibration formula (this is in fact exactly what one does in the agda formalizations of the Orton-Pitts-Licata style internal presentation of cubical type theory). There is an interesting connection here with the difficulty question of definitional equivalence which supports the full universal property of coproducts, and there may be a coherence theorem to prove.]

Best,
Jon

P.S. Over the past few years my opinions on the questions have changed a lot, and I expect that they will continue to change, hopefully as a result of this very interesting discussion. Thanks!






On Mon, May 28, 2018, at 3:39 PM, Michael Shulman wrote:
> I knew this situation seemed familiar: it reminds me of Tom Leinster's
> comments about the homotopy hypothesis:
> https://golem.ph.utexas.edu/category/2010/03/a_perspective_on_higher_catego.html
> (scroll down to "What is an n-category?")
> 
> The "Homotopy Hypothesis" of higher category theory, first formulated
> by Grothendieck, is the claim that "infinity-groupoids are the same as
> spaces".  The prevailing approach to this in higher category theory
> nowadays is the one that Tom describes as a "joke":
> 
> Q.  How do you prove the Homotopy Hypothesis?
> A.  Define an infinity-groupoid to be a Kan complex; define a space to
> be a Kan complex; done!
> 
> Describing this as a joke is not to denigrate the value of such a
> "definitional solution"; it's certainly been enormously fruitful for
> higher category theory.  But at the same time, Tom's point is that it
> doesn't, on its own, answer the question that was originally asked.
> He has a nice picture of a spectrum from "algebra" to "topology",
> starting with algebraic notions of infinity-groupoid, then moving
> through non-algebraic notions of infinity-groupoid, to algebraic
> notions of space, and eventually non-algebraic notions of space, with
> Kan complexes occupying the fulcum at the middle.  A full-strength
> statement of the homotopy hypothesis would then equate fully algebraic
> notions of infinity-groupoid with fully non-algebraic notions of
> space.
> 
> I feel like here we have something similar.  If we call the
> "Initiality Hypothesis" something like "type theory is the initial
> elementary infinity-topos", then we can make a similar "joke":
> 
> Q: How do you prove the Initiality Hypothesis?
> A: Define an elementary infinity-topos to be a (suitably structured)
> CwF; define type theory to be the initial such CwF; done!
> 
> Again, this is not to denigrate the value of such an approach!  It
> just doesn't, on its own, answer the original question.  I can imagine
> a similar spectrum from "syntax" to "semantics", starting with
> "syntactic notions of type theory", then moving through "semantic
> notions of type theory", to "syntactic notions of toposes", and
> eventually "semantic notions of toposes".  Untyped syntax with
> implicit substitution (5) is way over on the syntactic side; locally
> cartesian closed quasicategories with appropriate stuff are way over
> on the semantic side; CwFs and the initial one as a QIIT are at the
> fulcrum in the middle.  And just as Kan complexes can play an
> important intermediate role in connecting the disparate ends of the
> homotopy-hypothesis spectrum, it seems likely that QIIT syntax can
> play a similar intermediate role in connecting the ends of the
> initiality-hypothesis spectrum.
> 
> Does this seem reasonable?
> 
> 
> On Mon, May 21, 2018 at 10:46 PM, Michael Shulman <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.