#
Homotopy Type Theory

functor (Rev #1)

## Definition

Let $A$ and $B$ be precategories. 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(Fa,Fb)$, 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$

## Properties

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

## See also

Category theory in HoTT natural transformation full functor faithful functor

## References

HoTT Book

Revision on September 4, 2018 at 14:22:31 by
Ali Caglayan.
See the history of this page for a list of all contributions to it.