That's true that categories are not going to find any special love there and that's sad. Much of the foundational tradition has been made in Set Theoretic langu

That's true that categories are not going to find any special love there and that's sad. Much of the foundational tradition has been made in Set Theoretic language and its value cannot be ignored (think say on Gödel on CH), but it's sad that there is such community divide forbidding any osmosis. Categorical thinking leads to natural costless abstractions with practical unifying power and transversal applicability, and while that's not a FOM, it's an indicative that there may be something there. Also by comparison, as user fmap said, there is much coding in Set Theory. Just look at an ordered pair. In set theory it is the Kuratowski pair, and that a violent encoding. It a hack. We're not nearer to answer what they really are by that. Categorically they are a limit, which perhaps it's also not metaphysical chant, but we can feel it however less hacky.