Bicubical Directed Type Theory
Many structures in mathematics and computer science include a notion of a directed transition (or morphism), and when working with such structures one intends to always preserve this directed structure as an invariant. Homotopy type theory provides a setting in which all constructions preserve morphism structure, but only supports invertible morphisms. Directed type theory is an extension of homotopy type theory that also accounts for directed morphisms. Bicubical directed type theory is a constructive model of type theory in which every type comes packaged with two special types: one of (undirected) paths in the type and another of morphisms (i.e. directed paths). This work is an extension of the cartesian cubical model of type theory [Angiuli et al., 2017] and the bisimplicial model of directed type theory [Riehl and Shulman, 2017]. For a type A and terms x y : A, we write Path_A x y to denote the type of paths from x to y and Hom_A x y denotes the type of morphisms from x to y. The model is “bicubical” as the data for paths and morphisms in a type can each be represented by a cubical data-structure. We add this basic infrastructure to extensional type theory (i.e. dependent type theory with equality and uniqueness of identity proofs), and then use the internal logic of the type theory to describe and reason about the path and morphism structure of types—a technique first described in Orton and Pitts [2017].
In particular, we care about the various ways in which a dependent type can be fibrant: The general idea is that, given a type A and family of types B : A → Type, we want to know when path and/or morphism structure in A can be lifted to some structure in the type family B. When such structure is defined in B for every path in A, we call B a fibration. As an example, an important instance of this is called a coercion structure: If B : A → Type has a coercion structure, then any path p : Path_A x y uniquely determines a function coe_B p : B x → B y.
Given each notion of fibration we define, we can internally construct a corresponding universe of types paired with the desired fibration structure using the construction described in Licata et al. [2018]. Take for example UCoe: Given A : Type, any dependent type B : A → UCoe is always equipped with a coercion structure coe_B.
Lastly, we consider the different univalence structures each universe exhibits. Univalence struc- tures provide an internal interpretation for paths and/or morphisms in the universe. For example, univalence for paths in a universe U generally refers to the construction of an equivalence between the type of paths Path_U A B and the type of equivalences A ≃ B (i.e. pairs of invertible functions between A and B). As our primary contribution, we construct a universe UCov that is suitably fibrant with respect to both paths and morphisms, we prove it is closed under all the type-formers in the type theory, we build univalence for paths, and additionally we construct directed univalence: There is an equivalence between the function space A → B and the morphism space Hom_UCov A B for every A and B in UCov. As a caveat, the full proof of directed univalence is currently not entirely constructive; specifically, the proof that for every morphism p : Hom_UCov A B there is a path between p and its roundtrip through the equivalence uses a nonconstructive axiom.
Having presented this new model of type theory, we suggest how directed univalence can be useful for functional programming and when formalizing (meta)theory of computational structures. We have formalized all of our results using the Agda proof-assistant.