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

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

Hi Mike,

you are right there is a genuine content in the initiality theorem. Indeed, we are using the preterm/judgement presentation to construct initial QIITs (jww Ambrus Kaposi, Andras Kovac and Jakob von Raumer) in general. Jakob is currently implementing a plugin for Lean that allows us to define QIITs even though they are not present in Lean’s core theory.

What I am arguing about is the way the syntax of type theory should be presented. The separation of preterms and typing derivation reflects conventional thinking, in the sense that collection and logical reasoning need to be separated. To me one of the important innovations of type theory is not only that they don’t need to be separated, they shouldn’t. If we think that type theory is a good way to present Mathematics then shouldn’t we use it, when we present the syntax of type theory?

The intrinsic presentation also capture the spirit of type theory in the sense that we are only interested in typed objects, I.e. that we don’t need to think about untyped objects first.

There is no contradiction in saying that the initiality theorem is useful: it helps to relate systems which are inspired by the old thinking to the new ideas (in CS we call this “legacy software”). I think QITs and HITs should be primitive and once they are there is no need to present type theory in the extrinsic way. 

Thorsten




On 28/05/2018, 23:39, "homotopyt...@googlegroups.com on behalf of Michael Shulman" <homotopyt...@googlegroups.com on behalf of shu...@sandiego.edu> 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.



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.