data-category-0.7: Category theory