Speaker:

Krzysztof Kapulkin

Thursday, July 25, 2013 - from 14:00
to 14:40

Abstract:

The Univalent Foundations Program is a new approach to the foundations
of mathematics, proposed by Vladimir Voevodsky (IAS, Princeton),
inspired by the homotopy-theoretic models of constructive type theory.
It builds on the existing language of Martin-Lof Type Theory (which is
the underlying language of many interactive proof assistants, such as
Coq and AGDA), to which it adds a new axiom, called the Univalence
Axiom. This axiom is not valid in the types-as-sets interpretation of type
theory, but it holds in (and was, in fact, inspired by) the model of type
theory in Kan complexes.
The language of the Univalent Foundations is particularly suitable
for developing homotopy theory synthetically, allowing only constructions
and proofs that are homotopy-invariant. Recent advances in this
approach include calculations of some homotopy groups of spheres and
a synthetic proof of Blakers{Massey Theorem.
Working in Voevodskys program we begin to systematically develop
category theory. We rst dene precategories which have an arbitrary
type as its type of objects, but the type of morphism is required to satisfy
the principle of Uniqueness of Identity Proofs, allowing one to talk about
equality of morphisms. Categories (or univalent categories) are required
to satisfy an additional condition, which is a version of the Univalence
Axiom.
For such (univalent) categories we start developing the theory: we
dene adjunctions, equivalences, the Yoneda embedding (showing that it
is full and faithful). We moreover prove that for categories, the notion of
equality is the same as the notion of categorical equivalence and thus, in
our system, every property of categories is automatically invariant under
equivalence.
Finally, we show that the inclusion of categories into precategories
admits a left adjoint (in the bicategorical sense) and the components of
the unit of this adjunction are categorical equivalences. In the homotopytheoretic
models of type theory, this can be seen as a truncated version
of the Rezk completion of a Segal space or the stack completion of a
prestack. (Joint work with Benedikt Ahrens and Michael Shulman.)