Synthetic topos theory
[004X] Definition

Let \(U\) be a universe and let \(C\) be a category that has finite limits and \(U\)-small colimits. We say \(U\)-small colimits in \(C\) satisfy descent if, for any \(U\)-small category \(I\), any functors \(X,Y:{I}^{\triangleright }\rightarrow C\), and any natural transformation \(p:X\Rightarrow Y\), if \(Y\) is a colimit diagram and if the restriction of \(p\) to \(I\) is cartesian (that is, all naturality squares are pullbacks), then \(X\) is a colimit diagram if and only if \(p\) is cartesian.