We're a research group based in the UK focusing on applying category theory to AI. Our tools are dependently typed theories, theorem provers, and whiteboards.