LOGIKSEMINARIET STOCKHOLM-UPPSALA


Richard Garner (Cambridge)

ger ett föredrag med titeln

      Topological and higher-dimensional aspects of type theory

kl 10.30, 29 april i sal Eng 2-0022, Uppsala universitet (i Filosofiska
institutionens lokaler vid Engelska parken).

Abstract

It was observed by Hofmann and Streicher in the 1990s that, in Martin-Löf's
intensional type theory, it is possible to endow each type with a groupoid
structure, by taking as the ``type of morphisms'' from an element a to an
element b, the identity type Id(a,b). However, it was made clear even at
this time that this was not the end of the story. Indeed, the associativity
and unitality axioms for this type-theoretic groupoid do not hold
on-the-nose, but only up to propositional equality. Thus, if we are to
obtain a genuine groupoid from a type, we must first quotient out by
propositional equality.

A similar phenomenon occurs in the construction of the fundamental group of
a topological space: in order that the group operation should be associative
on-the-nose, one must quotient out paths by the homotopy relation. This
suggests the following analogy: that types are like topological spaces, and
that propositional equality is like the homotopy relation. Remarkably, it
turns out that this analogy can be made into something precise.

The purpose of this talk is to give an overview of the growing body of work
which exploits this connection, and to describe some of the challenges that
remain.




_______________________________________________
logik@math.su.se mailing list.
To unsubscribe or change your subscription options:
https://www2.math.su.se/mailman/options/logik?UserOptions=3Dedit

Seminar homepage: http://www.math.su.se/~jesper/seminarier/