Date: January 28, 2015 at 7:06:38 AM EST
From: "Boris Zilber" <zilber@maths.ox.ac.uk>
To: <kmb120205@googlemail.com>, <vladimir@ias.edu>
Cc: <zilber@maths.ox.ac.uk>
Reply-To: "Boris Zilber" <zilber@maths.ox.ac.uk>
Subject: TLMS 141108-Voevodsky: discussion

Dear Vladimir,
at this stage we have obtained a quick advice of an expert on your paper presented to TLMS. As you can see below it is overall very positive and advises us on publishing the paper. Nevertheless it also suggest to extend the introductory part of the paper (and perhaps some inner sections) to help the reader (see the last 4 lines of the report below). The Editors and I feel the same and hope that you will be able to do the appropriate revision quickly.  
Best regards
Boris Zilber

Referees report (quick advice): 

Prof. Voevodsky is developing a new and exciting foundational approach to
mathematics which he calls Univalent Foundations (UF). UF might change the
way we do mathematics in the future. This approach is based on type theory
instead of set theory. An important part of this project is to understand the
meta-theory of type systems. The meta-theory has a syntactic side and a se-
mantic side. The syntactic side deals with defining carefully what a type theory
is. The semantic side deals with relating type theories to other mathematical
structures such as categories (with certain properties). This is known as cate-
gorical semantics . The paper under consideration which deals with trhe syntax
defines B-systems which formalise the notion of a type system. It relates this
notion to that of a C-system (which Voevodsky introduced earlier) which is an-
other syntactical object closer to the semantics in categories. The notion of a
B-system is very important. It will lead to a big clarification and simplification
of the categorical semantics of type theories, and will also allow for a construc-
tive approach to semantics. This paper is a very important part of Voevodsky's
project and it is important publish it. The main remark I have about the paper
is that the introduction should explain the ideas behind B-systems and their
position in the overall project, and how this differs from other approaches. A
few more explanations in the body of the paper would also be helpful to the
reader