nLab
semifunctor

Semifunctors

Idea

A semifunctor is a homomorphism between semicategories, like a functor is a homomorphims between categories.

Definition

A semifunctor FF from a semicategory CC to a semicategory DD is a map sending each object xCx \in C to an object F(x)DF(x) \in D and each morphism f:xyf : x \to y in CC to morphism F(f):F(x)F(y)F(f) : F(x) \to F(y) in DD, such that

  • FF preserves composition: F(gf)=F(g)F(f)F(g\circ f) = F(g)\circ F(f) whenever the left-hand side is well-defined.

If CC is a category, then FF need not preserve its identity morphisms, but this axiom does require that it send them to idempotents in DD.

Relation to Profunctors

In Rel, the bicategory of relations, adjoint pairs of relations (using axiom of choice) are equivalent to functions. Even with choice, the analogous theorem for Prof, the bicategory of profunctors, says that an adjoint pair of profunctors is equivalent, not necessarily to a functor, but instead a semifunctor. If the codomain of the semifunctor is Cauchy complete this is equivalent to a functor, which recovers the usual formulation of this theorem.

Examples

A mapping FF of a category into another category that sends id Xid_X to a nontrivial idempotent endomorphism of F(X)F(X) is a semifunctor but not a functor.

More generally, recall from semicategory that the forgetful functor U:CatSemicatU \colon Cat \to Semicat has a right adjoint GG, which sends a semicategory to its category of idempotents, or Karoubi envelope. Thus to give a semifunctor from a category CC to a (semi)category DD is the same as giving a functor from CC to the Karoubi envelope D¯\bar D of DD (but beware that this correspondence does not hold for natural transformations).

Semifunctors between categories arise in the study of non-extensional type theories such as lambda calculus with β\beta equivalence, but not η\eta equivalence for the function type (see Hayashi 85). Whereas with both β,η\beta, \eta, a function type ABA \to B can be described as a right adjoint functor to A×A \times -, the non-extensional function type can be described by weakening the requirement to the right adjoint being merely a semifunctor.

  • Susumu Hayashi, “Adjunction of semifunctors: categorical structures in nonextensional lambda calculus” Theoretical Computer Science 1985

Revised on October 3, 2017 17:18:44 by Max S. New (129.10.110.48)