category_theory.discrete_category source