Dilatations of categories, via their lean formalization

Arnaud Mayeux

Given a category $\calC$ and a center, that is a collection of pairs $(d_i,N_i)$ consisting of a morphism $d_i$ and a sieve $N_i$ over its codomain, the dilatation of $\calC$ is a…