Theory Presentation Combinators Conference Paper uri icon

  •  
  • Overview
  •  
  • Research
  •  
  • Identity
  •  
  • Additional Document Info
  •  
  • View All
  •  

abstract

  • 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\^{o}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.

publication date

  • 2012