Contents

Latest updates
 The paper Relative
pseudomonads, Kleisli bicategories, and substitution
monoidal structures, written with M. Fiore, M.
Hyland, and G. Winskel.
 The slides of two talks (Talk I
and Talk II) on Homotopy Type
Theory and Algebraic Model Structures, given by
Christian Sattler and me at the Journées du GDR
Topologie Algébrique held in Paris on December 2nd and
3rd, 2016.
 The paper The
Frobenius condition, right
properness, and uniform
fibrations, written with Christian Sattler.
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)
Publications
 S. Awodey, N. Gambino and K. Sojakova, Homotopyinitial
algebras in type theory.
Journal of the Association for Computing Machinery, to
appear. The associated Coq code is available here.
 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.
Older preprints.
 On the
coherence conditions for pseudodistributive laws,
arXiv:0907:1359, 2009.
Slides
of talks and links
 The slides of my talk Algebraic
models of homotopy type theory, given at the
International Category Theory conference (Halifax,
Canada), August 7th13th, 2016.
 The slides of a tutorial on Homotopy Type Theory at
the Young
Set Theory conference (Copenhagen, June 13th17th,
2016):
 "Aspects
of univalence", given at the minisimposyum on
Homotopy Type Theory and Univalent Foundations at DMV,
Hamburg, September 2015.
 "Univalent
foundations of mathematics and homotopical algebra",
given at the workshop Homotopical
Algebra and Geometry at Lancaster University,
April 2015.




Lectures
on Homotopy Type Theory, given by Dan Licata,
Peter LeFanu Lumsdaine and me at the Mathematical
Structures of Computation conference in Lyon, January
2014.









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 
