Ed Morehouse, Taltech
Double-Categorical Models of Directed Universes
The Univalence principle of Homotopy Type Theory relates paths between types in a universe with functions that participate in an coherent equivalence, thus giving each universe of types the structure of a ∞-groupoid. We propose a framework in which the predicate on functions is made a parameter, permitting univalent universes of directed types. We further investigate the instance of this framework in which types are interpreted as categories and universes as double categories with connection structure.