Homotopy Type Theory
functor (Rev #1, changes)

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


Let AA and BB be precategories. A functor F:ABF : A \to B consists of

  • A function F 0:A 0B 0F_0 : A_0 \to B_0
  • For each a,b:Aa,b:A, a function F a,b:hom A(a,b)hom B(Fa,Fb)F_{a,b}:hom_A(a,b) \to hom_B(Fa,Fb), generally also denoted FF.
  • For each a:Aa:A, we have F(1 a)=1 FaF(1_a)=1_{F a}.
  • For each a,b,c:Aa,b,c: A and f:hom A(a,b)f:hom_A(a,b) amd g:hom A(b,c)g:hom_A(b,c), we have
F(gf)=FgFfF(g \circ f) = F g \circ F f


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

See also

Category theory in HoTT natural transformation full functor faithful functor


HoTT Book

category: category theory

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.