Homotopy Type Theory
functor (Rev #8, changes)

Showing changes from revision #7 to #8: Added | Removed | Changed

Contents

Idea

The concept definition if offunctor in homotopy type theory is a straightforward translation of the evident ordinary concept one. However, the notion ofhomomorphismsunivalent category? between allows us to construct some such functors that in classical mathematics would require either the categories axiom of choice or the use of anafunctors.

Definition

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 Formally, terms the type of formal functors fromCoqAA -code this to reads as follows (e.g.Ahrens-Kapulkin-Shulman 13BB , isfunctors_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).
Func(A,B) F 0:A 0B 0 F: a,b:Ahom A(a,b)hom B(Fa,Fb)( a:AF(1 a)=1 Fa)×( a,b,c:A f:hom A(a,b) g:hom A(b,c)F(gf)=FgFf) Func(A,B) \coloneqq \sum_{F_0:A_0\to B_0} \sum_{F:\prod_{a,b:A} hom_A(a,b) \to \hom_B(F a,F b)} \Big(\prod_{a:A} F(1_a) = 1_{F a}\Big) \times \Big( \prod_{a,b,c:A} \prod_{f:\hom_A(a,b)} \prod_{g:\hom_A(b,c)} F(g \circ f) = F g \circ F f\Big)

A formal definition in Coq? can be found in Ahrens-Kapulkin-Shulman 13.

Properties

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

References

CoqCoq? code formalizing the concept of functors includes the following:

category: category theory

Revision on September 7, 2018 at 14:03:31 by Mike Shulman. See the history of this page for a list of all contributions to it.