feat(category_theory/*): Representably flat functors (#9519)
Defined representably flat functors as functors `F : C тед D` such that `(X/F)` is cofiltered for each `X : C`.
- Proved that if `C` has all finite limits and `F` preserves them, then `F` is flat.
- Proved that flat functors preserves finite limits.
In particular, if `C` is finitely complete, then flat iff left exact.
- Proved that if `C, D` are small, then `F` flat implies `Lan F.op` preserves finite limits implies `F` preserves finite limits.
In particular, if `C` is finitely cocomplete, then flat iff `Lan F.op` is left exact.
Co-authored-by: erdOne <36414270+erdOne@users.noreply.github.com>
