Homotopy Type Theory functor > history (Rev #2)

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(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

Properties

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

See also

Category theory natural transformation full functor faithful functor

References

HoTT Book