Internal category [efr-0036]

Let \mathcal {C} be a category. An internal category in \mathcal {C} consists of the following data:

1. Objects C_0, C_1 \in \mathcal {C}
2. Morphisms c,d: C_1 \to C_0 and i: C_0 \to C_1, and \circ : C_1 \times _0 C_1 \to C_1, where this is the pullback of c and d (which is in particular assumed to exist)
3. Such that

   write out the equations here

An internal functor consists of two maps C_0 \to D_0, C_1 \to D_1, such that the squares for each operation commutes (where the square involving \circ has one side formed by the map induced on the pullback)