Guarded Cubical Type Theory

[Bas Spitters]

Our paper has just been accepted for CSL
(http://csl16.lif.univ-mrs.fr/). I believe this is one of the first
HoTT papers that makes progress on an problem that originated from
computer science (as opposed to maths).

While I am at it, three more HoTT papers have been accepted at CSL:
http://csl16.lif.univ-mrs.fr/accepted/
(abstracts below)

Guarded Cubical Type Theory: Path Equality for Guarded Recursion
Lars Birkedal, Aleš Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas
Spitters, Andrea Vezzosi

This paper improves the treatment of equality in guarded dependent
type theory (GDTT), by combining it with cubical type theory (CTT).
GDTT is an extensional type theory with guarded recursive types, which
are useful for building models of program logics, and for programming
and reasoning with coinductive types. We wish to implement GDTT with
decidable type-checking, while still supporting non-trivial equality
proofs that reason about the extensions of guarded recursive
constructions. CTT is a variation of Martin-L"of type theory in which
the identity type is replaced by abstract paths between terms. CTT
provides a computational interpretation of functional extensionality,
is conjectured to have decidable type checking, and has an implemented
type-checker. Our new type theory, called guarded cubical type theory,
provides a computational interpretation of extensionality for guarded
recursive types. This further expands the foundations of CTT as a
basis for formalisation in mathematics and computer science. We
present examples to demonstrate the expressivity of our type theory,
all of which have been checked using a prototype type-checker
implementation, and present semantics in a presheaf category.
https://arxiv.org/abs/1606.05223

---

Extending Homotopy Type Theory with Strict Equality
Thorsten Altenkirch, Paolo Capriotti, Nicolai Kraus
In homotopy type theory (HoTT), all constructions are necessarily
stable under homotopy equivalence. This has shortcomings: for example,
it is believed that it is impossible to define a type of
semi-simplicial types. More generally, it is difficult and often
impossible to handle towers of coherences. To address this, we propose
a 2-level theory which features both strict and weak equality. This
can essentially be represented as two type theories: an "outer" one,
containing a strict equality type former, and an "inner" one, which is
some version of HoTT. Our type theory is inspired by Voevosky's
suggestion of a homotopy type system (HTS) which currently refers to a
range of ideas. A core insight of our proposal is that we no not need
any form of equality reflection in order to achieve what HTS was
suggested for. Instead, having unique identity proofs in the outer
type theory is sufficient, and it also has the meta-theoretical
advantage of not breaking decidability of type checking. The inner
theory can be an easily justifiable extensions of HoTT, allowing the
construction of "infinite structure" which are considered impossible
in plain HoTT. Alternatively, we can set the inner theory to be
exactly the current standard formulation of HoTT, in which case our
system can be thought of as a type-theoretic framework for working
with "schematic" definitions in HoTT. As demonstrations, we define
semi-simplicial types and formalise constructions of Reedy fibrant
diagrams.
http://arxiv.org/abs/1604.03799

---
Kuen-Bang Hou and Michael Shulman.
The Seifert-van Kampen Theorem in Homotopy Type Theory
Homotopy type theory is a recent research area connecting type theory
with homotopy theory
by interpreting types as spaces. In particular, one can prove and
mechanize type-theoretic ana-
logues of homotopy-theoretic theorems, yielding “synthetic homotopy
theory”. Here we consider
the Seifert–van Kampen theorem, which characterizes the loop structure
of spaces obtained by
gluing. This is useful in homotopy theory because many spaces are
constructed by gluing, and
the loop structure helps distinguish distinct spaces. The synthetic
proof showcases many new
characteristics of synthetic homotopy theory, such as the
“encode-decode” method, enforced
homotopy-invariance, and lack of underlying sets.
http://www.cs.cmu.edu/~kuenbanh/files/vankampen.pdf

---
Ian Orton and Andrew Pitts.
Axioms for Modelling Cubical Type Theory in a Topos

The homotopical approach to intensional type theory views proofs of
equality as paths. We
explore what is required of an interval-like object I in a topos to
give a model of type theory in
which elements of identity types are morphisms from I. Cohen, Coquand,
Huber and Mörtberg
give such a model using a particular category of presheaves. We
investigate the extent to which
their model construction can be expressed in the internal type theory
of any topos and identify
a collection of quite weak axioms for this purpose. This clarifies the
definition and properties of
the notion of Kan filling that lies at the heart of their constructive
interpretation of Voevodsky’s
univalence axiom. Furthermore, since our axioms can be satisfied in a
number of different ways,
we show that there is a range of topos-theoretic models of homotopy
type theory in this style.
https://www.cl.cam.ac.uk/~rio22/pdf/cubsai_paper.pdf

[Michael Shulman]

These should all be added to the references page on the wiki:
https://ncatlab.org/homotopytypetheory/show/References
In general, anyone who writes or notices a HoTT-related paper should
feel free to add a citation and link there.

> --
> 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 HomotopyTypeThe...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Bas Spitters]

Done. Thanks for the reminder.
I've chosen to put them in only one category.
It would be better to have a tags system, but there seems to be no
easy way to connect this to the nlab/instiki.