nLab retrofunctor




A retrofunctor (also called a cofunctor) is a kind of morphism between categories. In contrast to a functor, the assignment on objects of a retrofunctor goes in the opposite direction to the assignment on morphisms.

Retrofunctors generalise both bijective-on-objects functors and discrete opfibrations.

Retrofunctors arise naturally in the study non-cartesian internal categories.

In the literature, the terminology “cofunctor” is common. However, terminology is misleading, as a cofunctor is not the opposite of a functor. We use the terminology “retrofunctor”, as this avoids confusion, and aligns with the concept of monad retromorphism (of which retrofunctors are a motivating example).


A retrofunctor φ:AB\varphi : A \nrightarrow B from a category AA to a category BB consists of a map sending each object aAa \in A to an object φ 0aB\varphi_{0}a \in B and a map sending each pair (aA,u:φ 0abB)(a \in A, u : \varphi_{0}a \to b \in B) to a morphism φ 1(a,u):aa\varphi_{1}(a, u) : a \to a' in AA, where a=cod(φ 1(a,u))a' = cod(\varphi_{1}(a, u)), such that

  • φ 1\varphi_{1} respects codomains: φ 0a=cod(u)\varphi_{0}a' = cod(u) where a=cod(φ 1(a,u))a' = cod(\varphi_{1}(a, u)),

  • φ 1\varphi_{1} preserves identity morphisms: φ 1(a,1 φ 0a)=1 a\varphi_{1}(a, 1_{\varphi_{0}a}) = 1_{a},

  • φ 1\varphi_{1} preserves composition: φ 1(a,vu)=φ 1(a,v)φ 1(a,u)\varphi_{1}(a, v \circ u) = \varphi_{1}(a', v) \circ \varphi_{1}(a, u) where a=cod(φ 1(a,u))a' = cod(\varphi_{1}(a, u)).

Given a pair of retrofunctors φ:AB\varphi : A \nrightarrow B and γ:BC\gamma : B \nrightarrow C, their composite retrofunctor γφ:AC\gamma \circ \varphi \colon A \nrightarrow C sends each object aAa \in A to an object γ 0φ 0aC\gamma_{0}\varphi_{0}a \in C and each pair (aA,u:γ 0φ 0acC)(a \in A, u : \gamma_{0}\varphi_{0}a \to c \in C) to a morphism φ 1(a,γ 1(φ 0a,u))\varphi_{1}(a, \gamma_{1}(\varphi_{0}a, u)) in AA. This defines a category Cof\mathbf{Cof} whose objects are small categories, and whose morphisms are retrofunctors.



The category Cof\mathbf{Cof} of small categories and retrofunctors has an orthogonal factorization system (Bij op,DOpf)(Bij^{op}, DOpf) which factors each retrofunctor φ:AB\varphi : A \nrightarrow B into a bijective on objects functor AIA \leftarrow I followed by a discrete opfibration IBI \to B.


Let Poly(1,1)\mathbf{Poly}(1, 1) be the monoidal category arising from the bicategory of polynomials on the singleton set. Then Cof\mathbf{Cof} is isomorphic to the category of comonoids in Poly(1,1)\mathbf{Poly}(1, 1).


Originally proven in (Ahman-Uustalu 2016). See (Spivak-Niu 2021, Theorem 6.26) for details.



The notion of retrofunctor first appeared under the name comorphism in the paper:

The definition of internal retrofunctor between non-cartesian internal categories was introduced in Section 4.4 of the thesis:

  • Marcelo Aguiar, Internal categories and quantum groups, PhD thesis, Cornell University, 1997 (pdf)

The characterization of retrofunctors as morphisms between directed containers is developed in the papers:

The link between retrofunctors, delta lenses, and split Grothendieck opfibrations is developed in the papers:

Retrofunctors between groupoids and the link with inner automorphisms of groupoids is explored in the paper:

The notion of retrofunctor between partite internal categories is introduced in Definition 5.5 of the paper:

A detailed account of the relationship between retrofunctors and polynomials appears in Chapter 6 of the draft textbook:

  • David Spivak, Nelson Niu, Polynomial Functors: A General Theory of Interaction, 2021 (pdf)

Enrichment in the category of Cof\mathbf{Cof} of categories and retrofunctors is considered in the paper:

The terminology retrofunctor was introduced in:

  • Matthew Di Meglio, The category of asymmetric lenses and its proxy pullbacks. Master’s thesis. Macquarie University, 2021. doi: 10.25949/20236449, pdf

The terminology is justified by the fact that retrofunctors are monad retromorphisms in the double category Span(Set)Span(Set).

Last revised on November 3, 2023 at 09:24:39. See the history of this page for a list of all contributions to it.