@MartinEscardo this is a definition of categories as monads in the bicategory of spans using some specific choice of construction of pullback in Set, but it is naturally a weak 2-category - so we should state it for pullbacks, but then we can’t even state the associativity law as it is a naturally a dependent equality (unless we use some kind of unbiased pullbacks)