We are happy to announce that Part I of the
MSCS Special Issue on Homotopy Type Theory and Univalent Foundations
has formally been published, and is available at
The articles making up this volume are listed, and briefly described,
below (copied from the preface).
We would like to thank the authors for their contribution and the
referees for their careful proof-reading and constructive criticism.
Part II is currently being prepared and will be formally published soon.
Valery Isaev, Indexed type theories
Valery Isaev, in his contribution "Indexed type theories", develops a
syntactic analog to indexed infinity-categories. These indexed type
theories behave to type theory like indexed infinity-categories behave
Isaev puts forth indexed type theory as a way to employ type-theoretic
language in the study of more general infinity-categories than models of
Homotopy Type Theory or infinity-topoi.
Auke B. Booij, Extensional constructive real analysis via locators
In "Extensional constructive real analysis via locators", Auke Booij
explores the formulation of constructive real analysis---a notoriously
difficult topic---in Univalent Foundations.
Booij defines real numbers equipped with a "locator"---additional
structure that allows one, for instance, to compute signed-digit
representations of such numbers.
The paper culminates in a constructively valid intermediate value
theorem that determines the root of a function including a locator.
Booij has implemented and computer-checked some of his results in the
computer proof assistant Coq; the source files are available in a public
Martín Hötzel Escardó, Injective types in univalent mathematics
Under which conditions can a function f : X -> D be extended along an
embedding X -> Y to a map Y -> D?
This question is studied in Martín Hötzel Escardó's "Injective types in
In particular, Escardó gives two characterizations of the "algebraically
injective types", i.e., those types D for which any map X -> D can be
Particular care is given to questions of universe levels and the need
for propositional resizing.
The results described in this paper are fully computer-checked in the
Agda computer proof assistant.
Cesare Gallozzi, Homotopy type-theoretic interpretations of constructive
The interpretation of constructive set theories in type theory is a
classic topic, dating back to the pioneering work of Peter Aczel in the
late 1970s. Cesare Gallozzi contributes to this line of work in his
"Homotopy type-theoretic interpretations of constructive set theories"
by also taking homotopical properties into account. To this end, the
paper introduces a stratification of models of constructive set theory
in type theory by homotopy (or truncation) levels. The models are
indexed by two parameters: the homotopy level of the underlying types,
and the homotopy level of the equivalence relation which interprets
equality in the models. These models are then studied from a
proof-theoretic perspective and compared with similar models, in
particular, a model of Håkon Gylterud is obtained as a special case of
Gallozzi's family of models.