Dr Nicola Gambino

• Category Theory
• Logic
  
• Theoretical Computer Science
  

Information

• CV
• BibTex file
  

1. Kripke-Joyal forcing for type theory and uniform fibrations, written with S. Awodey and S. Hazratpour
   Selecta Mathematica - New Series, to appear.
   
2. Monoidal Kleisli Bicategories and the Arithmetic Product of Coloured Symmetric Sequences, written with R. Garner and C. Vasilakopoulou
   Documenta Mathematica, 29 (3), 2024, pp. 627-702.
   
3. 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.
4. 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.
5. 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.
   
6. Towards a constructive simplicial model of Univalent Foundations, with S. Henry
   Journal of the London Mathematical Society, 105 (2), 2022, pp. 1073-1109.
   
7. On the formal theory of pseudomonads and pseudodistributive laws, with G. Lobbia
   Theory and Applications of Categories, 37 (2), 2021, pp. 14-56.
   
8. 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.
9. The Frobenius condition, right properness, and uniform fibrations, written with C. Sattler
   Journal of Pure and Applied Algebra, 221 (12), 2017, pp. 3027-3068.
   
10.  Homotopy-initial algebras in type theory. written with S. Awodey and K. Sojakova
    Journal of the Association for Computing Machinery, 63 (6), 2017, 45pp.
    
11. On operads, bimodules and analytic functors, written with A. Joyal
    Memoirs of the American Mathematical Society, 249 (1184), 2017, (v) + 110pp.
    
12. Polynomial functors and polynomial monads, written with J. Kock.
    Mathematical Proceedings of the Cambridge Philosophical Society, 154 (1) 2013, pp. 153-192.
    
13. 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.
    
14. Monads in double categories, written with T. M. Fiore and J. Kock
    Journal of Pure and Applied Algebra 215 (6) 2011, pp. 1174-1197.
    
15. Weighted limits in simplicial homotopy theory
    Journal of Pure and Applied Algebra 214 (7) 2010, pp. 1193-1199. 
16. 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.
17. The identity type weak factorisation system, with R. Garner
    Theoretical Computer Science 409 (1) 2008, pp. 94-109.
18. The associated sheaf functor theorem in Algebraic Set Theory
    Annals of Pure and Applied Logic 56 (1) 2008, pp. 68-77.
19. Homotopy limits for 2-categories 
    Mathematical Proceedings of the Cambridge Philosophical Society 145 (1) 2008, pp. 43-63.
20. 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. 
21. Spatiality for formal topologies, written with P. Schuster
    Mathematical Structures in Computer Science 17 (1) 2007, pp. 65-80. 
22. Heyting-valued interpretations for constructive set theory
    Annals of Pure and Applied Logic 137 (1-3) 2006, pp. 164-188. 
23. 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.

• The calculus of analytic functors, Innovation Lectures, Faculty of Science, Masaryk University, December 2023: Lecture 1, Lecture 2, Lecture 3, Lecture 4
• Categorical Logic, AILA Summer School, August 2023
  
• Two-dimensional categorical logic, Logic Colloquium 2023, University of Milan, June 2023.
  
• The effective model structure, Algebraic Topology Seminar, University of Sheffield, April 2023.
  
• A new monoidal bicategory: categorical symmetric sequences and the arithmetic product, San Diego Seminar on Categories and Types, November 2022.
• Type theory: from functional programming to higher categories, Pure Mathematics Colloquium, University of Manchester, November 2022.
  
• The effective model structure, Topology Seminar, École Polytechnique Fédérale de Lausanne, November 2022
• Differential lambda-calculus and analytic functors, Annual Meeting of the Associazione Italiana per la Logica e le sue Applicazioni, Caserta, September 2022.
  
• The matrix product of coloured symmetric sequences, 2nd Workshop on Polynomial Functors, online, March 2022.
  
• Towards a constructive simplicial model of Univalent Foundations (long version), Mathematical Logic and Constructivity, Stockholm, August 2019.
  
• Towards a constructive simplicial model of Univalent Foundations (short version), International Conference on Homotopy Type Theory 2019, CMU, August 2019
  
• Syntax and semantics of dependent type theories, Summer School on Higher Topos Theory and Univalent Foundations, Leeds, June 2019.
  
• An introduction to CZF,  Seminario de Logica Matematica XXIX #10, Lisbon, January 2018.
• Two talks (Talk I, Talk II) 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 (Type Theory,  Homotopical Algebra, Homotopical models of type theory, Univalent Foundations)
• "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.
• A unified approach to Univalent Foundations and Homotopical Algebra, TLCA-RTA, Vienna, July 2014.
• 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.
• The bicategory of operads is cartesian closed, BMC (Special session on Category Theory), Sheffield, 2013.
• An introduction to Homotopy Type Theory, Department of Computer Science seminar, University of Leicester, March 15th, 2013.
  
• Syntax for dependent type theories, Proof Theory and Constructivism Seminar, Leeds, February 20th, 2013.
  
• Il programma "Univalent Foundations of Mathematics" di Vladimir Voevodsky (in Italian), Palermo, May 17th, 2012.
  
• Constructive Mathematics in Constructive Set Theory, Second MALOA Training Workshop, Leeds, June 30th, 2011. 
• Homotopy-theoretic aspects of Martin-Löf type theory, Logic Colloquium 2010, Paris, July 30th, 2010.
• Polynomial Functors and Polynomial Monads, Leeds Symposium in Proof Theory and Constructivism, July 13th 2009.
• Lectures on Dependent Type Theories, Midlands Graduate School 2009, Leicester, March 30th - April 3rd, 2009.

• Yorkshire and Midlands Category Theory Seminar (YaMCATS)
• Bicategories, categorification and quantum theory, London Mathematical Society Research School, Leeds, July 11th-15th, 2022
  
• Summer School on Higher Topos Theory and Univalent Foundations, University of Leeds, June 24th-29th, 2019
  
• 101st Peripatetic Seminar on Sheaves and Logic, Leeds, September 16th-17th, 2017
• Logic Colloquium 2016, University of Leeds, July 31st-August 6th, 2016
  
• 96th PSSL, University of Palermo (Italy), celebrating the 60th birthday of Pino Rosolini, 2014
  
• Type theory, homotopy theory and Univalent Foundations, CRM, Barcelona, 2013

Postdoctoral Research Fellows (past and present)

• Raffael Stenzel (2024-present)
  
• Giacomo Tendas (2024-present)
  
• Adrian Miranda (2023-present)
  
• Federico Olimpieri (2021-2024)
• Zeinab Galal (2021-2023)
• Sina Hazratpour (2019-2020)
  
• Karol Szumiło (2018-2020)
• Christian Sattler (2014-2017)
  

• Ngo Hang-Chan (2024-present)
  
• Bruno Lindan (2024-present)
  
• Calum Hughes (2022-present)
• Florrie Verity (2021-present)
• Matteo Spadetto, On the syntax and the semantics of propositional dependent type theories, 2024
• Luca Mesiti, Aspects of 2-dimensional elementary topos theory, 2024.
  
• Andrew Slattery, Commutativity of Relative Pseudomonads, 2024
  
• Gabriele Lobbia, Pseudomonads, relative monads and strongly finitary notions of multicategory, 2022
  
• Raffael Stenzel, On univalence, Rezk completeness and presentable quasi-categories, 2019
  
• Marco Larrea, Models of dependent type theory from algebraic weak factorisation systems, 2018
  
• Jakob Vidmar, Polynomial functors and W-types for groupoids, 2019
  
• Cesare Gallozzi, Homotopy Type-Theoretic Interpretations of Constructive Set Theories, 2018