12,080
edits
Changes
Directory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 11:00, 27 March 2009
, 11:00, 27 March 2009→Functor: markup
===Functor===
===Functor===
<pre>
{| align="center" cellpadding="8" width="90%" <!--QUOTE-->
|
|
<p>'''Definition 1.3.''' A ''functor'' <math>F : \mathcal{A} \to \mathcal{B}</math> is first of all a morphism of graphs (see Example C4), that is, it sends objects of <math>\mathcal{A}</math> to objects of <math>\mathcal{B}</math> and arrows of <math>\mathcal{A}</math> to arrows of <math>\mathcal{B}</math> such that, if <math>f : A \to A',</math> then <math>F(f) : F(A) \to F(A').</math> Moreover, a functor preserves identities and composition; thus:</p>
<p>F(1_A) = 1_F(A),</p>
<p>F(gf) = F(g)F(f).</p>
<p>In particular, the identity functor 1_$A$ : $A$ -> $A$ leaves objects and arrows unchanged and the composition of functors F : $A$ -> $B$ and G : $B$ -> $C$ is given by:</p>
<p>(GF)(A) = G(F(A)),</p>
<p>(GF)(f) = G(F(f)),</p>
<p>for all objects A of $A$ and all arrows f : A -> A' in $A$.</p>
</pre>
<p>(Lambek & Scott, 6).</p>
|}
===Natural Transformation===
===Natural Transformation===