Nullable Compositions [talk]

Conference

International Congress on Mathematical Software (ICMS) 2020 - July 15, 2020

Speakers/authors

Favonia (assistant professor)

Abstract

Cubical type theory has come a long way to have univalent universes, higher inductive types, computational semantics, and Quillen equivalence to the standard homotopy theory. For it to be a foundation of practical tools, however, we still need more efficient normalization, type-checking, unification, and so on. One hot spot is compositions, the new gadget introduced in cubical type theory to impose proper higher-dimensional structure (fibrancy) in types. As an effort to eliminate compositions as much as possible, we have been considering variants of cubical type theory where there are no irreducible compositions at the zeroth dimension. I call these undesirable compositions as null compositions. To remove them, we have to kill all nullable compositions. We have found ways to implement this move in various cubical type theories, but a general solution is still lacking. This talk is an overview of what is currently known.

Keywords

type theory