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 first 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 defined in each dimension by considering all possible “many-in-one-out”
pasting diagrams in the previous definition. Michael Makkai, in setting out his definition of weak higher
category using these shapes and his concept of a FOLDS signature, explicitly mentions the influence of type
theory in his thinking. In my second talk, I will give a type-theoretic prespective on the definition 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.
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.
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.
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) |
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... |
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, classification, and efficient 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.
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 |
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 |
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