Thanks. Just what I needed. Well, maybe - it is a minor distraction perhaps from the real task - internal saturated anafunctors :)

]]>For one whose interests incline in that direction, it would be a nice exercise to work out those axioms by starting with the usual definition of a flat functor and interpreting it in the internal logic of the topos.

]]>Er, yes. What Toby said.

]]>From Elephant B2.6.1 (slightly shortened):

We begin by defining a number of objects associated with an internal category $C$.

- $P$, the object of pairs of morphisms with common codomain, is defined as the pullback $C_1 \times_{0,0} C_1$.
- $Q$, the object of pairs with common domain, is $C_1 \times_{1,1} C_1$.
- $R$, the object of parallel pairs, is the intersection of $P$ and $Q$, or equivalently the pullback $C_1 \times_{(0,1),(0,1)} C_1$.
- $S$, the object of commutative squares, is $C_2 \times_{1,1} C_2$.
- $T$, the object of diagrams of type $\bullet \overset{g}\underset{h}\rightrightarrows \bullet \overset{f}\rightarrow \bullet$ with $f g = f h$, is $C_2 \times_{(0,1),(0,1)} C_2$.

These are all defined with diagrams which I hope you can write down for yourself, perhaps by my subscript notation. The pulled back maps in these pullbacks are all given by lowercase letters that match the uppercase letter that names the pullback itself. For example, $p_1, p_2\colon P \to C_1$, $d_0 p_1 = d_0 p_2$, and $P$ is universal with this structure. The structure maps $C_1 \rightrightarrows C_0$ themselves are $d_0, d_1$ as usual.

From Elephant B2.6.2:

]]>An internal category $C$ in a regular category is

filteredif each of the three morphisms $C_0 \to 1$, $(d_1 p_1, d_1 p_2)\colon P \to C_0 \times C_0$, and $(d_2 t_1, d_2 t_2)\colon T \to R$ is a cover.Note: in this definition we have adopted the custom of naming morhpisms into a pullback by the names of the morphisms into the product of which the pullback is a subobject.

It did, but google books doesn’t give me any joy with either of Johnstone’s books, nor the handbook of categorical algebra.

Could you pretty please copy out the axioms?

]]>Cool, hope it helped.

]]>Thanks, Finn. I’ve accepted your answer.

]]>I’ve mumbled something in response over at MO.

]]>Cross-posted from MO. Feel free to put any answers there to pointy-licious goodness

I’m working out of *Sheaves in geometry and logic*, for reference.

There is a characterisation of flat functors $A:C \to Set$ as those such that the Grothendieck construction $\int_C A$ is a filtering category. There are more general versions of this result, in which $Set$ is replaced by a more general topos. One should also be able to characterise those discrete opfibrations that arise from flat functors (up to iso/equiv?). How about if we replace $C$ by an internal category, in a topos $E$ say? Then functors out of $C$ are replaced by discrete opfibrations over $C$ in $E$.

My question is this:

]]>What sort of thing should be considered as the analogue of a flat functor in the internal setting?