Seerp Roald Koudenburg: Formalising size in formal category theory