Skip to main content

Peter LeFanu Lumsdaine: Computads, cell complexes, and theories, II

Time: Wed 2017-04-26 10.00 - 11.45

Location: Room 16, building 5, Kräftriket, Department of Mathematics, Stockholm University

Participating: Peter LeFanu Lumsdaine (SU)

Export to calendar

ABSTRACT: This is a continuation of my talk from March 15.  I look at logic  the “computads”/“cell complexes” picture from last time.  In particular, this will shed light on why:

(1) theories in algebraic or first-order logic are easy to define;

(2) theories in higher-order logic are less easy to define;

(3) theories in essentially algebraic and dependent-algebraic logic are rather hard to define;

(4) general dependent type theories are remarkably hard to define.

More precisely, (1) and (2) are computad-like situations, while (3) and (4) are cell-complex-like.