to the history of the homotopy-theoretical ideas in type theory (Uppsala abstracts)

[Vladimir Voevodsky]

Here are the abstracts of the 2006 Uppsala Conference (http://www2.math.uu.se/~palmgren/itt/). They give a very important snapshot of the earlier years of development of homotopy-theoretical ideas in type theory:

Steve Awodey (Pittsburgh)

Type theory of higher-dimensional categories

Abstract: We investigate some structures in higher-dimensional categories

that are useful for the semantics of intensional type theory.  The

possibility of using such type theories as an internal language for certain

kinds of higher categories is considered.

Benno van den Berg (Darmstadt)

Types as weak omega-categories

Abstract: Fix a type X in a context \Gamma. Define a globular set as

follows: A_0 consists of the terms of type X in context \Gamma, modulo

definitional equality; A_1 consists of terms of the types Id(X,p,q) (in

context \Gamma) for elements p, q in A_0, modulo definitional equality;

A_2 consists of terms of well-formed types Id(Id(X,p,q),r,s) (in context

\Gamma) for elements p, q in A_0, r, s in A_1, modulo definitional

equality; etcetera...

What is the structure of this globular set? That of a weak omega-groupoid,

certainly. But unless I missed something there is no definition of a weak

omega-groupoid for globular sets. However, there is a definition of a weak

omega-category, especially the one explained in detail in Tom Leinster's

book "Higher operads, higher categories". I will show that the globular

set defined above is a weak omega-category in precisely this sense.

Wojciech Chacholski (Stockholm)

Representations of spaces and mapping complexes

ABSTRACT:

derived functors of colimits and limits, mapping complexes, fibrant 

and cofibrant replacements are fundamental objects of homotopy 

theory. The frameworks which have been developed in order to study 

these constructions range  from model categories to theory of 

derivators.   These approaches however are not easy to use. For

example it is often a difficult task to impose a model structure 

that reflects desired properties. Even if one is able to prove its 

existence, such a statement shades little info on how to construct

cofibrant/ fibrant replacements. In the talk I will explain a modified

approach, the key feature of which is its simplicity and applicability.

This is joint work with J. Scherer.

Peter Dybjer (Göteborg)

History and meaning of the identity type.

Content:

Lawvere's equality in hyperdoctrines. Howard's treatment of identity.

Martin-Löf's identity in his theory of iterated inductive definitions. The

different identity types in versions of type theory. The meaning

explanations for the identity type. Identity type vs identity judgement.

My own experience of proving coherence of monoidal categories using type

theory as a metalanguage. My own view of identity in type theory

justifying extensional identity types.

Nicola Gambino (Montreal)

Title: Quillen model structures on diagrams of categories

Abstract: The category small categories admits a natural Quillen model 

structure whose weak equivalences are categorical equivalences. The aim 

of this talk is to show how this model structure determines two distinct 

Quillen model structures on diagrams of categories. I will discuss

how this result links with 2-dimensional category theory, the theory of 

homotopy limits, and Lawvere's notion of hyperdoctrine.

Richard Garner (Uppsala)

Factorisation axioms for type theory 

ABSTRACT: Though the type constructors of intensional type theory hint at

the presence of a weak factorisation system on its category of contexts,

they are not sufficiently strong to construct such. This can be fixed by

decree, by adding axioms for a weak factorisation system to our type theory.

We examine the consequences of doing this.

Martin Hyland (Cambridge)

Algebraic Homotopy Theory: Lessons for Type Theory

Abstract:

Constructions in abstract homotopy theory generally have

two ingredients. One is essentially algebraic and is founded

on ideas of enriched category theory. The other is strictly

homotopy theoretic in flavour and typically uses ideas from

the theory of model categories. I shall explore the impact 

for type theory of an approach based on the algebraic ideas.

M. E. Maietti and G. Sambin

Intensionality vs. extensionality: a solution with two levels of

abstraction.

Some precise results show that extensionality of a theory is

incompatible with its effectiveness, when this is meant to include

consistency with the axiom of choice and internal Church thesis. This

looks as an obstacle to the project of formalization of mathematics in a

computer language, since the latter is by definition effective while the

former is extensional by tradition.

There is a way out (which we first proposed at TYPES '04) which is very

natural, although contrary to established tradition. That is to

introduce two theories: a ground type theory, which is a sort of

idealized programming language and thus is intensional, and an

extensional theory, suitable to develop (constructive) mathematics. The

novelty lies on the link between the two theories: the extensional

theory is to be obtained from the intensional one by abstraction, that

is by "forgetting" some information, and this is to be done in such a

way that implementation is always possible, that is, by forgetting only

those pieces of information which can be restored at will. This

requirement is not as trivial as it may look at first: the second

incompleteness theorem by Gödel says that the normalization process of

a formal system will always be a source to restore information, which is

not available within the system itself.

Per Martin-Löf (Stockholm)

Topos theory and type theory

Abstract: My purpose is to relate type theory to topos theory by taking the

concept of model of type theory to be the counterpart of the notion of

elementary topos. Inductive and projective limits of comma (or slice) models

of type theory will be considered. The former correspond to the filter

quotients of topos theory.

Thomas Streicher (Darmstadt)

Identity Types vs. Weak \omega-Groupoids some ideas, some problems

ABSTRACT After reviewing some basics about Identity Types in intensional

         Martin-Löf type theory and shortly presenting the groupoid model

         I explain why every type forms an internal weak \omega-groupoid.

         It thus seems tempting to use Kan complexes as a model. But there

         are problems with the Beck condition. I sketch an idea how to define

         a sufficiently internal notion of Kan complexes allowing to choose

         "fillers" in a functorial way. This notion might be of interest for

         geometers as well.

         Finally, I discuss to which extent a weak \omega-groupoid model

         says something about the types definable in traditional type theory.

         I am afraid nothing because their interpretations all stay within 

         discrete simplicial sets.

         

         

Michael Warren (Pittsburgh)

Model categories and intensional identity types

Abstract:

Quillen model categories provide a flexible axiomatic framework in which to

develop the homotopy theory of various categories.  In this talk we will

show that model categories also provide a framework in which to develop the

semantics of Martin-Löf's intensional type theory.  In particular, the

internal language of any model category, in which fibrant objects are closed

types and fibrations are dependent types, contains a form of intensional

identity type arising from the path objects present in the model structure.

We explore this connection further by considering several variations on this

theme as well as looking at dependent products and sums in the setting of

Quillen model categories.  If time permits the connection between cocategory

objects and model structures will also be discussed.

         

         

[Joyal, André]

Dear All,

It appears that the connection between type theory
and homotopy theory is unfolding progressively.
The groupoid model of Hoffmann and Streitcher was a precursor,
the Uppsala conference a landmark and
Voevodsky's univalence axiom a huge step forward.
There is also the idea of using a proof assistant like Coq for doing homotopy theory.

The notion of Quillen model category is useful for working in an infty-category
with finite limits and colimits. It has a nice feature: the opposite
of a Quillen model category is also a Quillen model category.
But the category of sets is not self-dual and there is no formal duality in type theory.
The axiomatisation of the category sets by Lawvere was an important step toward
the discovery of the notion of elementary topos.  Voevodsky's univalent foundation
is of similar nature. We are heading toward an elementary axiomatisation
of the notion of higher topos, with a corresponding user-friendly proof assistant.
The contribution of everybody, type theorists, homotopy theorists, category theorists,
computer scientists, etc, is essential to the success of the enterprise.
It is more important than the conquest of Mars.

-André

---

From: HomotopyT...@googlegroups.com [HomotopyT...@googlegroups.com] on behalf of Vladimir Voevodsky [vlad...@ias.edu]
Sent: Thursday, December 04, 2014 10:39 AM
To: homotopytypetheory
Cc: Prof. Vladimir Voevodsky
Subject: [HoTT] to the history of the homotopy-theoretical ideas in type theory (Uppsala abstracts)

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

[Martin Escardo]

Dear André,

Well said, in particular regarding the convergence of many branches of
knowledge in an interesting and unexpected way, as you say at the end
of your message.

But, regarding the subject heading of this thread emphasizing
"homotopy-theoretical ideas in type theory", how about, conversely,
"type theoretical ideas in homotopy theory", such as the very notion
of identity type, which is essential to the formulation of the
univalence axiom and higher inductive types, and their applications in
HoTT/UF to homotopy?

I would think the fundamental ideas flow in both directions!

Best wishes,
Martin

> ------------------------------------------------------------------------
> *From:* HomotopyT...@googlegroups.com

> [HomotopyT...@googlegroups.com] on behalf of Vladimir Voevodsky
> [vlad...@ias.edu]

> *Sent:* Thursday, December 04, 2014 10:39 AM
> *To:* homotopytypetheory
> *Cc:* Prof. Vladimir Voevodsky
> *Subject:* [HoTT] to the history of the homotopy-theoretical ideas in

> <mailto:HomotopyTypeThe...@googlegroups.com>.

> For more options, visit https://groups.google.com/d/optout.
>

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

> <mailto:HomotopyTypeThe...@googlegroups.com>.

> For more options, visit https://groups.google.com/d/optout.

--
Martin Escardo
http://www.cs.bham.ac.uk/~mhe

[Joyal, André]

Dear Martin,

Clearly, type theory is bringing a new formal language to homotopy theory.
The notions of contexts, of variables, the operations of sum and product
are very convenient. Also, the univalence axiom is exactly what you
need to prove homotopical descent.

I just read the article of Vladimir in the Institute letter (Summer 2014).
I would like to comment his statement on the greater foundational importance of
infty-groupoids over infty-categories.
I can agree, since the objects of an infty-topos are infty-groupoids, not infty-categories.
But an infty-topos is itself an (infty,1)-category.
Of course, (infty,1)-categories are structured infty-groupoids (infty-posets).
But this structure is best expressed in the (infty,1)-category of infty-groupoids.
Which is first, the chicken or the egg?
I observe that 1-category theory and 2-category theory are playing an important role
in the foundation of type theory and homotopy theory.

Best wishes,
André
________________________________________
From: Martin Escardo [m.es...@cs.bham.ac.uk]
Sent: Friday, December 05, 2014 5:07 PM
To: Joyal, André; Vladimir Voevodsky; homotopytypetheory
Subject: Re: [HoTT] to the history of the homotopy-theoretical ideas in type theory (Uppsala abstracts)

[Martin Escardo]

On 06/12/14 16:54, Joyal, André wrote:
> I just read the article of Vladimir in the Institute letter (Summer
> 2014). I would like to comment his statement on the greater
> foundational importance of infty-groupoids over infty-categories. I
> can agree, since the objects of an infty-topos are infty-groupoids,
> not infty-categories. But an infty-topos is itself an
> (infty,1)-category. Of course, (infty,1)-categories are structured
> infty-groupoids (infty-posets). But this structure is best
> expressed in the (infty,1)-category of infty-groupoids. Which is
> first, the chicken or the egg? I observe that 1-category theory and
> 2-category theory are playing an important role in the foundation of
> type theory and homotopy theory.

Thanks for this explanation/observation/view. It is very useful.

Best wishes,
Martin