restriction-categories

This is a formalisation of restriction categories inspired by a series of lectures given by Robin Cockett during his sabatical visit to IoC, Tallinn in early 2013:

http://cs.ioc.ee/~tarmo/tsem12/cockett.html

Authors: James Chapman, Tarmo Uustalu, Niccolò Veltri.

The master branch uses type-in-type instead of universe polymoprhism. The universe-polymoprhism branch uses universe polymoprhism.