Definition Internal pseudocategory [efr-ZRUX]

Let \mathcal {C} be a 2-category with pullbacks. Then an internal pseudocategory in \mathcal {C} (or simply a pseudocategory in \mathcal {C}) consists of the following data:

  1. Two objects C_0, C_1 \in \mathcal {C}
  2. Morphisms d,c: C_1 \to C_0, e: C_0 \to C_1 so that de = ce = 1_{A_0}
    3. .
  3. A morphism m: C_1 \times _{C_0} C_1 \to C_1, so that dm = d\pi _2, cm = c\pi _1
  4. Isomorphism 2-cells \alpha : m(1_{C_1} \times _{C_0} m) \to m(m \times _{C_0} 1_{C_1}), \lambda : m \langle ec, 1_{C_1} \rangle \to 1_CA_1
    5. , and \rho : m\langle 1_{A_1}, ed \rangle \to 1_{A_1}
  5. Satisfying the following equations:
    1. d \circ \lambda = 1_d = d \circ \rho
    2. c \circ \lambda = 1_c = c \circ \rho
    3. d \circ \alpha = 1_{d\pi _3}, c \circ \alpha = 1_{c\pi _1}
    4. \lambda \circ e = \rho \circ e
  6. And so that the following diagrams commute:

A homomorphism or strict functor of pseudocategories A \to B is a pair of morphisms F_1: A_1 \to B_1, F_0: A_0 \to B_0 which commute with all the structure---that is, dF_1 = F_0d, F_1 \alpha = \alpha (F_1 \times _{F_0} F_1 \times _{F_0} F_1), and so on. There is a clear notion of natural transformation of homomorphisms. We write \mathsf {PsCat}_s(\mathbb {C}) for the 2-category of pseudocategories, homomorphisms and natural transformations in \mathbb {C}.