Part I of MSCS Special Issue on HoTT/UF published

[Benedikt Ahrens]

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.