Homotopy Type Theory
functor (Rev #7)



The concept if functor is the evident concept of homomorphisms between categories.


Let AA and BB be precategories. Informally, a functor F:ABF : A \to B consists of

  • A function F 0:A 0B 0F_0 : A_0 \to B_0
  • For each a,b:Aa,b:A, a function F a,b:hom A(a,b)hom B(Fa,Fb)F_{a,b}:hom_A(a,b) \to hom_B(F a,F b), generally also denoted FF.
  • For each a:Aa:A, we have F(1 a)=1 FaF(1_a)=1_{F a}.
  • For each a,b,c:Aa,b,c: A and f:hom A(a,b)f:hom_A(a,b) amd g:hom A(b,c)g:hom_A(b,c), we have
F(gf)=FgFfF(g \circ f) = F g \circ F f

In terms of formal Coq-code this reads as follows (e.g. Ahrens-Kapulkin-Shulman 13, 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).
    apply isofhleveldirprod.
    apply impred; intro a.
    apply (pr2 (_ --> _)).
    repeat (apply impred; intro).
    apply (pr2 (_ --> _)).

  Definition functor (C C' : precategory) := total2 (
    fun F : functor_data C C' => is_functor F).


By induction on identity, a functor also preserves idtoisoidtoiso (See precategory).

Composition of functors

For functors F:ABF:A\to B and G:BCG:B \to C, their composite GF:ACG \circ F : A \to C is given by

  • The composite (G 0F 0):A 0C 0(G_0 \circ F_0): A_0 \to C_0
  • For each a,b:Aa,b:A, the composite
    (G Fa,FbF a,b):hom A(a,b)hom C(GFa,GFb)(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(GF)=(HG)FH(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:

(KH)(GF) ((KH)G)F K(H(GF)) (K(HG))F K((HG)F) \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


Coq code formalizing the concept of functors includes the following:

category: category theory

Revision on September 7, 2018 at 08:37:58 by Urs Schreiber. See the history of this page for a list of all contributions to it.