Dr Nicola Gambino

Reader in Pure Mathematics
Department of Mathematics
University of Manchester

Member of the Algebra, Logic and Number Theory group

Research Interests



On-line repositories


Papers in journals
  1. Models of Martin-Löf type theory from algebraic weak factorisation systems, written with M. F. Larrea
    Journal of Symbolic Logic, 88 (1), 2023, pp. 242-289.
  2. The effective model structure and ∞-groupoid objects, written with S. Henry, C. Sattler and K. Szumiło
    Forum of Mathematics, Sigma, Volume 10, Vol. 10:e34, 2022, pp. 1–59.
  3. The constructive Kan-Quillen model structure: two new proofs, written with C. Sattler and K. Szumiło
    The Quarterly Journal of Mathematics, 
    73 (4), 2022, pp. 1307–1373.
  4. Towards a constructive simplicial model of Univalent Foundations, with S. Henry
    Journal of the London Mathematical Society, 105 (2), 2022, pp. 1073-1109.
  5. On the formal theory of pseudomonads and pseudodistributive laws, with G. Lobbia
    Theory and Applications of Categories, 37 (2), 2021, pp. 14-56.
  6. Relative pseudomonads, Kleisli bicategories, and substitution monoidal structures, with M. Fiore, M. Hyland, and G. Winskel
    Selecta Mathematica - New Series, 24 (3), 2018, pp. 2791-2830.
  7. The Frobenius condition, right properness, and uniform fibrations, written with C. Sattler
    Journal of Pure and Applied Algebra, 221 (12), 2017, pp. 3027-3068.
  8.  Homotopy-initial algebras in type theory. written with S. Awodey and K. Sojakova
    Journal of the Association for Computing Machinery, 63 (6), 2017, 45pp.
  9. On operads, bimodules and analytic functors, written with A. Joyal
    Memoirs of the American Mathematical Society, 249 (1184), 2017, (v) + 110pp.
  10. Polynomial functors and polynomial monads, written with J. Kock.
    Mathematical Proceedings of the Cambridge Philosophical Society, 154 (1) 2013, pp. 153-192.
  11. Double adjunctions and free monads, written with T. M. Fiore and J. Kock
    Cahiers de Topologie et Geometrie Differentielles Categoriques, LIII (4) 2012, pp. 242-307.
  12. Monads in double categories, written with T. M. Fiore and J. Kock
    Journal of Pure and Applied Algebra 215 (6) 2011, pp. 1174-1197.
  13. Weighted limits in simplicial homotopy theory
    Journal of Pure and Applied Algebra 214 (7) 2010, pp. 1193-1199. 
  14. Lawvere-Tierney sheaves in Algebraic Set Theory, written with S. Awodey, P. L. Lumsdaine and M. A. Warren
    Journal of Symbolic Logic 73 (3) 2009, pp. 861-890.
  15. The identity type weak factorisation system, with R. Garner
    Theoretical Computer Science 409 (1) 2008, pp. 94-109.
  16. The associated sheaf functor theorem in Algebraic Set Theory
    Annals of Pure and Applied Logic 56 (1) 2008, pp. 68-77.
  17. Homotopy limits for 2-categories 
    Mathematical Proceedings of the Cambridge Philosophical Society 145 (1) 2008, pp. 43-63.
  18. 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. 203-220. 
  19. Spatiality for formal topologies, written with P. Schuster
    Mathematical Structures in Computer Science 17 (1) 2007, pp. 65-80. 
  20. Heyting-valued interpretations for constructive set theory
    Annals of Pure and Applied Logic 137 (1-3) 2006, pp. 164-188. 
  21. The generalised type-theoretic interpretation of constructive set theory, written with P. Aczel
    Journal of Symbolic Logic 71 (1) 2006, pp. 67-103. 

Papers in refereed conference proceedings

  1. 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. 95-104.
    The related Coq code is available on here.
  2. 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. 62-77.
  3. 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. 210-225.
  4. 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. 1-23.
Slides of talks
Conferences and workshops

Postdoctoral Research Fellows (past and present)

PhD students (past and present)
Contact details

Postal address: Department of Mathematics, University of Manchester, Alan Turing building, Oxford Road, Manchester M13 9PL, United Kingdom
Phone:  +44 (0)161 275 58 64
Email: nicola.gambino AT manchester DOT ac DOT uk
Web: https://personalpages.manchester.ac.uk/staff/nicola.gambino
Office: Room 2.106.

This page was last updated on April 28th, 2023.