Fact-checked by Grok 2 weeks ago

Functor

In category theory, a functor is a structure-preserving mapping F: \mathcal{C} \to \mathcal{D} between categories \mathcal{C} and \mathcal{D}, consisting of a function on objects that assigns each object c in \mathcal{C} to an object F(c) in \mathcal{D}, and a function on morphisms that assigns each morphism f: c \to c' in \mathcal{C} to a morphism F(f): F(c) \to F(c') in \mathcal{D}, while preserving the domains and codomains of morphisms. This mapping must satisfy two axioms: it preserves identity morphisms, so F(\mathrm{id}_c) = \mathrm{id}_{F(c)} for every object c in \mathcal{C}, and it preserves composition of morphisms, so F(g \circ f) = F(g) \circ F(f) for any composable morphisms f: c \to c' and g: c' \to c'' in \mathcal{C}. These properties ensure that functors translate the relational structure of one category into another without distortion. The concept of a functor was introduced by and in their 1945 paper "General Theory of Natural Equivalences," where it emerged as a tool to formalize relationships between constructions, such as and theories. Functors generalize homomorphisms between algebraic structures, extending the idea to entire categories, and they come in covariant and contravariant variants: covariant functors preserve the direction of morphisms, while contravariant functors reverse it by mapping f: c \to c' to F(f): F(c') \to F(c), with adjusted preservation axioms. They form the arrows in the category Cat of (small) categories, where objects are categories and morphisms are functors, enabling the study of categorical hierarchies and equivalences. Functors are foundational to category theory's applications across mathematics and , underpinning concepts like natural transformations—which are morphisms between functors that commute with their actions on objects and morphisms—and adjunctions, pairs of functors that represent universal approximations between categories. Notable examples include the from groups to sets, which discards the group operation while preserving the underlying set structure, and the Hom functor, which assigns to objects the sets of morphisms between them, revealing representable structures via the . In , functors model type constructors in languages like , facilitating modular and composable code through operations like mapping and composition.

Definition and Basics

Formal Definition

In , a functor F: \mathcal{C} \to \mathcal{D} from a \mathcal{C} (the category) to a \mathcal{D} (the category) consists of two mappings: one that sends each object A of \mathcal{C} to an object F(A) of \mathcal{D}, and one that sends each f: A \to B in \mathcal{C} to a F(f): F(A) \to F(B) in \mathcal{D}. This structure ensures that the mapping respects the categorical composition and identities. Specifically, functors preserve identity morphisms, meaning that for every object A in \mathcal{C}, F(\mathrm{id}_A) = \mathrm{id}_{F(A)}. They also preserve composition of morphisms: if f: A \to B and g: B \to C are morphisms in \mathcal{C}, then F(g \circ f) = F(g) \circ F(f). Functors are commonly notated with F(-) to indicate the action on objects and simply F applied to arrows for morphisms. The concept was introduced by and in their 1945 paper "General Theory of Natural Equivalences," establishing the foundational framework for mappings between categories in .

Covariant and Contravariant Functors

In , a covariant functor F: \mathcal{C} \to \mathcal{D} between categories \mathcal{C} and \mathcal{D} acts on s by preserving their direction: it maps a f: A \to B in \mathcal{C} to a F(f): F(A) \to F(B) in \mathcal{D}. This preserves the order of , so that F(g \circ f) = F(g) \circ F(f) for composable s f and g in \mathcal{C}. A contravariant functor, by contrast, reverses the direction of morphisms: it maps f: A \to B to F(f): F(B) \to F(A). Formally, a contravariant functor from \mathcal{C} to \mathcal{D} is equivalent to a covariant functor from \mathcal{C} to the opposite category \mathcal{D}^{\mathrm{op}}, or equivalently from \mathcal{C}^{\mathrm{op}} to \mathcal{D}. Consequently, its action on composition reverses the order: F(g \circ f) = F(f) \circ F(g). An illustrative example of a naturally contravariant functor arises in linear algebra, where the dual space construction sends a vector space V over a field K to its dual V^*, the space of linear functionals V \to K. For a linear map T: W \to V, it induces the dual map T^*: V^* \to W^* defined by T^*(f) = f \circ T for f \in V^*, thereby reversing the morphism direction.

Properties

Preservation and Naturality

A functor F: \mathcal{C} \to \mathcal{D} between categories \mathcal{C} and \mathcal{D} must preserve the morphisms and the of morphisms as part of its defining axioms. Specifically, for every object A in \mathcal{C}, F(\mathrm{id}_A) = \mathrm{id}_{F(A)} in \mathcal{D}, and for any composable morphisms f: A \to B and g: B \to C in \mathcal{C}, F(g \circ f) = F(g) \circ F(f) in \mathcal{D}. These preservation requirements ensure that F maintains the structural relations of \mathcal{C} within \mathcal{D}, enabling the formation of concepts such as faithful functors, where F is injective on hom-sets, and full functors, where F is surjective on hom-sets, though these are stronger properties beyond the basic axioms. Natural transformations provide a way to compare parallel functors F, G: \mathcal{C} \to \mathcal{D} by serving as s in the . A natural transformation \eta: F \Rightarrow G consists of a family of s \eta_A: F(A) \to G(A) in \mathcal{D}, one for each object A in \mathcal{C}, satisfying the naturality condition: for every f: A \to B in \mathcal{C}, \begin{CD} F(A) @>{\eta_A}>> G(A) \\ @V{F(f)}VV @VV{G(f)}V \\ F(B) @>>{\eta_B}> G(B) \end{CD} this square commutes, meaning G(f) \circ \eta_A = \eta_B \circ F(f). The commutative property of the naturality square guarantees that \eta respects the action of morphisms across the functors, preserving their relational structure. If each component \eta_A is an isomorphism in \mathcal{D}, then \eta is a natural isomorphism, denoted F \cong G, indicating that F and G are equivalent up to canonical isomorphism. Two functors are equivalent if there exists a natural isomorphism between them, capturing an essential similarity in how they map the structure of \mathcal{C} to \mathcal{D}.

Functor Categories

In , the , often denoted [ \mathcal{C}, \mathcal{D} ] or \mathcal{D}^\mathcal{C}, is defined such that its objects are all functors F: \mathcal{C} \to \mathcal{D}, and its morphisms are between these functors. This construction organizes the functors from one category to another into a of their own, where the morphism on a functor F is the \mathrm{id}_F, satisfying (\mathrm{id}_F)_X = \mathrm{id}_{F(X)} for each object X in \mathcal{C}. The in the [ \mathcal{C}, \mathcal{D} ] is induced by the vertical of natural transformations: given natural transformations \eta: F \Rightarrow G and \theta: G \Rightarrow H between functors F, G, H: \mathcal{C} \to \mathcal{D}, their composite \theta \circ \eta is the natural transformation whose component at each object X \in \mathcal{C} is (\theta \circ \eta)_X = \theta_X \circ \eta_X. Furthermore, the of functors between categories induces a corresponding on functor categories; specifically, for functors F: \mathcal{C} \to \mathcal{D} and G: \mathcal{D} \to \mathcal{E}, the composite functor G \circ F: \mathcal{C} \to \mathcal{E} serves as an object in [ \mathcal{C}, \mathcal{E} ], and this operation aligns with the categorical when considering functors between functor categories themselves. Examples of small functor categories include \mathbf{Set}^{\mathbf{B}}, the category whose objects are functors from the category of finite sets and bijections (often denoted B or core(FinSet)) to the category of sets (Set), with natural transformations as morphisms; such functors correspond to combinatorial structures that assign sets to finite sets in a way preserving the category's operations. This category is particularly useful in , as its objects can model of structures on finite sets. Key properties of functor categories include their size and local smallness: if both \mathcal{C} and \mathcal{D} are small categories, then [ \mathcal{C}, \mathcal{D} ] is itself small. More generally, if \mathcal{C} is small and \mathcal{D} is locally small, then [ \mathcal{C}, \mathcal{D} ] is locally small, meaning the hom-sets between any two objects are small sets. Regarding variance, the functor category construction exhibits contravariance in the domain category \mathcal{C}; for instance, a functor K: \mathcal{C}' \to \mathcal{C} induces a precomposition functor [ \mathcal{C}, \mathcal{D} ] \to [ \mathcal{C}', \mathcal{D} ] given by F \mapsto F \circ K, while it is covariant in the codomain \mathcal{D}, as a functor L: \mathcal{D} \to \mathcal{E} induces postcomposition F \mapsto L \circ F: [ \mathcal{C}, \mathcal{D} ] \to [ \mathcal{C}, \mathcal{E} ]. For contravariant functors from \mathcal{C} to \mathcal{D}, the appropriate category is [ \mathcal{C}^{\mathrm{op}}, \mathcal{D} ], reflecting the opposite category in the indexing.

Variants

Opposite Functors

The opposite category C^{\mathrm{op}} of a given category C is constructed by retaining the same collection of objects as C, while formally reversing the direction of all morphisms. Specifically, for every morphism f: A \to B in C, there exists a corresponding morphism denoted f^{\mathrm{op}}: B \to A in C^{\mathrm{op}}. The identity morphism \mathrm{id}_A in C becomes \mathrm{id}_A^{\mathrm{op}} in C^{\mathrm{op}}, and composition is defined such that if f: A \to B and g: B \to C are morphisms in C, then f^{\mathrm{op}} \circ g^{\mathrm{op}} = (g \circ f)^{\mathrm{op}} in C^{\mathrm{op}}. This construction ensures that C^{\mathrm{op}} is indeed a category, with the reversal providing a dual perspective on the structure of C. A contravariant functor from a category C to a category D is equivalent to a covariant functor from the opposite category C^{\mathrm{op}} to D, or alternatively, from C to the opposite category D^{\mathrm{op}}. This equivalence arises because the morphism-reversing action of a contravariant functor aligns precisely with the structure of the opposite category, allowing all functors to be understood in covariant terms when one domain or is oppified. As introduced in the discussion of covariant and contravariant functors, this perspective unifies the treatment of variance in . Given a functor F: C \to D, its opposite functor F^{\mathrm{op}}: C^{\mathrm{op}} \to D^{\mathrm{op}} is induced by applying the oppification to both domain and codomain categories. On objects, F^{\mathrm{op}} acts identically to F, so F^{\mathrm{op}}(A) = F(A) for any object A in C^{\mathrm{op}}. On morphisms, it maps f^{\mathrm{op}}: B \to A in C^{\mathrm{op}} (corresponding to f: A \to B in C) to F(f)^{\mathrm{op}}: F(B) \to F(A) in D^{\mathrm{op}}. This mapping rule ensures that F^{\mathrm{op}} is a well-defined functor. The functor F^{\mathrm{op}} inherits preservation properties from F, but adapted to the reversed structures. Since F preserves identities, F(\mathrm{id}_A) = \mathrm{id}_{F(A)}, it follows that F^{\mathrm{op}}(\mathrm{id}_A^{\mathrm{op}}) = F(\mathrm{id}_A)^{\mathrm{op}} = \mathrm{id}_{F(A)}^{\mathrm{op}}, which is the identity morphism in D^{\mathrm{op}}. For , if f^{\mathrm{op}}: B \to A and g^{\mathrm{op}}: C \to B in C^{\mathrm{op}} (corresponding to f: A \to B and g: B \to C in C), then F^{\mathrm{op}}(f^{\mathrm{op}} \circ g^{\mathrm{op}}) = F^{\mathrm{op}}((g \circ f)^{\mathrm{op}}) = F(g \circ f)^{\mathrm{op}} = F(f)^{\mathrm{op}} \circ F(g)^{\mathrm{op}} = F^{\mathrm{op}}(f^{\mathrm{op}}) \circ F^{\mathrm{op}}(g^{\mathrm{op}}), thus preserving in the opposite sense. These properties confirm that oppification is a on the of categories.

Multifunctors and Profunctors

A multifunctor generalizes the concept of a functor to multiple input categories, allowing mappings from products of categories to a target category. In particular, a bifunctor, or binary functor, is a functor F: \mathcal{C} \times \mathcal{D} \to \mathcal{E} between categories \mathcal{C}, \mathcal{D}, and \mathcal{E}. It maps a pair of objects (A, B) with A \in \mathrm{Ob}(\mathcal{C}) and B \in \mathrm{Ob}(\mathcal{D}) to an object F(A, B) \in \mathrm{Ob}(\mathcal{E}). On morphisms, it sends a pair (f: A \to A', g: B \to B') to a morphism F(f, g): F(A, B) \to F(A', B') in \mathcal{E}, while preserving identities and composition in each variable separately: F(\mathrm{id}_A, \mathrm{id}_B) = \mathrm{id}_{F(A,B)} and F(f_1 \circ f_2, g) = F(f_1, g) \circ F(f_2, g), with analogous preservation for the second variable. Bifunctors can exhibit mixed variance by incorporating opposite categories. For instance, a bifunctor F: \mathcal{C}^{\mathrm{op}} \times \mathcal{D} \to \mathcal{E} is contravariant in the first argument and covariant in the second: it reverses arrows in \mathcal{C} via F(f^{\mathrm{op}}, g) = F(f, g)^{\mathrm{op}} (adjusted for the target), while acting covariantly on \mathcal{D}. This flexibility extends to higher arities, though bifunctors form the primary case for two variables. Such constructions underpin functor categories for multi-arity mappings, where natural transformations respect the product structure. A profunctor, also known as a , is a specific type of bifunctor P: \mathcal{C}^{\mathrm{op}} \times \mathcal{D} \to \mathrm{Set}, contravariant in \mathcal{C} and covariant in \mathcal{D}, generalizing relations between categories beyond ordinary functors. It assigns to each pair (C, D) a set P(C, D), with action on morphisms (f^{\mathrm{op}}, g) inducing a P(f^{\mathrm{op}}, g): P(C', D) \to P(C, D') via pre- and post-composition, preserving the categorical axioms. Profunctors encompass functors, as a functor F: \mathcal{C} \to \mathcal{D} yields the representable profunctor \mathcal{D}(-, F(-)): \mathcal{C}^{\mathrm{op}} \times \mathcal{D} \to \mathrm{Set}. They form the morphisms in the bicategory \mathbf{Prof} of small categories, profunctors, and transformations. A canonical example of a profunctor is the hom-bifunctor \mathrm{Hom}_{\mathcal{C}}(-, -): \mathcal{C}^{\mathrm{op}} \times \mathcal{C} \to \mathrm{Set} in a locally small \mathcal{C}, which sends (A, B) to the hom-set \mathrm{Hom}_{\mathcal{C}}(A, B) of morphisms from A to B. On morphisms, it acts by (f^{\mathrm{op}}, g) \mapsto (q \mapsto g \circ q \circ f) for q: A \to B, thus contravariantly in the domain and covariantly in the . This bifunctor underlies the Yoneda embedding and relational structures in .

Examples

Algebraic Examples

In category theory, a prominent example of a functor arising from algebraic structures is the forgetful functor U: \mathbf{Grp} \to \mathbf{Set}, which maps each group to its underlying set and each group homomorphism to the corresponding function between those sets, thereby disregarding the group operation and identity. This functor is faithful but neither full nor essentially surjective, as it preserves the set-theoretic structure while omitting algebraic details. The F: \mathbf{Set} \to \mathbf{Grp}, which assigns to each set the generated by that set and to each function the induced , is left to the U, forming a free-forgetful adjunction that exemplifies how algebraic structures can be freely generated from sets. This adjunction highlights the universal property of in preserving colimits from the . Another algebraic example is the functor P: \mathbf{Set} \to \mathbf{Set}, defined by sending each set X to its power set \mathcal{P}(X), the collection of all subsets of X, and each function f: X \to Y to the direct image function P(f): \mathcal{P}(X) \to \mathcal{P}(Y) given by P(f)(S) = \{ f(s) \mid s \in S \} for S \subseteq X. This covariant functor preserves unions and is monotonic, reflecting the lattice structure inherent in subsets. For a fixed object A in a \mathbf{C}, the hom-functor \mathrm{Hom}(A, -): \mathbf{C} \to \mathbf{Set} maps each object B to the set \mathrm{Hom}(A, B) of from A to B, and each g: B \to C to the post-composition map \mathrm{Hom}(A, g): \mathrm{Hom}(A, B) \to \mathrm{Hom}(A, C) defined by h \mapsto g \circ h. This covariant representable functor embodies the Yoneda lemma's principle that objects are determined by their , providing a way to probe structure.

Topological and Geometric Examples

In topology, the fundamental group functor provides an algebraic invariant capturing the 1-dimensional holes in spaces. It is defined on the category \mathbf{Top}_* of pointed topological spaces, where objects are pairs (X, x_0) with X a topological space and x_0 \in X a basepoint, and morphisms are continuous maps preserving basepoints. The functor \pi_1: \mathbf{Top}_* \to \mathbf{Grp} assigns to each (X, x_0) the fundamental group \pi_1(X, x_0), consisting of homotopy classes of based loops at x_0 under concatenation, forming a group. For a basepoint-preserving continuous map f: (X, x_0) \to (Y, y_0), \pi_1(f) induces the group homomorphism sending a loop class [\gamma] to [f \circ \gamma]. This construction preserves the category structure, as composition of maps induces composition of homomorphisms and identity maps induce identity homomorphisms. Singular homology functors extend this idea to higher dimensions, assigning abelian groups that detect holes of various orders. For each integer n \geq 0, the functor H_n: \mathbf{Top} \to \mathbf{Ab} maps a topological space X to the nth singular homology group H_n(X), generated by formal integer linear combinations of continuous maps \sigma: \Delta^n \to X (singular n-simplices), modulo boundaries from the chain complex with alternating-sum boundary operators. Continuous maps f: X \to Y induce chain maps f_\#: C_n(X) \to C_n(Y) by postcomposition f_\#(\sigma) = f \circ \sigma, which descend to homomorphisms H_n(f): H_n(X) \to H_n(Y) on homology. These functors satisfy homotopy invariance: if f \simeq g via a homotopy, then H_n(f) = H_n(g), and they form a sequence of covariant functors preserving exact sequences and direct sums. The arises in the study of sheaves over topological spaces, pushing forward structure along continuous s. For a continuous f: X \to Y between topological spaces, the f_*: \mathbf{Sh}(X) \to \mathbf{Sh}(Y) acts on the of sheaves of sets (or abelian groups) on X and Y. It assigns to a sheaf \mathcal{F} on X the sheaf f_* \mathcal{F} on Y, where for an V \subseteq Y, the sections are (f_* \mathcal{F})(V) = \mathcal{F}(f^{-1}(V)), with restriction maps induced by those of \mathcal{F}. Morphisms of sheaves \phi: \mathcal{F} \to \mathcal{G} on X map to f_* \phi: f_* \mathcal{F} \to f_* \mathcal{G} by precomposition with f^{-1}. This functor is right to the f^{-1}: \mathbf{Sh}(Y) \to \mathbf{Sh}(X) and preserves limits, reflecting how local data on X becomes global on Y via f. In the slice context, for subspaces over X and Y, it similarly pushes forward bundles or sheaves. The global sections functor extracts overall data from sheaves on a space. For a topological space X, the functor \Gamma: \mathbf{Sh}(X) \to \mathbf{Set} (or to \mathbf{Ab} for abelian sheaves) assigns to a sheaf \mathcal{F} on X its group of global sections \Gamma(X, \mathcal{F}), the set of sections over the entire space X compatible with the sheaf axiom. A morphism \phi: \mathcal{F} \to \mathcal{G} of sheaves induces \Gamma(\phi): \Gamma(X, \mathcal{F}) \to \Gamma(X, \mathcal{G}) by applying the sheaf map \phi_X: \mathcal{F}(X) \to \mathcal{G}(X) to sections. This is covariant, and it is left exact but not necessarily exact, with higher derived functors yielding sheaf cohomology groups that measure obstructions to global extendability of local sections.

Relations to Other Concepts

Adjunctions and Limits

An adjunction consists of a pair of functors F: \mathcal{C} \to \mathcal{D} and G: \mathcal{D} \to \mathcal{C}, together with a natural between hom-sets \hom_{\mathcal{D}}(F(A), B) \cong \hom_{\mathcal{C}}(A, G(B)) for all objects A in \mathcal{C} and B in \mathcal{D}. This bijection is induced by unit and counit natural transformations: the unit \eta: \id_{\mathcal{C}} \to G F and the counit \varepsilon: F G \to \id_{\mathcal{D}}, which satisfy the triangle identities ensuring the compositions align appropriately. These components make the adjunction a universal property capturing a duality between the functors, often arising in contexts where one functor "freely generates" structures that the other "forgets," such as the functor being left adjoint to the from groups to sets. In an adjunction F \dashv G, the functor F is called the left adjoint to G, denoted F \dashv G, while G is the right adjoint. Left adjoint functors preserve all colimits, meaning that if a colimit diagram in \mathcal{C} exists, then F applied to it yields a colimit in \mathcal{D}. Conversely, right adjoint functors preserve all limits: if a limit diagram in \mathcal{D} exists, then G applied to it forms a in \mathcal{C}. These preservation properties follow from the hom-set isomorphism and the universal nature of and colimits, often verified using the Yoneda lemma to relate the adjunction to representable functors. Kan extensions provide a universal mechanism for extending a functor along another functor, embodying an adjoint relationship. Specifically, given functors F: \mathcal{C} \to \mathcal{E} and p: \mathcal{C} \to \mathcal{B}, the left Kan extension \Lan_p F: \mathcal{B} \to \mathcal{E} is a functor equipped with a \eta: F \to (\Lan_p F) \circ p that is universal: for any other functor K: \mathcal{B} \to \mathcal{E} with a \theta: F \to K \circ p, there exists a unique \overline{\theta}: \Lan_p F \to K such that \theta = \overline{\theta} \circ \eta. The right Kan extension \Ran_p F is defined dually, serving as a right to the precomposition functor p^*: [\mathcal{B}, \mathcal{E}] \to [\mathcal{C}, \mathcal{E}]. This construction generalizes many universal properties in , where the Kan extension acts as the "most efficient" extension of F along p.

Monads and Universal Constructions

In category theory, every adjunction induces a monad. Specifically, given an adjunction F \dashv G with F: \mathcal{C} \to \mathcal{D} the left adjoint and G: \mathcal{D} \to \mathcal{C} the right adjoint, the composite endofunctor T = G \circ F: \mathcal{C} \to \mathcal{C} on the domain category \mathcal{C} carries the structure of a monad, where the unit natural transformation \eta: \mathrm{id}_\mathcal{C} \to T is the unit of the adjunction and the multiplication natural transformation \mu: T^2 \to T is given by \mu = G \varepsilon F, with \varepsilon: F \circ G \to \mathrm{id}_\mathcal{D} the counit of the adjunction. These components satisfy the monad axioms: associativity \mu \circ T\mu = \mu \circ \mu T and unit laws \mu \circ T\eta = \mu \circ \eta T = \mathrm{id}_T. This construction generalizes algebraic structures, such as the monad on the category of sets induced by the free group adjunction, where T sends a set to the underlying set of its free group. A functor U: \mathcal{E} \to \mathcal{C} is tripleable if it admits a left F such that the induced T = U \circ F on \mathcal{C} yields an Eilenberg-Moore category \mathcal{C}_T (the category of T-algebras) equivalent to \mathcal{E} via the comparison functor \Phi: \mathcal{E} \to \mathcal{C}_T. Tripleable functors are precisely those equivalent to from categories of algebras over a , capturing universal algebraic theories categorically. For instance, the from groups to sets is tripleable, as its left (the functor) generates the whose algebras are groups. Functors play a central role in the universal properties of free constructions, often preserving or reflecting . The free functor F in an adjunction F \dashv U typically creates free objects that are initial in comma categories, such as the free group on a set X being initial among groups equipped with maps from X. This universality ensures that F preserves colimits, including initial objects, providing a categorical foundation for free generations in . Similarly, representable functors associated with free objects, like the underlying-set functor represented by the on one generator, embody these properties through natural isomorphisms. Beck's monadicity theorem provides precise conditions for a functor to be monadic, meaning it is tripleable and thus equivalent to the from a of algebras. Specifically, a functor U: \mathcal{B} \to \mathcal{C} with left adjoint F is monadic if U reflects isomorphisms and \mathcal{B} has coequalizers of reflexive U-split pairs that are preserved by U. This , originally formulated in the context of , characterizes when arise as algebraic theories over a , with applications in such as recognizing varieties of algebras via forgetful functors. The conditions ensure the comparison functor to the Eilenberg-Moore is an equivalence, generalizing Birkhoff's variety categorically.

Implementations

In Programming Languages

In languages, particularly those influenced by such as , a functor is implemented as a F that supports a polymorphic fmap of type (a -> b) -> F a -> F b, allowing the application of a from type a to b over the structure F a to produce (F bwithout altering the structure itself.[](https://hackage.haskell.org/package/base/docs/Data-Functor.html) Thisfmapoperation must satisfy two laws to ensure functoriality: the identity law, wherefmap id == id, meaning applying the [identity function](/page/Identity_function) leaves the functor unchanged; and the composition law, where fmap (f . g) == fmap f . fmap g`, preserving within the functor. These laws guarantee that the mapping behaves consistently, akin to how functions compose in the category of types. The Functor typeclass directly embodies the notion of a covariant endofunctor on the Hask, where objects are types and morphisms are , providing a computational of categorical functors by lifting morphisms through the in the same . For instance, the List type serves as a example of a functor, where fmap corresponds to the that applies a to each element of a list, such as fmap (+1) [1,2,3] yielding [2,3,4], thereby transforming List Int to List Int while maintaining the list structure. Similarly, the Maybe type, which represents optional values as Just a or Nothing, implements fmap by applying the function only if the value is present, as in fmap sqrt (Just 4) returning Just 2.0, or Nothing otherwise, enabling safe computation over potentially absent data. In languages like , which support explicit variance s on type parameters, functors can be declared as covariant or contravariant to control relationships. A covariant functor uses the + , such as trait CovariantFunctor[+A], allowing subtypes to flow in the same direction as the type parameter, which aligns with the -like operations in functional libraries like . Conversely, a contravariant functor employs the - , like trait ContravariantFunctor[-A], where reverses direction, useful for structures that consume values of the parameterized type, such as comparators or input processors, enabling more flexible type-safe compositions in polymorphic code.

In Proof Assistants

In proof assistants, functors from are formalized as structured mappings between categories that preserve identities and composition, enabling the verification of categorical properties and constructions within dependently typed or systems. These formalizations typically build on foundational libraries for precategories or categories, addressing challenges such as proof relevance, univalence, and the handling of large or infinite categories. Seminal efforts include the UniMath library in , the agda-categories library in Agda, and the mathlib library in , each providing definitions and theorems that support advanced applications like Yoneda embeddings and adjunctions. In the proof assistant, the UniMath library formalizes functors within its univalent foundations, defining a functor F : C \to D between precategories C and D as a pair of functions—on objects and morphisms—that respects identities and , with natural transformations treated as morphisms between functors. Key properties include fully faithful functors, which preserve isomorphisms, and the Yoneda embedding, proven to be fully faithful as a functor from a to its presheaf . The library also covers functor categories, where functors form objects and natural transformations form morphisms, ensuring the structure is itself a when the target is. This formalization leverages univalence to equate isomorphic categories definitionally, facilitating proofs in , though it requires careful management of truncation levels for set-like structures. Agda's categories library defines functors in the module Categories.Functor.[Core](/page/Core), representing a functor between categories \mathcal{C} and \mathcal{D} as a with fields for object and morphism mappings, plus axioms for preserving identities (F.id) and (F._∘_). It includes constructions like constant functors and diagonal functors, as well as properties such as and fullness, with support for proof-relevant to handle equivalences via natural isomorphisms. Notably, the library formalizes duality and opposite categories, allowing functors to be definitionally equal to their opposites under certain conditions, and extends to 2-categories with 2-functors. This approach highlights Agda's strengths in dependent types for encoding categorical variance and , enabling formalizations of advanced like monoidal functors without extensionality assumptions. In , mathlib's submodule defines Functor C D as a bundled extending C ⥤ D, with components obj for objects and map for morphisms, enforced by axioms map_id and map_comp to ensure functoriality. is denoted by ⋙, and the functor by 𝟭; applications use F.obj X for objects and F.map f for morphisms. The proves essential results like the and preservation of limits by certain functors, integrating seamlessly with Lean's typeclass system for instances like the category of types. It supports large categories via universe polymorphism and has been used to formalize schemes via the functor-of-points approach, demonstrating scalability for . Challenges in Lean include inference for complex functor compositions, addressed through tactics and attributes. Across these systems, formalizing functors reveals tensions between strict and weak equalities, with Agda and UniMath emphasizing proof-irrelevance for setoids while prioritizes computational content. Common theorems include the composition of functors forming a and the naturality of transformations, underpinning formal proofs of adjunctions and monads in .