[HoTT] Part I of MSCS Special Issue on HoTT/UF published

[HoTT] 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.




-- 
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.