Digital Twins are of universal interest in design and engineering. These are all developed either within a given software package or patched together at great cost. There is no coherent framework and little transparency. Several developments in applied category theory make it possible to define a digital twin entirely in category theoretic terms. A categorical digital twin is defined by its mathematics and is therefore transparent and independent of any particular software package. We define a digital twin as an enriched category over a familiar wiring diagram of a process and proceed to analyze it using functors and profunctors among enriched categories. The availability of packages for programming with categories in dependently typed languages such as Agda makes it possible to implement and execute these digital twins within a categorical framework. We work in the realm of symmetrical monoid categories and semi-rings. Being able to describe very different aspects of a digital twin, including some that don’t appear particularly mathematical, using these ubiquitous structures provides tremendous reusability. Our goal in this talk is to introduce our Agda implementation of categorical digital twins with particular emphasis on programming with categories and the power that dependent languages bring to the task. These are techniques that generalize beyond our particular domain and should be translatable to other dependent languages as well. We will introduce the necessary mathematics, but monoids and semi-rings are ubiquitous and attendees will be immediately familiar. Enriched categories may be a new construct but should be readily understandable to attendees with an introductory understanding of category theory.