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.