Theory Presentation Combinators

12/14/2018

∙

by   Jacques Carette, et al.

∙

0

∙

share

To build a scalable library of mathematics, we need a method which takes advantage of the inherent structure of mathematical theories. Here we argue that theory presentation combinators are a helpful tool towards that quest. We motivate our choice of combinators, and give them precise semantics. We observe that the category of contexts plays a fundamental rôle (explicitly or otherwise) in all such developments, so we will examine its structure carefully. In particular, as it is a fibered category, cartesian liftings are pervasive. While our original work was based on experience and intuition, this work is firmly grounded in categorical semantics, and has resulted in a much cleaner and more powerful set of theory presentation combinators.