# Homotopy Type Theory functor precategory (Rev #2, changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

## Definition

For precategories $A,B$, there is a precategory $B^A$, called the functor precategory, defined by

• $(B^A)_0$ is the type of functors from $A$ to $B$.
• $hom_{B^A}(F,G)$ is the type of natural transformations from $F$ to $G$. Proof. We define $(1_F)_a \equiv 1_{F a}$. Naturality follows by the unit axioms of a precategory. For $\gamma : F \to G$ and $\delta : G \to H$, we define $(\delta \circ \gamma)_a \equiv \delta_a \circ \gamma_a$. Naturality follows by associativity. Similarly, the unit and associativity laws for $B^A$ follow from those for $B$.

Proof. We define $(1_F)_a \equiv 1_{F a}$. Naturality follows by the unit axioms of a precategory. For $\gamma : F \to G$ and $\delta : G \to H$, we define $(\delta \circ \gamma)_a \equiv \delta_a \circ \gamma_a$. Naturality follows by associativity. Similarly, the unit and associativity laws for $B^A$ follow from those for $B$.

## Properties

### Lemma 9.2.4

A natural transformation $\gamma : F \to G$ is an isomorphism in $B^A$ if and only if each $\gamma_a$ is an isomorphism in $B$.

Proof. If $\gamma$ is an isomorphism?, then we have $\delta : G \to F$ that is its inverse. By definition of composition in $B^A$, $(\delta \gamma)_a \equiv \delta_a \gamma_a$. Thus, $\delta \gamma = 1_F$ and $\gamma \delta=1_G$ imply that $\delta_a \gamma_a = 1_{F a}$ and $\gamma_a \delta_a = 1_{G a}$, so $\gamma_a$ is an isomorphism.

Conversely, suppose each $\gamma_a$ is an isomorphism?, with inverse called $\delta_a$. We define a natural transformation $\delta : G \to F$ with components $\delta_a$; for the naturality axiom we have

$F f \circ \delta_a=\delta_b \circ \gamma_b \circ F f \circ \delta_a = \delta_b \circ G f \circ \gamma_a \circ \delta_a = \delta_b \circ G f$

Now since composition and identity of natural transformations is determined on their components, we have $\gamma \delta=1_G$ and $\delta \gamma 1_F.\ \square$

### Theorem 9.2.5

If $A$ is a precategory and $B$ is a category, then $B^A$ is a category.

## References

HoTT Book

category: category theory

Revision on September 5, 2018 at 08:25:11 by Ali Caglayan. See the history of this page for a list of all contributions to it.