@[reducible, inline]

abbrev AlgebraicTopologyI.Category (obj : Type u_1) : Type (max u_1 (u_2 + 1))

Definition 3.1 (Category). A category, in the sense of Miller's Lectures on Algebraic Topology I. This is a thin wrapper around Mathlib's CategoryTheory.Category, repackaging it under the AlgebraicTopologyI namespace so that downstream files in this book can refer to it directly.