An introduction to enriched cofunctors

TL;DR

This paper introduces enriched cofunctors between categories enriched in a distributive monoidal category, establishing a double category framework and exploring enriched lenses and weighted lenses with detailed examples.

Contribution

It extends the concept of cofunctors to enriched categories, defines a double category structure, and connects enriched lenses with weighted lenses, providing new categorical tools.

Findings

Defined a double category of enriched categories, functors, and cofunctors

Established enriched lenses as compatible pairs of functors and cofunctors

Identified weighted lenses as enriched in weighted sets

Abstract

Cofunctors are a kind of map between categories which lift morphisms along an object assignment. In this paper, we introduce cofunctors between categories enriched in a distributive monoidal category. We define a double category of enriched categories, enriched functors, and enriched cofunctors, whose horizontal and vertical 2-categories have 2-cells given by enriched natural transformations between functors and cofunctors, respectively. Enriched lenses are defined as a compatible enriched functor and enriched cofunctor pair; weighted lenses, which were introduced by Perrone, are precisely lenses enriched in weighted sets. Several other examples are also studied in detail.