Re: Where is the problem with initiality?

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

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