Webpage of the Compositional Systems and Methods group at TalTech.

12 December 2019, 14:00, CYB101


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.