Projects

I fixed a few mistakes in the materials for The Great Elf Game, and re-uploaded it to tes.

I proved some things about bundles internal to a category equipped with a class of étale maps, and about natural bundles; I was unable to prove some other things. I tried to formalise 'natural sheaves' which should be appropriately-natural ways of selecting an object of every Grothendieck topos.

I started out thinking about Lascar groups of first-order theories. I ended up thinking about linear logics for enriched categories. slides

I implemented a very small dependently-typed programming language that compiles to machine code via LLVM IR. So now I know about bidirectional type-checking, and how to write a compiler targeting LLVM IR.

I made a website where people could play The Great Pirate Game remotely during the lockdown.

Do you love 2012 Adele song Skyfall from 2012 James Bond film Skyfall? Think it could do with a few more notes? Don't worry: I've added some.

I did an EPQ about shapes. The premise was to represent shapes as multivector-valued distributions. I proved a fundamental theorem of calculus for these.