@[reducible, inline]
abbrev
AlgebraicTopologyI.Functor
(C : Type u_1)
[CategoryTheory.Category.{u_2, u_1} C]
(D : Type u_3)
[CategoryTheory.Category.{u_4, u_3} D]
:
Type (max u_2 u_4 u_1 u_3)
Definition 3.4 (Functor). A functor F : C тед D between two
categories, in the sense of Miller's Lectures on Algebraic Topology I.
This is a thin wrapper around Mathlib's CategoryTheory.Functor, repackaging
it under the AlgebraicTopologyI namespace so that downstream files in this
book can refer to it directly.