In case of questions please contact Marek Zawadowski (zawado 'at' mimuw.edu.pl).

9th meeting

The meeting will take place on
Eric Finster
(EPFL, Lausanne), *Opetopic Type Theory.*

10:30--12:00 | Eric Finster | Dependent Type Theory |

12:20--13:50 | Eric Finster | Towards an Opetopic Type Theory |

*Dependent Type Theory*

Eric Finster (EPFL, Lausanne)

**Abstract:**
In the past few years some very interesting connections have been discovered between a class of formal
systems know as dependent type theories, well studied in computer science and logic for many years, and
concepts from homotopy theory and higher category theory. In short, these languages exhibit a kind of
internal “decoherence” which forces the objects they describe to act more like homotopy types than sets.
This observation has become the motivating priciple for Voevodsky’s Univalent Foundations Project, which
seeks a new foundational system in which homotopy plays a central role. In my ﬁrst talk, I will give a brief
overview of some concepts from type theory, focusing on how one can use them to encode homotopy theoretic
statements.

*Towards an Opetopic Type Theory*

Eric Finster (EPFL, Lausanne)

**Abstract:**
Given the success of dependent type theories in describing homotopy types, one is naturally led to look for
connections with other concepts from higher category theory. One intriguing possibility is the Opetopes:
a collection of shapes recursively deﬁned in each dimension by considering all possible “many-in-one-out”
pasting diagrams in the previous deﬁnition. Michael Makkai, in setting out his deﬁnition of weak higher
category using these shapes and his concept of a FOLDS signature, explicitly mentions the inﬂuence of type
theory in his thinking. In my second talk, I will give a type-theoretic prespective on the deﬁnition of the
Opetopes, relating them to the computer scientist’s “inductive family”, and describe some work in progress
for developing a type theory which incorporates them into its structure.

8th meeting

The meeting took place on
Urs Schreiber
(Department of Mathematics, University of Nijmegen),
*Differential cohomology and action functionals in a cohesive
infinity-topos. *

10:30--12:00 | Urs Schreiber | Differential cohomology and action functionals in a cohesive
infinity-topos |

12:20--13:50 | Urs Schreiber | Differential cohomology and action functionals in a cohesive
infinity-topos (part 2) |

*Differential cohomology and action functionals in a cohesive
infinity-topos*

Urs Schreiber (University of Nijmegen)

**Abstract:**
I explain how in higher topos theory there is a natural
formulation of differential cohomology, which is the theory of higher
gauge fields / higher connections. Then I indicate the natural
construction of higher Chern-Simons action functionals on moduli
stacks of such higher gauge fields.
I'll assume a knowledge of some basic category theory and some basic
differential geometry, but otherwise will be self-contained. It will
be helpful, though, to have heard of Lie groupoids/differentiable
stacks. Pointers to the literature and further background material is here.

7th meeting

The meeting took place on
Mihaly Makkai
(Department of Mathematics, McGill University),
*Canonical versus non-canonical constructions in category theory. A
selective survey of concepts in higher category theory, with
examples and problems. *

10:30--12:00 | Mihaly Makkai | Canonical versus non-canonical constructions in category theory |

12:20--13:50 | Mihaly Makkai | Canonical versus non-canonical constructions in category theory (part 2) |

*Canonical versus non-canonical constructions in category theory. A
selective survey of concepts in higher category theory, with
examples and problems*

Mihaly Makkai (McGill University)

**Abstract:**
The title is descriptive enough, I think, so that you will not need an abstract, I hope.

6th meeting

The meeting took place on
Bartek Klin
(Department of Computer Science, University of Warsaw),
*Coalgebras and bialgebras.*

10:30--12:00 | Bartek Klin | Coalgebras and bialgebras |

12:20--13:50 | Bartek Klin | Coalgebras and bialgebras (part 2) |

5th meeting

The meeting took place on
Bartek Klin
(Department of Computer Science, University of Warsaw),
*Coalgebras and coinduction*

Jerzy Król
(University of Silesia),
*Breaking a general tovariance...*

10:30--12:00 | Bartek Klin | Coalgebras and coinduction |

12:20--13:50 | Jerzy Król | Breaking a general tovariance... |

4th meeting

Joint meeting of the Seminar on Quantum Field Theories & the Polish Seminar on Category Theory took place
on
Aleks Kissinger
(Computing Laboratory, Oxford University),
*Frobenius States and a Graphical Language for Multipartite Entanglement*

Marek Zawadowski
(Department of Mathematics, University of Warsaw),
*Monoidal categories, an introduction*

10:00 AM | Welcome coffee | |

10:30 AM | Marek Zawadowski | Monoidal categories, an introduction |

12:00 AM | Lunch | |

12:30 PM | Aleks Kissinger | Quantum mechanics and quantum computation |

1:30 PM | Coffee break | |

2:00 PM | Aleks Kissinger | Categorical quantum mechanics and the graphical calculus |

3:00 PM | Coffee break | |

3:30 PM | Aleks Kissinger | Graphs of many-body systems: the algebraic structure of entanglement |

4:30 PM | End of the meeting! | |

6:00 PM | Dinner at "U Szwejka"! |

*Frobenius States and a Graphical Language for Multipartite Entanglement*

Aleks Kissinger (Oxford University)

**Abstract:**
While multipartite quantum states constitute a key resource for quantum computations and protocols,
obtaining a high-level, structural understanding of entanglement involving arbitrarily many qubits
is a long-standing open problem in quantum computer science. We approach this problem by identifying
the close connection between a special class of highly entangled tripartite states, which we call
Frobenius states, and the standard notion of a commutative Frobenius algebra. We use these states
(and their induced algebras) as a primitive in a graphical language that is both universal for quantum
computation and capable of highlighting the behavioural differences in types of Frobenius states. This
graphical language then suggests methods for state preparation, classiﬁcation, and efﬁcient classical
modeling of certain kinds of quantum systems.

*Monoidal categories, an introduction*

Marek Zawadowski (MIM UW)

**Abstract:**
This talk is meant to be an introduction to the theory of monoidal
categories and some of its extensions. After reviewing the basic
notions concerning monoidal categories I will discuss the coherence,
the graphical language, and some 2-dimensional aspect of the theory.
Then I will present some extension of the notion of a monoidal
category: braided, autonomous, and traced categories among others.
These notions will be illustrated with some typical examples.

3rd meeting

The meeting took place on
Paweł Waszkiewicz
(Jagellonian University),
*V-enriched categories---an introduction*

Jerzy Król
(University of Silesia),
*Sheaves, categories, and physics*

10:30--12:00 | Paweł Waszkiewicz | V-enriched categories---an introduction |

12:20--13:50 | Jerzy Król | Sheaves, categories, and physics |

2nd meeting

The meeting took place on
Marek Zawadowski
(Depertment of Mathematics, University of Warsaw)
*An introduction to Higher-dimensional Categories*

Stanisław Szawiel
(Department of Mathematics, University of Warsaw),
*A Constructuion of Opetopic Sets*

10:30--12:00 | Marek Zawadowski | An introduction to Higher-dimensional Categories |

12:20--13:50 | Stanisław Szawiel | A Constructuion of Opetopic Sets |

1st meeting

The meeting took place on
Thomas Streicher
(Universität Darmstadt)
*Types and Kan Complexes*

10:15--11:15 | Thomas Streicher | Type Theory and its Categorical Models |

11:30--12:30 | Thomas Streicher | Basics of Simplicial Homotopy Theory |

12:45--13:45 | Thomas Streicher | Interpreting Type Theory in SSet and Voevodsky's Equivalence Axiom |

*Types and Kan Complexes*

Thomas Streicher (Universität Darmstadt)

**Abstract:**
Constructive type theory was introduced by Martin-Loef as a foundation for
constructive mathematics. Its impredicative version is implemented within the Coq system
which allows to construct proofs interactively as elements of a given type representing a
proposition. In this sense it provides a synthesis of (constructive) logic and functional
programming.

In order to make type checking decidable one has to distinguish between "judgemental"
and "propositional" equality. The former corresponds to "conversion" and is decidable
whereas the latter is (closer to) mathematical equality which is highly non-decidable.

This distinction between two notions of equality makes life a bit cumbersome. But
it allows one to interpret propositional equality as being isomorphic as in the Groupoid
Model of Hofmann and Streicher from 1993. Already there it was suggested that actually
types should not be interpretad as groupoids but as weak higher-dimensional groupoids".
The most accessible notion of weak higher dimensional groupoid is provided by Kan complexes
within the topos SSet of simplicial sets as suggested independently by Streicher and
Voevodsky in 2006.

Recently Voevodsky has shown that this model validates his "Equivalence Axiom"
stating that types are equal iff there is a "weak equivalence" between them. Here "weakly
equivalent" means that there is a map between the types which is surjective when this
condition is expressed in terms of propositional equality. The intention is that extending
Coq this way allows one to consider isomorphic types as equal as it is common in category
theory.

Our lectures are organized into 3 parts

1. Type Theory and its Categorical Models

2. Basics of Simplicial Homotopy Theory

3. Interpreting Type Theory in SSet and Voevodsky's Equivalence Axiom