connectedness fibrationally

connectedness fibrationally

[Thomas Streicher]

Recently it has been discussed what is the appropriate notion of connecteness
for a category \X relative to a category \B. The following appears as natural
to me.

Let \B be a category and P : \X -> \B be a fibration of categories with
a terminal object and with internal sums.
Then for every object I in \B there is an obvious functor
\Delta_I : \B/I -> \X_I sending u : J -> I to \coprod_u 1_J.
An object X \in \X_I is an I_indexed family of connected objects iff
the functor \X_I(X,\Delta_I(-)) : (\B/I)^\op -> Set is represented by \id_I,
i.e there exists eta_X : X \to 1_I such that for every cocartesian arrow
\phi : 1_J -> \Delta_I(u) over u : J -> I and vertical arrow
\alpha : X -> \Delta_I(u) there exists a unique arrow s : I -> J
making the diagram

     X --------------------> 1_I
     |                        |
     | \alpha                 | 1_s
     |                        |
     V          cocart.       V
 \Delta_I(u) <---------------1_J

commute (where the top arrow is vertical).

In case I = 1 (where we write \Delta for \Delta_I) this means that for
every f : X -> Delta(I) there is a unique i : 1 -> I with
f = \Delta(i) \circ eta_X.

Notice that in case \B has finite limits, P is a fibration of categories
with finite limits and stable and disjoint sums the fibration P is equivalent
to \Delta^* P_{\X_1}. This is an old result of Moens (1982) (see section 15
of www.mathematik.tu-darmstadt.de/~streicher/FIBR/FibLec.pdf.gz for an
exposition).

Thomas