Speaker:

   Felix Dilke (SpringerNature)

Title

   Bewl, a Scala DSL for topos theory

Abstract

   A topos can be viewed as a category with all the extras, and has a
   very rich structure that includes an "internal language" as defined
   by Mitchell and Benabou, which includes most of the apparatus of
   conventional first-order model theory and logic. My motivation was
   to develop this into a software equivalent, a programmatic DSL
   (domain-specific language) which facilitates exploring topoi and
   doing topos-theoretic calculations.

   In this talk, I'll briefly recap how topos theory offers an
   alternative foundation for mathematics, describe some of the
   motivations for the project, and summarize its history so far,
   detailing some of the interesting technical and conceptual
   obstacles I encountered.

   Large blocks of textbook topos theory can now be encoded as library
   modules in Bewl. The DSL also includes facilities for defining and
   manipulating algebraic structures such as rings, groups and
   modules, together with a library for topos equivalents of standard
   algebraic constructions. There are also many utilities and helper
   functions to tell, for example, if an arrow is epic or if an object
   in a topos is injective, and to construct coproducts.

   The Bewl codebase [1] is now adequate for doing simple calculations
   in topoi, but is of course limited to topoi which can be modelled
   in software. It's still useful as a way to explore category theory,
   to understand the topos-theoretic viewpoint, and may also be of
   interest to those studying semigroups and monoids. There are also
   potential applications to music theory. Another offshoot has been a
   pure math (as opposed to software) construction for injective hulls
   in a locally finite topos [2].

   [1] https://github.com/fdilke/bewl

   [2] https://arxiv.org/abs/1802.00960