Geometric morphisms?

Stream: Is there code for X?

[Fernando Chu]

Is there code for geometric morphisms? If not, I'm wondering if it would be alright to define them between arbitrary categories, so that $f^*$ is only required to preserve all finite limits that exist. This gives more flexibility at the cost of not being the "right" domain to consider.

[Joël Riou]

In mathlib, PreservesFiniteLimits means the preservation of finite limits which exist.

[Adrian Marti]

There also seems to be an API for preserving colimits (PreservesColimit?), so that the definition should be straightforward (defining a geometric morphism to be a finite-limit preserving and colimit preserving functor in the opposite direction). I think that the challenge is to prove the extension properties for functors (Diaconescu's theorem) for promoting flat functors on sites to geometric morphisms, which is how (in my experience) you construct geometric morphisms. (there are also other ways to promote functors on sites to geometric morphisms)