Abstract Milly Maietti


Categorical methods play a prominent role in model theory of foundations for constructive mathematics based on type theory.

In this talk we focus on some notions of quotient completion of suitable Lawvere doctrines  introduced in j.w.w G. Rosolini [3,4].

Based on j.w.w F. Pasquali and G. Rosolini, we describe some applications to the tripos-to-topos constructions [1], to a tripos-to-quasi-topos construction and to models of foundations for constructive mathematics [2,5] including a predicative version of Hyland's Effective Topos built in j.w.w S. Maschio.

[1] J.M. Hyland, P. T. Johnstone and A.M.Pitts Tripos theory. Math.Proc.Cambridge Philos.Soc.88, 205-232, 1980.

[2] M.E. Maietti. A minimalist two-level foundation for constructive mathematics. Annals of Pure and Applied Logic, 160(3):319-354, 2009.

[3] M.E. Maietti and G. Rosolini. Elementary quotient completion. Theory and Applications of Categories, 27(17):445–463, 2013.

[4] M.E. Maietti and G. Rosolini. Unifying Exact Completions. Applied Categorical Structures 23(1):43-52,2015

[5]  Nordstrom, B., Petersson, K., Smith, J.: Programming in Martin Lof's Type Theory. Clarendon Press, Oxford (1990)

Share this page:

Contact details

Department of Mathematics
University of Leicester
University Road
Leicester LE1 7RH
United Kingdom

Tel.: +44 (0)116 229 7407

Campus Based Courses

Undergraduate: mathsug@le.ac.uk
Postgraduate Taught: mathspg@le.ac.uk

Postgraduate Research: pgrmaths@le.ac.uk

Distance Learning Course  

Actuarial Science:

DL Study

Student complaints procedure

AccessAble logo

The University of Leicester is committed to equal access to our facilities. DisabledGo has detailed accessibility guides for College House and the Michael Atiyah Building.