Wed 10 Jan 2018 17:05 - 17:30 at Watercourt - Types Chair(s): Thorsten Altenkirch

Category theory in homotopy type theory is intricate as categorical laws can only be stated “up to homotopy”, and thus require coherences. The established notion of a univalent category (Ahrens et al. 2015) solves this by considering only truncated types, and it roughly corresponds to an ordinary category. The drawback is that univalent categories fail to capture many naturally occurring structures, such as type universes or the type of univalent categories themselves. This stems from the fact that the natural notion of a category in homotopy type theory is not that of an ordinary, but rather a higher category.

Out of the large variety of approaches to higher category theory that mathematicians have proposed, we believe that, for type theory, the simplicial strategy is best suited. Given the first (n+3) levels of a semisimplicial type S, we can equip S with three properties: first, contractibility of the types of certain horn fillers; second, a completeness property; and third, a truncation condition. We call this a complete semi-Segal n-type.

The definition of a univalent (1-) category by (Ahrens et al. 2015) can easily be extended or restricted to the definition of a univalent n-category (more precisely, (n,1)-category) for $n \in {0,1,2}$, and we show that the type of complete semi-Segal n-types is equivalent to the type of univalent n-categories in these cases. Thus, we believe that the notion of a complete semi-Segal n-type can be taken as the definition of a univalent n-category.

We develop most of the material of the paper without assuming truncatedness conditions. While this makes some of the intermediate categorical notions not completely well-behaved, or “wild”, it has the advantage of making our constructions more modular, since every new level of wild structure can be built on top of the previous levels.

The paper comes with an electronic appendix containing a formalisation in the proof assistant Agda using a completely explicit representation of semi-simplicial types for levels up to 4.

Wed 10 Jan

 15:50 - 17:30: Research Papers - Types at Watercourt Chair(s): Thorsten AltenkirchUniversity of Nottingham 15:50 - 16:15Talk A Principled approach to Ornamentation in MLThomas WilliamsInria, Didier RémyInria 16:15 - 16:40Talk Type-Preserving CPS Translation of Σ and Π Types is Not Not PossibleWilliam J. BowmanNortheastern University, USA, Youyou CongOchanomizu University, Japan, Nick RiouxNortheastern University, USA, Amal AhmedNortheastern University, USA Link to publication DOI Pre-print 16:40 - 17:05Talk Safety and Conservativity of Definitions in HOL and Isabelle/HOLOndřej KunčarTechnische Universität München, Germany, Andrei PopescuMiddlesex University, London 17:05 - 17:30Talk Univalent Higher Categories via Complete Semi-Segal TypesPaolo CapriottiUniversity of Nottingham, Nicolai KrausUniversity of Nottingham