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