Chiara Sarti

A Personal Website

  • Chiara Sarti
  • They/Them
  • She/Her
  • PhD Stu­dent
  • Cat The­o­rist
  • Office FS20 CL
  • Email CS2197


I am a PhD stu­dent under the super­vi­sion of Prof. Jamie Vicary at the Com­puter Lab­o­ra­tory of the Uni­ver­sity of Cam­bridge. Within the depart­ment, I work as a mem­ber of the Cam­bridge Log­i­cal Struc­tures Hub (CLASH.)

My research inter­ests are focused around inter­nal lan­guages of higher struc­tures, such as higher dimen­sional cat­e­gories. These nor­mally take the form of depen­dent type the­o­ries, such as Homo­topy Type The­ory (HoTT) for groupoids, but I am also inter­ested in dia­gram­matic cal­culi.

I am cur­rently work­ing on com­par­i­son prob­lems between glob­u­lar weak omega-cat­e­gories and other mod­els of higher cat­e­gories, such as com­pli­cial sets. By using the type the­ory CaTT as a syn­tax for omega-cat­e­gories, these prob­lems can be stated in terms of build­ing tac­tics to algo­rith­mi­cally fill cer­tain fam­i­lies of types in CaTT, such as cones or cylid­ers.

When I am not think­ing about math, I am in peace­ful resis­tance against the British regime for its brazen crimes against human­ity. These range from killing hun­dreds of thou­sands of its most vul­ner­a­ble cit­i­zens through aus­ter­ity, to starv­ing mil­lions by drilling for new oil in the full knowl­edge this will destroy crops, to buy­ing weapons from Israel which are bat­tle-tested on tod­dlers.

For refus­ing to go along with this, I have been prosecuted under new dra­con­ian anti-protest leg­is­la­tion, once spend­ing 19 days in prison for march­ing down a road 20 min­utes, with­out even get­ting a trial.

As I am a polit­i­cal enemy of the car­bon regime, I expect to be impris­oned again sooner or later. Should this hap­pen, I can be reached by email­ing this address. Resis­tance can be finan­cially ruinous: every­one who sup­ports us chips-in to keep the lights on.

Research Projects

CaTT contexts are finite computads

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 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.

Posetal Diagrams

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.

Zeta-regularized Lattice Field Theory with Lorentzian background metrics

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.


I have given the fol­low­ing sci­en­tific talks:

  • Pose­tal dia­grams, ACT con­fer­ence, Mary­land (remote), August 3rd 2023,
  • Pose­tal dia­grams, YAM­CATS sem­i­nar, Leeds, June 19th 2023,
  • Pose­tal dia­grams, POO­DLE sem­i­nar, Oxford, June 8th 2023,
  • On some impos­si­ble prop­er­ties of the affine line object, Part III sem­i­nar, Cam­bridge, April 3rd 2022.