12 December 2019, 14:00, CYB101

Speaker

Ed Morehouse, Taltech

Title

Double-Categorical Models of Directed Universes

Abstract

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.