12.dets, 14:00 CYB-101 Ed Morehouse "Double-Categorical Models of Directed Universes"
Tarkvarateaduse instituudi seminaril neljapäeval, 12.12.2019 kell 14:00 esineb Ed Morehouse teemal "Double-Categorical Models of Directed Universes".
Seminar toimub ruumis CYB-101.
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.