Minisymposium on categorification and foundations of mathematics and quantum theory

9:15- 10:05: Bas Spitters (Radboud University, Nijmegen)

Bohrification: Topos theory and quantum theory

Abstract. Bohrification associates to a (unital) C*-algebra
* the Kripke model, a presheaf topos, of its classical contexts;
* in this Kripke model a commutative C*-algebra, called the Bohrification
* the spectrum of the Bohrification as a locale internal in Kripke model.

We will survey this technique, provide a short comparison with the related work by Isham and co-workers, which motivated Bohrification, and use sites and geometric logic to give a concrete external presentation of the internal locale. The points of this locale may be physically interpreted as (partial) measurement outcomes.

10:15 - 11:05: Thierry Coquand (Chalmers)

About the Kan simplicial set model of type theory

11:15 - 12:05: Volodymyr Mazorchuk (Uppsala)

2-categories, 2-representations and applications

Abstract. In this talk I plan to explain what a 2-category is, how 2-categories appear in algebra and topology, how one can study them, in particular, how one constructs 2-representations of 2-categories, and, finally, how all this can be applied.

13:30 - 14:20: Erik Palmgren (Stockholm)

Proof-relevance of families of setoids and identity in type theory

Abstract. Families of types are fundamental objects in Martin-Löf type theory. When extending the notion of setoid (type with an equivalence relation) to families of setoids, a choice between proof-relevant or proof-irrelevant indexing appears. It is shown that a family of types may be canonically extended to a proof-relevant family of setoids via the identity types, but that such a family is in general proof-irrelevant if, and only if, the proof-objects of identity types are unique. A similar result is shown for fibre representations of families. The ubiquitous role of proof-irrelevant families is discussed.

14:30 - 15:20: Nils Anders Danielsson (Chalmers)

Bag equality via a proof-relevant membership relation.

Abstract. Two lists are "bag equal" if they are permutations of each other, i.e.
if they contain the same elements, with the same multiplicity, but perhaps not in the same order. I will describe how one can define bag equality as the presence of bijections between sets of membership proofs. This definition has some nice properties:

* Many bag equalities can be proved using a form of equational
reasoning.

* The definition generalises easily to arbitrary unary containers,
including types with infinite values, such as streams.

* By using a small variant of the definition one gets set equality
instead, i.e. equality where neither multiplicity nor order matters.
Other variations give the subset and subbag preorders. Many
preservation properties—such as "the list monad's bind operation
preserves bag equality"—can be proved uniformly for all these
relations at once, thus avoiding proof duplication.

* The definition works well in mechanised proofs.

(This symposium is arranged by the Logic Seminar)

All welcome!

Erik Palmgren