Contents

# Contents

## Idea

The definition of functor in homotopy type theory is a straightforward translation of the ordinary one. However, the notion of (univalent) category allows us to construct some such functors that in classical mathematics would require either the (classical) axiom of choice or the use of anafunctors.

## 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$

Formally, the type of functors from $A$ to $B$ is

$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 $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) }$

Category theory

natural transformation

full functor

faithful functor

## References

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

category: category theory

Last revised on October 11, 2018 at 06:38:46. See the history of this page for a list of all contributions to it.