Unified framework for the ingestion of early epidemic data for downstream data analytics
 Kamau, E Kelly, S Darji, D Baidjoe, A Brownstein, J Campbell, F Dasgupta, A Degail, M Demidova, A Ferretti, L Han, A Koyie, S Ngamala, P Polain, O Rojek, A Sauer, J Scarpino, S Sewalk, K Sopko, J Zakrzewski, S Merson, L Kraemer, M Wellcome Open Research volume 10 524-524 (08 May 2026)
Mon, 18 May 2026
16:30
L5

Algebraic type theory 

Steve Awodey
(Carnegie Mellon University)
Abstract
A representable natural transformation u : U* —> U in the category Psh(C) of presheaves on a small category C is a “natural model" of dependent type theory. The type-forming operations may be described as an algebraic structure on u, representing corresponding operations on the type-families classified by u. For example, the dependent product or “Pi-type” is an algebra structure for the polynomial endofunctor
 
P_u : Psh(C) —> Psh(C) .
 
Similar operations on u represent the other type-formers of unit type, dependent sums, and identity types. The latter are given by a recently determined “path-type” structure, which relates such models to cubical (Quillen) model categories.
Add to calendar
Flow interactions and forward flight dynamics of tandem flapping wings
 Fang, F Mavroyiakoumou, C Ristroph, L Shelley, M Journal of Fluid Mechanics volume 1034 (08 May 2026)

Awards for Excellence

We are very pleased to announce that the annual Awards for Excellence scheme is now open. The scheme enables the department to recognise exceptional performance during the period April 2025 – April 2026 with a monetary award.

‘Exceptional performance’ is classed as:

Subscribe to