Contents

Latest updates
Research interests
 Mathematical Logic (constructive set theory, type
theory, categorical logic)
 Category Theory (2categories, homotopical algebra,
polynomial and analytic functors)
 Theoretical Computer Science (computerassisted
proofchecking)
Recent preprints
 N. Gambino and C. Sattler, Uniform
fibrations and the Frobenius condition,
ArXiv:1510.00669, 2015. Comments welcome!
 S. Awodey, N. Gambino and K. Sojakova, Homotopyinitial
algebras in type theory. ArXiv:1504.05531, 2015.
The associated Coq code is available here
Publications
 On operads,
bimodules and analytic functors, written with A.
Joyal
Memoirs of the
American Mathematical Society, to appear.
 Polynomial
functors and polynomial monads, written with J.
Kock.
Mathematical
Proceedings of the Cambridge Philosophical Society,
154 (1) 2013, pp. 153192.
 Inductive
types in Homotopy Type Theory, written with S.
Awodey and K. Sojakova
Proceedings of the
2012 27th Annual ACM/IEEE Symposium on Logic in
Computer Science (LICS 2012), pp. 95104.
The related Coq code is available on here.
 Double
adjunctions and free monads, written with T. M.
Fiore and J. Kock
Cahiers de Topologie
et Géométrie Differentielles Catégoriques, LIII
(4) 2012, pp. 242307.
 Monads in
double categories, written with T. M. Fiore and J.
Kock
Journal
of
Pure and Applied Algebra 215 (6) 2011, pp.
11741197.
 Weighted limits in
simplicial homotopy theory
Journal of Pure and
Applied Algebra 214 (7) 2010, pp. 11931199.
 LawvereTierney
sheaves in Algebraic Set Theory, written with S.
Awodey, P. L. Lumsdaine and M. A. Warren
Journal of
Symbolic Logic 73 (3) 2009, pp. 861890.
 The identity
type weak factorisation system, with R. Garner
Theoretical Computer
Science 409 (1) 2008, pp. 94109.
 The
associated sheaf functor theorem in Algebraic Set
Theory
Annals of
Pure and Applied Logic 56 (1) 2008, pp. 6877.
 Homotopy limits
for 2categories
Mathematical
Proceedings of the Cambridge Philosophical Society
145 (1) 2008, pp. 4363.
 The
cartesian closed bicategory of generalised species of
structures, written with M. Fiore, M. Hyland and
G. Winskel
Journal of the London
Mathematical Society 77 (2) 2008, pp.
203220.
 Spatiality
for formal topologies, written with P. Schuster
Mathematical
Structures in Computer Science 17 (1) 2007, pp.
6580.
 Heytingvalued
interpretations for constructive set theory
Annals of Pure and
Applied Logic 137 (13) 2006, pp.
164188.
 The
generalised typetheoretic interpretation of
constructive set theory, written with P. Aczel
Journal of Symbolic
Logic 71 (1) 2006, pp. 67103.
 Presheaf models
for Constructive Set Theories
In L. Crosilla and P. Schuster (editors), From
Sets and Types to Topology and Analysis, Oxford
University Press, 2005, pp. 6277.
 Wellfounded
Trees and Dependent Polynomial Functors, written
with M. Hyland
In S. Berardi and M. Coppo and F. Damiani (editors),
Types for proofs and programs, Lecture Notes in
Computer Science 3085, Springer (2004), pp. 210225.
 Collection
Principles in Dependent Type Theory, written with
P. Aczel
In Z. Luo and J. McKinna and R. Pollack (editors),
Types for proofs and programs, Lecture Notes in
Computer Science 2277, Springer (2002), pp. 123.
Old preprints.
 On the
coherence conditions for pseudodistributive laws,
arXiv:0907:1359, 2009.
Slides
of talks and links
PhD
students
 Jakob Vidmar (started in September 2014)
 Cesare Gallozzi (started in October 2014)
 Raffael Stenzel (started in September 2015)
 Marco Larrea Schiavon (started in September 2015)
Editorial duties
Teaching
Old
teaching (in Italian)
Some links
Contact
details
Postal
address

School of Mathematics


University of
Leeds 

Leeds LS2 9JT 

United Kingdom 


Office 
9.15 of the School of Mathematics 
Phone 
+44 (0)113 343 51 43 
Fax 
+44 (0)113 343 5090 
Email 
n.gambino AT leeds.ac.uk 
Web 
http://www.maths.leeds.ac.uk/~pmtng 
