Tamara von Glehn abstract and references

Title: Fibrations and models of type theory

Abstract: Dependent type theory can be interpreted in categories with sufficient structure: types are a specified class of morphisms, where substitution corresponds to pullback, quantifiers correspond to adjoints to pullback, and identity types arise from a weak factorisation system.

This talk will explore the category of these models of type theory. I will consider various ways new models can be built using standard categorical constructions, for example using gluing and fibrations, and look at what logical principles in the type theory are preserved by the process.

References

Background on categorical models of dependent type theory, and some constructions:

- M. Shulman, Univalence for inverse diagrams and homotopy canonicity, Mathematical Structures in Computer Science, 25:05, p1203--1277, 2015. https://arxiv.org/abs/1203.3253

- M. Hofmann and T. Streicher, The groupoid interpretation of type theory, In Twenty-five years of constructive type theory (Venice, 1995), volume 36 of Oxford Logic Guides, pages 83--111, Oxford University Press, 1998.

- T. Streicher, How Intensional is Homotopy Type Theory?, 2013. www.mathematik.tu-darmstadt.de/~streicher/barc_corr.pdf<http://www.mathematik.tu-darmstadt.de/~streicher/barc_corr.pdf>

 This talk:

- T. von Glehn, Polynomials and models of type theory, PhD thesis, University of Cambridge, 2015. https://www.repository.cam.ac.uk/handle/1810/254394

 

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.