Improving the Expressivity of Structural Type Theory
Abstract
Abstract Structural type theory is an extension of simple type theory that incorporates types for any kind of mathematical structure and allows isomorphic structures to be identified within them. In order to guarantee consistency, the system incorporates several syntactic restrictions. Modelling structural type theory in Tarski–Grothendieck set theory and extending the definition of transport functions, we show that some of these restrictions can be lifted, thus improving the expressive power of the system. In addition, we show how to treat axiomatic theories as first-class objects in our reformulation of structural type theory, and we state and prove within it a result analogous to the morphism theorem by Farmer.
Authors 1
-
Leiden University · University of Applied Sciences Leiden
Affiliation as printed
Leiden Institute of Advanced Computer Science (LIACS), Leiden University Einsteinweg 55, 2333 CC, Leiden, The Netherlands