I am a homotopy theorist, higher category theorist and homotopy type theorist, now a principal category theory scientist at Symbolica and previously a postdoc at the Centre of Australian Category Theory. My particular interests lie in domain specific type theories for synthetic (higher) mathematics and science e.g.:
synthetic (stable) homotopy theory;
probabilistic conformation-relevant molecular computing.
Speaking less like a mathematician and more like a philosopher I am interested in how internal-language/term-model relationships between:
some sort of category; and
some flavor of type theory;
give us, purely from the data of a category, a treatment of the objects of that category as if they were:
’sets with elements’; or
’spaces-as-ω-groupoids'; etc.
Indeed, I am interested in how, through these relationships, our abstract conception of the epistemology of a demonstrative science: termed type theories; endows objects with:
substance
directly from
structure.
I am interested in how and why we may work with mathematical entities by manipulating the stuff of knowing about them. My works aims to put these relationships to practical use in mathematics, computer science, and beyond.