Publications and slides

Research papers

1. Double adjunctions and free monads, written with T. M. Fiore and J. Kock
   Cahiers de Topologie et Géométrie Differentielles Catégoriques, Forthcoming.
   
2. Monads in double categories, written with T. M. Fiore and J. Kock
   Journal of Pure and Applied Algebra 215 (6) 2011, pp. 1174-1197.
   
3. Weighted limits in simplicial homotopy theory
   Journal of Pure and Applied Algebra 214 (7) 2010, pp. 1193-1199. 
4. 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.
5. The identity type weak factorisation system, with R. Garner
   Theoretical Computer Science 409 (1) 2008, pp. 94-109.
6. The associated sheaf functor theorem in Algebraic Set Theory
   Annals of Pure and Applied Logic 56 (1) 2008, pp. 68-77.
7. Homotopy limits for 2-categories 
   Mathematical Proceedings of the Cambridge Philosophical Society 145 (1) 2008, pp. 43-63.
8. The cartesian closed bicategory of generalised species of structures, written with M. Fiore, M. Hyland and G. Wynskel
   Journal of the London Mathematical Society 77 (2) 2008, pp. 203-220. 
9. Spatiality for formal topologies, written with P. Schuster
   Mathematical Structures in Computer Science 17 (1) 2007, pp. 65-80. 
10. Heyting-valued interpretations for constructive set theory
    Annals of Pure and Applied Logic 137 (1-3) 2006, pp. 164-188. 
11. The generalised type-theoretic interpretation of constructive set theory, written with P. Aczel
    Journal of Symbolic Logic 71 (1) 2006, pp. 67-103. 
12. 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.
13. 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.
14. 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.

Preprints

15. Inductive types in homotopy type theory, written with S. Awodey and K. Sojakova, ArXiv:1105.6206, 2012.
    
16. Polynomial functors and polynomial monads, written with J. Kock, ArXiv:0906:4931, 2010.

Survey papers

17. On the coherence conditions for pseudo-distributive laws, arXiv:0907:1359, 2009.

Slides of seminars and conference talks

• 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.