# Homotopy Type Theory functor (Rev #7, changes)

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

# Contents

## Idea

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

## Definition

Let $A$ and $B$ be precategories . A Informally, afunctor $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 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).
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) }$