[[!redirects functors]] #Contents# * table of contents {:toc} ## Idea ## The concept if _[[nLab:functor]]_ is the evident concept of [[nLab:homomorphisms]] between [[nLab:categories]]. ## Definition ## {#Definition} Let $A$ and $B$ be [[precategories]]. Informally, a **functor** $F : A \to B$ consists of * A function $F_0 : A_0 \to B_0$ * For each $a,b:A$, a function $F_{a,b}:hom_A(a,b) \to hom_B(F a,F b)$, generally also denoted $F$. * For each $a:A$, we have $F(1_a)=1_{F a}$. * For each $a,b,c: A$ and $f:hom_A(a,b)$ amd $g:hom_A(b,c)$, we have $$F(g \circ f) = F g \circ F f$$ In terms of formal [[nLab:Coq]]-code this reads as follows (e.g. [Ahrens-Kapulkin-Shulman 13](AhrensKapulkinShulman13), _[functors_transformations.v](https://github.com/benediktahrens/rezk_completion/blob/master/functors_transformations.v)_): Definition functor_data (C C' : precategory_ob_mor) := total2 ( fun F : ob C -> ob C' => forall a b : ob C, a --> b -> F a --> F b). Definition functor_on_objects {C C' : precategory_ob_mor} (F : functor_data C C') : ob C -> ob C' := pr1 F. Coercion functor_on_objects : functor_data >-> Funclass. Definition functor_on_morphisms {C C' : precategory_ob_mor} (F : functor_data C C') { a b : ob C} : a --> b -> F a --> F b := pr2 F a b. Local Notation "# F" := (functor_on_morphisms F)(at level 3). Definition is_functor {C C' : precategory_data} (F : functor_data C C') := dirprod (forall a : ob C, #F (identity a) == identity (F a)) (forall a b c : ob C, forall f : a --> b, forall g : b --> c, #F (f ;; g) == #F f ;; #F g). Lemma isaprop_is_functor (C C' : precategory_data) (F : functor_data C C'): isaprop (is_functor F). Proof. apply isofhleveldirprod. apply impred; intro a. apply (pr2 (_ --> _)). repeat (apply impred; intro). apply (pr2 (_ --> _)). Qed. Definition functor (C C' : precategory) := total2 ( fun F : functor_data C C' => is_functor F). ## Properties ## By induction on [[identity]], a functor also preserves $idtoiso$ (See [[precategory]]). ### Composition of functors ### For functors $F:A\to B$ and $G:B \to C$, their composite $G \circ F : A \to C$ is given by * The composite $(G_0 \circ F_0): A_0 \to C_0$ * For each $a,b:A$, the composite $$(G_{F a, F b} \circ F_{a,b}):hom_A(a,b)\to hom_C(G F a, G F b)$$ ### Lemma 9.2.9 ### Composition of functors is associative $H(G F)=(H G)F$. **Proof:** Since composition of functions is associative, this follows immediately for the actions on objects and on homs. And since hom-sets are sets, the rest of the data is automatic. $\square$ ### Lemma 9.2.10 ## Lemma 9.2.9 is coherent, i.e. the following pentagon of equalities commutes: $$ \array{ && (K H)(G F) \\ & \nearrow && \searrow \\ ((K H) G) F && && K (H (G F)) \\ \downarrow && && \uparrow \\ (K(H G)) F && \longrightarrow && K( (H G) F) } $$ ## See also ## [[Category theory]] [[natural transformation]] [[full functor]] [[faithful functor]] ## References ## * {#AhrensKapulkinShulman13} [[nLab:Benedikt Ahrens]], [[nLab:Chris Kapulkin]], [[nLab:Michael Shulman]], section 4 of _Univalent categories and the Rezk completion_, Mathematical Structures in Computer Science 25.5 (2015): 1010-1039 ([arXiv:1303.0584](http://arxiv.org/abs/1303.0584)) * {#HoTTBook} [[nLab:UF-IAS-2012|Univalent Foundations Project]], section 9.2 of _[[HoTT Book|Homotopy Type Theory – Univalent Foundations of Mathematics]]_, IAS 2013 [[nLab:Coq]] code formalizing the concept of functors includes the following: * _[functors_transformations.v](https://github.com/benediktahrens/rezk_completion/blob/master/functors_transformations.v)_ category: category theory