Contents

Latest updates
Research interests
 Mathematical Logic (Categorical Logic, Type Theory,
Constructive Set Theory)
 Category Theory (2categories, Homotopical Algebra,
polynomial and analytic functors)
 Theoretical Computer Science (computerassisted
proofchecking)
Publications
 Relative
pseudomonads, Kleisli bicategories, and substitution
monoidal structures, with M. Fiore, M. Hyland, and
G. Winskel
Selecta Mathematica  New Series. To
appear.
 The
Frobenius condition, right properness, and uniform
fibrations, written with C. Sattler
Journal of Pure and Applied Algebra, 221 (12),
2017, pp. 30273068.
 Homotopyinitial
algebras in type theory. written with S. Awodey
and K. Sojakova
Journal of the Association for Computing Machinery, 63
(6), 2017, 45pp.
 On operads,
bimodules and analytic functors, written with A.
Joyal
Memoirs of the
American Mathematical Society, 249 (1184),
2017, (v) + 110pp.
 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 Geometrie Differentielles Categoriques, 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.
Older preprints
 On the
coherence conditions for pseudodistributive laws,
arXiv:0907:1359, 2009.
Slides
of talks
 Two talks on algebraic model structures, by Christian
Sattler and me, Journées du GDR Topologie Algébrique,
Paris, 2016
 Algebraic models
of homotopy type theory International Category
Theory conference, Halifax, 2016.
 Tutorial on Homotopy Type Theory, Young Set Theory,
Copenhagen, 2016:
 "Aspects of
univalence", Homotopy Type Theory and Univalent
Foundations at DMV, Hamburg, 2015.
 "Univalent foundations
of mathematics and homotopical algebra",
Homotopical Algebra and Geometry, Lancaster, 2015.

 On the bicategory
of operads and analytic functors, International
Category Theory Conference, Cambridge, 2014.
 Lectures
on Homotopy Type Theory, (Dan Licata, Peter LeFanu
Lumsdaine and me), Mathematical Structures of
Computation, Lyon, 2014.








Conferences and workshops
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
Postgraduate
teaching
Some links
Contact
details
Postal
address

School of Mathematics


University of Leeds 

Leeds LS2 9JT 

United Kingdom 


Office 
Room 9.15, 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 
