# School of Mathematics

## Dr Nicola Gambino

Associate Professor

Pure Mathematics

### Contact details

Room: 9.15

Tel: +44 (0)113 3435143

Email: n.gambino @ leeds.ac.uk

### Keywords

Categorical Logic

Type theory

Computer-assisted proof-checking

Operads

Analytic functors

Polynomial functors

2-categories

Quillen model categories

## Research interests

I am a mathematician with research interests in mathematical logic, category theory, and theoretical computer science. Within mathematical logic, I am mainly nterested in type theory. In recent years, my work has focused on Homotopy Type Theory and Univalent Type Theories. Within category theory, I am interested in polynomial and analytic functors, species of structures, operads, Quillen model structures, 2-categories, and the connections between these topics.

### Useful links

Home page

AMS MathSciNet (Subscription required)

ArXiv

Google scholar

## Publications

**Awodey S, Gambino N, Sojakova K** Homotopy-initial algebras in type theory *Journal of the ACM*, **63**, 2017

DOI:10.1145/3006383

View abstract

**Gambino N, Sattler C** The Frobenius condition, right properness, and uniform fibrations *Journal of Pure and Applied Algebra*, 2016

DOI:10.1016/j.jpaa.2017.02.013

View abstract

**Awodey S, Gambino N, Palmgren E** Introduction– from type theory and homotopy theory to univalent foundations *Mathematical Structures in Computer Science*, **25**, 1005-1009, 2015

DOI:10.1017/S0960129514000474

View abstract

**Gambino N, Kock J** Polynomial functors and polynomial
monads *Mathematical Proceedings of the Cambridge Philosophical Society*, **134**, 153-192, 2013

DOI:10.1017/S0305004112000394

View abstract

**Awodey S; Gambino N; Sojakova K ** *Inductive types in homotopy type theory*Proceedings of the 2012 27th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, 95-104 2012

DOI:10.1109/LICS.2012.21

View abstract

**Gambino N, Fiore TM, Kock J** Double adjunctions and free monads *Cahiers de Topologie et Géométrie Differentielles Catégoriques*, **LIII**, 242-307, 2012

View abstract

**Fiore TM, Gambino N, Kock J** Monads in double categories *Journal of Pure and Applied Algebra*, **215**, 1174-1197, 2011

DOI:10.1016/j.jpaa.2010.08.003

View abstract

**Gambino N** Weighted limits in simplicial homotopy theory *Journal of Pure and Applied Algebra*, **214**, 1193-1199, 2010

DOI:10.1016/j.jpaa.2009.10.006

View abstract

**Awodey S, Gambino N, Lumsdaine PL, Warren MA** Lawvere-Tierney sheaves in Algebraic Set Theory *Journal of Symbolic Logic*, **74**, 861-890, 2009

DOI:10.2178/jsl/1245158088

View abstract

**Gambino N** The associated sheaf functor theorem in algebraic set theory *Annals of Pure and Applied Logic*, **156**, 68-77, 2008

DOI:10.1016/j.apal.2008.06.008

View abstract

**Gambino N** Homotopy limits for 2-categories *Mathematical Proceedings of the Cambridge Philosophical Society*, **145**, 43-63, 2008

DOI:10.1017/S0305004108001266

View abstract

**Gambino N, Garner R** The identity type weak factorisation theorem *Theoretical Computer Science*, **409**, 94-109, 2008

DOI:10.1016/j.tcs.2008.08.030

View abstract

**Fiore M, Gambino N, Hyland M, Wynskel G** The Cartesian
closed bicategory of generalised species of structures *Journal of the London Mathematical Society*, **77**, 203-220, 2008

DOI:10.1112/jlms/jdm096

View abstract

**Gambino N, Schuster P** Spatiality for formal topologies *Mathematical Structures in Computer Science*, **17**, 65-80, 2007

DOI:10.1017/S0960129506005810

View abstract

**Gambino N, Aczel P** The generalised type-theoretic interpretation of constructive set theory *Journal of Symbolic Logic*, **71**, 67-103, 2006

DOI:10.2178/jsl/1140641163

View abstract

**Gambino N** Heyting-valued interpretations for Constructive Set Theory *Annals of Pure and Applied Logic*, **137**, 164-188, 2006

DOI:10.1016/j.apal.2005.05.021

View abstract

**Gambino N** Presheaf Models for Constructive Set Theories In *From Sets and Types to Topology and Analysis: Towards Practicable Foundations for Constructive Mathematics*, 2005

DOI:10.1093/acprof:oso/9780198566519.003.0004

View abstract

**Gambino N, Hyland M** Wellfounded Trees and Dependent Polynomial Functors *Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)*, **3085**, 210-225, 2004

View abstract

**Aczel P, Gambino N** Collection principles in dependent type theory *Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)*, **2277 LNCS**, 1-23, 2002

View abstract

**Gambino N, Joyal A** On operads, bimodules and analytic functors *Memoirs of the American Mathematical Society*

View abstract

© Copyright Leeds 2011