Cofunctor

A cofunctor or retrofunctor is a funny little algebraic widget that arises from the study of Polynomial Functors. We shall present the "fibred" definition below:

A cofunctor $A\to B$ between categories consists of:

• A mapping of objects $F_{0}:A_{0}\to B_{0}$
• A lifting of objects $F^{*}_{0}:(b:B_{0})\to(a:A_{0})\to B(F_{0}(a),b)\to A_{0}$
• A lifting of morphisms $F_{1}^{*}:(b:B_{0})\to(a:A_{0})\to(u:B(F_{0}(a),b))\to A_{0}(a,F_{0}^{*}(b,a,u))$

Such that:

• $F_{0}(F_{0}^{*}(b,a,u))=b$
• $F_{0}^{*}(F_{0}(a),a,\mathrm{id})=a$
• $F_{1}^{*}(F_{0}(a),a,\mathrm{id})=\mathrm{}{id}$
• $F_{1}^{*}(b,a,u\circ v)=F_{1}^{*}(b,?,u)\circ F_{1}^{*}(?,?,v)$

These coherence conditions are super annoying!