Is this new? Let *A* be a locally small category. Let *D* be the category whose objects are set-valued bifunctors on *A* (contravariant on the first variable, covariant on the second) and whose maps are the dinatural transformations. Then *A* is a groupoid. Well, OK, what I mean is that dinaturals are closed under composition iff *A* is a groupoid. (And, yes, this could all be done with the category of sets replaced with a topos.) I trust the following is old, but who has a reference? If *A* is a groupoid then *D* is equivalent to the category of presheaves on *A*.
From: Peter Freyd [Let *D* be the category whose objects are] set-valued bifunctors on *A* (contravariant on the first variable, covariant on the second) Two definitional/notational suggestions: 1. "sesquifunctors on A" for the objects of *D* 2. A -X A as a notation for *D* The right-hand half of the X in -X is intended to suggest the contravariant bit. One then has the following hierarchy. A => B "functions" from A to B, viz. !A -o B A -o B (homo)morphisms from A to B A -X B sesquifunctors A\op x A -> B, dinaturally transformed The first two come from linear logic, with !A = FU being interpreted as the underlying object (e.g. underlying set) of A reflected back into the category via F. F serves merely to make the underlying objects the same "kind" as the objects they underlie, avoiding a proliferation of kinds in order to keep linear logic typeless, or at least kindless. Vaughan Pratt
participants (2)
-
Peter Freyd -
Vaughan Pratt