Homotopy Type Theory
functor > history (Rev #4)
Definition
Let A A and B B be precategories . A functor F : A → B F : A \to B consists of
A function F 0 : A 0 → B 0 F_0 : A_0 \to B_0
For each a , b : A a,b:A , a function F a , b : hom A ( a , b ) → hom B ( F a , F b ) F_{a,b}:hom_A(a,b) \to hom_B(F a,F b) , generally also denoted F F .
For each a : A a:A , we have F ( 1 a ) = 1 F a F(1_a)=1_{F a} .
For each a , b , c : A a,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 ( g ∘ f ) = F g ∘ F f F(g \circ f) = F g \circ F f
Properties
By induction on identity , a functor also preserves idtoiso idtoiso (See precategory ).
Composition of functors
For functors F : A → B F:A\to B and G : B → C G:B \to C , their composite G ∘ F : A → C G \circ F : A \to C is given by
The composite ( G 0 ∘ F 0 ) : A 0 → C 0 (G_0 \circ F_0): A_0 \to C_0
For each a , b : A a,b:A , the composite( G F a , F b ∘ F a , b ) : hom A ( a , b ) → hom C ( G F a , G F b ) (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 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:
( K H ) ( G F ) ↗ ↘ ( ( K H ) G ) F K ( H ( G F ) ) ↓ ↑ ( K ( H G ) ) F ⟶ K ( ( H G ) F )
<!-- Created with SVG-edit - https://github.com/SVG-Edit/svgedit-->
Layer 1
\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)
}
\begin{svg}
<svg width="640" height="480" xmlns="http://www.w3.org/2000/svg" xmlns:svg="http://www.w3.org/2000/svg">
<!-- Created with SVG-edit - https://github.com/SVG-Edit/svgedit-->
<g class="layer">
<title>Layer 1</title>
<path d="m181.62251,199.62251l132.82468,-96.63715l132.82499,96.63715l-50.7344,156.36285l-164.18071,0l-50.73455,-156.36285z" fill="none" id="svg_3" stroke="#000000" stroke-width="5"/>
</g>
</svg>
\end{svg}
See also
Category theory natural transformation full functor faithful functor
References
HoTT Book
Revision on September 4, 2018 at 22:54:58 by
Ali Caglayan .
See the history of this page for a list of all contributions to it.