A Personal Website

Paper with Thibaut Benjamin and Ioannis Markakis, to appear in MFPS 2024.

Two novel descrip­tions of weak omega-cat­e­gories have been recently pro­posed, using type-the­o­retic ideas. The first one is the depen­dent type the­ory CaTT whose mod­els are omega-cat­e­gories. The sec­ond is a recur­sive descrip­tion of a cat­e­gory of com­putads together with an adjunc­tion to glob­u­lar sets, such that the alge­bras for the induced monad are again omega-cat­e­gories. We com­pare the two descrip­tions by show­ing that there exits a fully faith­ful mor­phism of cat­e­gories with fam­i­lies from the syn­tac­tic cat­e­gory of CaTT to the oppo­site of the cat­e­gory of com­putads, which gives an equiv­a­lence on the sub­cat­e­gory of finite com­putads. We derive a more direct con­nec­tion between the cat­e­gory of mod­els of CaTT and the cat­e­gory of alge­bras for the monad on glob­u­lar sets, induced by the adjunc­tion with com­putads.

Paper with Nathan Corbyn, Lukas Heidemann, Nick Hu, Calin Tataru and Jamie Vicary, to appear in FSCD 2024.

We present the proof assis­tant homotopy.io for work­ing with finitely-pre­sented semi­strict higher cat­e­gories. The tool runs in the browser with a point-and-click inter­face, allow­ing direct manip­u­la­tion of proof objects via a graph­i­cal rep­re­sen­ta­tion. We describe the user inter­face and explain how the tool can be used in prac­tice. We also describe the essen­tial sub­sys­tems of the tool, includ­ing col­lapse, con­trac­tion, expan­sion, type­check­ing, and lay­out, as well as key imple­men­ta­tion details includ­ing data struc­ture encod­ing, mem­o­i­sa­tion, and ren­der­ing. These tech­ni­cal inno­va­tions have been essen­tial for achiev­ing good per­for­mance in a resource-con­strained set­ting.

Paper with Jamie Vicary, pub­lished in pro­ceed­ings of ACT 2023.

We now have a wide range of proof assis­tants avail­able for com­po­si­tional rea­son­ing in monoidal or higher cat­e­gories which are free on some gen­er­at­ing sig­na­ture. How­ever, none of these allow us to rep­re­sent cat­e­gor­i­cal oper­a­tions such as prod­ucts, equal­iz­ers, and sim­i­lar log­i­cal tech­niques. Here we show how the foun­da­tional math­e­mat­i­cal for­mal­ism of one such proof assis­tant can be gen­er­al­ized, replac­ing the con­ven­tional notion of string dia­gram as a geo­met­ri­cal entity liv­ing inside an n-cube with a pose­tal vari­ant that allows exotic branch­ing struc­ture. We show that these gen­er­al­ized dia­grams have richer behav­iour with respect to cat­e­gor­i­cal lim­its, and give an algo­rithm for com­put­ing lim­its in this set­ting, with a view towards future appli­ca­tion in proof assis­tants.

Preprint with Tobias Hartung and Karl Jansen, 2022.

Lat­tice field the­ory is a very pow­er­ful tool to study Feyn­man’s path inte­gral non-per­tur­ba­tively. How­ever, it usu­ally requires Euclid­ean back­ground met­rics to be well-defined. On the other hand, a recently devel­oped reg­u­lar­iza­tion scheme based on Fourier inte­gral oper­a­tor zeta-func­tions can treat Feyn­man’s path inte­gral non-per­tu­ba­tively in Lorentz­ian back­ground met­rics. In this arti­cle, we for­mally zeta-reg­u­lar­ize lat­tice the­o­ries with Lorentz­ian back­grounds and iden­tify con­di­tions for the Fourier inte­gral oper­a­tor zeta-func­tion reg­u­lar­iza­tion to be applic­a­ble. Fur­ther­more, we show that the clas­si­cal limit of the zeta-reg­u­lar­ized the­ory is inde­pen­dent of the reg­u­lar­iza­tion. Finally, we con­sider the har­monic oscil­la­tor as an explicit exam­ple. We dis­cuss mul­ti­ple options for the reg­u­lar­iza­tion and ana­lyt­i­cally show that they all repro­duce the cor­rect ground state energy on the lat­tice and in the con­tin­uum limit. Addi­tion­ally, we solve the har­monic oscil­la­tor on the lat­tice in Minkowski back­ground numer­i­cally.