Given two functors interpreted as anafunctors, the natural transformations and ananatural transformations between them are the same, so the term ‘ananatural’ is overkill; one only needs it to emphasise the ana-context and otherwise can just say ‘natural’. That is, a ‘natural transformation’ between anafunctors unambigously means an ananatural transformation.
Given two categories and and two anafunctors , let us interpret as spans and of strict functors (where each backwards-pointing arrow is strictly surjective and faithful; see the definition of anafunctor). Form the strict -pullback and consider the strict functors and . Then an ananatural transformation from to is simply a natural transformation between these two strict functors.
More explicitly, if are given by sets of specifications and additional maps (see the other definition of anafunctor), then an ananatural transformation from to consists of a coherent family of morphisms of indexed by the elements of and with common values in . That is:
for each object of , each -specification over , and each -specification over , we have a morphism
for each morphism in , each pair of -specifications over , and each pair of -specifications over , the diagram
is a commutative square.
Of course, an ananatural isomorphism is an invertible ananatural transformation.
Just as natural transformations can be composed vertically to form the morphisms of a functor category, so ananatural transformations can be composed vertically to form an anafunctor category.
Just as natural transformations can also be whiskered by functors and composed horizontally to make a strict 2-category of (strict) categories, (strict) functors and natural transformations, so ananatural transformations can also be whiskered by anafunctors and composed horizontally to make a bicategory of (strict) categories, anafunctors and (ana)natural transformations. Assuming the axiom of choice, is equivalent to ; without choice (and internally), has better properties than and we will usually identify the former with Cat.