Dear All, 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 https://www.cambridge.org/core/journals/mathematical-structures-in-computer-science/issue/8405D6FA1D4C76990B57C7E4ADD9A924 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. The editors Benedikt Ahrens Simon Huber Anders Mörtberg 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 to infinity-categories. 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 Git repository. 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 univalent mathematics". In particular, Escardó gives two characterizations of the "algebraically injective types", i.e., those types D for which any map X -> D can be extended constructively. 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 set theories 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. -- You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group. To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/HomotopyTypeTheory/f9a44347-79f7-fc0e-13c7-6c86f5eb8938%40gmail.com.