Taking "Taking Categories Seriously" Seriously

The Curry-Howard-Lambek correspondence posits that proofs, programs, and morphisms in a category are the same thing. Although many programming languages are based on categorical models, none so far allow the user to program directly with categories as primitive data structures. This talk will chronicle my efforts at GLAiVe to create a programming language based on the formal theory of categories. At GLAiVe we do pure category theory as well as Idris2 programming and hope to meet somewhere in the middle. On the programming side of things, I will explain how Lawvere's perspective on universal algebra gives a way to evaluate and translate domain-specific languages. On the pure maths side, I will explain a generalization of the Grothendieck construction and how it relates to compositional computation.