Editing Dual (category theory) (section)

==Formal definition==

We define the elementary language of category theory as the two-sorted [[first order language]] with objects and morphisms as distinct sorts, together with the relations of an object being the source or target of a morphism and a symbol for composing two morphisms.

Let σ be any statement in this language. We form the dual σ<sup>op</sup> as follows: 
# Interchange each occurrence of "source" in σ with "target".
# Interchange the order of composing morphisms. That is, replace each occurrence of <math>g \circ f</math> with <math>f \circ g</math>
Informally, these conditions state that the dual of a statement is formed by reversing [[morphism|arrows]] and [[function composition|compositions]].

''Duality'' is the observation that σ is true for some category ''C'' if and only if σ<sup>op</sup> is true for ''C''<sup>op</sup>.{{sfn|Mac Lane|1978|p=33}}{{sfn|Awodey|2010|p=53-55}}