Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: category theory

Topic: Skolemization of ends

Bartosz Milewski (Oct 20 2020 at 17:15):

I blindly translated Skolem equivalence from logic to end calculus:

$$\forall{x}. \exists{y}. R(x, y) \cong \exists{f}. \forall x. R(x, f x)$$

$$\int_{x \colon C} \int^{y \colon D} P (x, y) \cong \int^{F \colon [C, D]} \int_{x \colon C} P (x, F x)$$

I replaced quantifiers with (co-)ends and relations with profunctors. I wonder under what conditions this might work.

I tried using Yoneda to attack it, but I got stuck

$$Set\Big( \int^{F \colon [C, D]} \int_{x} P (x, F x), s\Big) \cong \int_F Set\Big( \int_{x} P (x, F x), s\Big)$$

although an end over a functor category reminds me of lenses.

John Baez (Oct 20 2020 at 17:52):

I'm not sure I'd heard of "Skolem equivalence". If we try to prove your first equivalence within ZF set theory, I think we need the axiom of choice to prove $\exists{f}. \forall x. R(x, f x)$ starting from $\forall{x}. \exists{y}. R(x, y)$. I'm not sure what this means for an attempt to prove it using coends. I guess one thing it means is that it'll be easier to get a morphism going from

$\int^{F \colon [C, D]} \int_{x \colon C} P (x, F x)$

to

$\int_{x \colon C} \int^{y \colon D} P (x, y)$

than the other way around. (In ZF set theory you can prove a map is an injection and a surjection, and then use the axiom of choice to conclude it's a bijection.)

John Baez (Oct 20 2020 at 17:53):

I'm only mentioning ZF set theory to pinpoint the thing that seems "tricky": proving that the desired $f$ exists.

Jules Hedges (Oct 20 2020 at 18:31):

Bartosz Milewski said:

I blindly translated Skolem equivalence from logic to end calculus:

$$\forall{x}. \exists{y}. R(x, y) \cong \exists{f}. \forall x. R(x, f x)$$

Skolem equivalence is also known as "the axiom of choice", I guess (although I think there's some subtlety that I don't remember, this is the AC that's used in higher order arithmetic, I think it's strictly weaker than the one in ZFC)

Bartosz Milewski (Oct 20 2020 at 19:01):

Yes, this equivalence requires the AoC so one would have to make some size and foundational assumptions about the categories in question. Also, profunctors are more like "proof-relevant" relations, so this might involve intuitionistic logic.

Dan Doel (Oct 20 2020 at 19:12):

Is it actually AC, though? The 'naive' constructive reading is a theorem, because it gets interpreted as $\prod_x \coprod_y$. So does the (co)end formula and using profunctors also not require choices?

Dan Doel (Oct 20 2020 at 19:25):

One might say that the complaint with the naive reading is that it is essentially interpreting it like the (co)end formula, not a proposition.

Martti Karvonen (Oct 21 2020 at 18:25):

Jules Hedges said:

Bartosz Milewski said:

I blindly translated Skolem equivalence from logic to end calculus:

$$\forall{x}. \exists{y}. R(x, y) \cong \exists{f}. \forall x. R(x, f x)$$

Skolem equivalence is also known as "the axiom of choice", I guess (although I think there's some subtlety that I don't remember, this is the AC that's used in higher order arithmetic, I think it's strictly weaker than the one in ZFC)

It is equivalent to AC and not strictly weaker (in the context of ZF). To see this, we show that Skolem-equivalence implies that epis split $Set$: indeed, if $f\colon X\to Y$ is surjective, then the inverse relation is total and by Skolem-equivalence there is a function inside of it which splits $f$.

Bartosz Milewski (Oct 21 2020 at 20:27):

Let me explain how I understand the profunctor interpretation. The left hand side essentially says that for every object x in C there exists and object y in D such that the set P(x, y) is nonempty (this set is interpreted as the set of witnesses to some relation between x and y). The claim is that this assignment from x to y can be made into a functor.

My intuition now is that the coend formulation of existential quantification is constructive, so AoC is not necessary. It's sort of "built into" the coend. Just like the AoC is a _theorem_ in the constructive dependent type theory.

Dan Doel (Oct 21 2020 at 20:44):

Put another way, if the context is instead $\infty$-groupoids, then this is written in HoTT as $(Π_x Σ_y P(x,y)) \simeq (Σ_f Π_x P(x,f(x)))$, no? This doesn't require a choice principle, and is the exact interpretation people use for the constructive interpretation of 'choice'. So, is there a reason it doesn't work for categories?

Bartosz Milewski (Oct 21 2020 at 21:48):

This is very interesting. I was casually looking up Skolem normal form in Wikipedia, saw the formula, and wondered what it would look like using profunctors. Didn't realize that in HoTT this is almost exactly the formula for AoC. Except that they are dealing with "mere propositions" which, I guess, would correspond to profunctors enriched over Bool. And they are truncating everything. So the question is, can this be generalized to Set-valued profunctors. In particular, how would one show the functoriality of F.

Dan Doel (Oct 21 2020 at 21:52):

In HoTT, the proper axiom of choice is like $Π_x \Vert Σ_y P(x,y) \Vert → \Vert Σ_f Π_x P(x,f(x))\Vert$, or it can be simplified to $Π_x \Vert P(x) \Vert → \Vert Π_x P(x)\Vert$.

Dan Doel (Oct 21 2020 at 21:54):

I'm not exactly sure how it translates back to ordinary stuff. Bool-enrichment seems promising.

Dan Doel (Oct 21 2020 at 21:57):

I should have said above, by "this" I meant the coend formula for $\infty$-groupoids $C$, $D$ and $P(x,y)$.

Dan Doel (Oct 21 2020 at 22:01):

Maybe it still doesn't work out in the set theoretic context, though, because functors are too on-the-nose.

Bartosz Milewski (Oct 22 2020 at 01:30):

I think this is the standard proof of:

$$\prod_{x\colon X} \Big( \sum_{y \colon Y(x)} P(x, y) \Big) \to \sum_{f \colon \prod_{x \colon X} Y(x)} \Big( \prod_{x \colon X} P(x, f x) \Big)$$

The left hand side is a function that, for every $x$, produces a pair $y:Y(x)$ and a set $P(x, y)$. We want to implement $f$ which, for every $x$ produces a $y$ of the type $Y(x)$. For that, we use the projection that picks the first component of our original function. With that $f$, we can now define a function that, for every $x$ will produce a set $P(x, f x)$. Again, we use our original function, this time projecting the second component.

Dan Doel (Oct 22 2020 at 01:52):

So, the reason that the HoTT axiom of choice is no longer constructive is that truncation adds ways for the left-hand Π to be functorial, so it can essentially map connected points of $X$ arbitrarily, without worrying whether their image is connected in $Y$. However, the right-hand $f$ doesn't have that luxury, it must be an actual functorial mapping, and there is no obvious way to figure out this choice of structure. So, the worry would be that a coend in $\mathsf{Set}$ also allows the left hand end to be more lax in its assignments than an actual functor.

Dan Doel (Oct 22 2020 at 01:53):

However, I don't know if that happens.

sarahzrf (Oct 22 2020 at 01:55):

if you enrich over truth values, then ends and coends really are ∀ and ∃, btw

sarahzrf (Oct 22 2020 at 01:55):

pick C and D to be discrete preordered sets, and this gives you axiom of choice

sarahzrf (Oct 22 2020 at 01:56):

so unless im missing something, if this works in Set without choice, it's going to have to be for reasons that are special to Set

Bartosz Milewski (Oct 23 2020 at 19:59):

I think this might actually work.

$$\int_{x \colon C} \int^{y \colon D} P (x, y) \cong \int^{F \colon [C, D]} \int_{x \colon C} P (x, F x)$$

Here's the sketch. Think of $P(x, y)$ as a fake hom-set from $x$ to $y$, a la collage of C and D. Pick an $x$. The coend over $y$ is like a sum of all those fake hom-sets emanating from $x$ (modulo some identifications). So we have a family of these sums indexed by $x$. Then the end over $x$ is like a set of tuples. An element of the end is a tuple that picks, for every $x$, one arrow from each of these sums. But this arrow goes to a particular $y$. So we have a mapping $x \mapsto y$. I bet this mapping is functorial. This would define our functor $F$ for that particular element of the end.

The right hand side builds the same set but from the other end. It starts with $P(x, F x)$, which is a fake hom-set from $x$ to $F x$. The end over $x$ is a set of tuples, picking one arrow from each fake hom-set. But that's exactly the tuple that was used to define this $F$.

Jules Hedges (Oct 23 2020 at 21:41):

Could it be that this is a "missing axiom" of co/end calculus? Something that's always true but isn't provable from the other axioms?

Bartosz Milewski (Oct 23 2020 at 21:49):

You mean, like not going through the definition of a coend, just through Yoneda and continuity? Maybe. Fosco pointed out that most of these are actually (co-)limits, except the rightmost one, which is a full-blown end over a profunctor.

Bartosz Milewski (Oct 24 2020 at 02:10):

I'm working through a formal proof and it's mostly straightforward, but the functoriality is a bit tricky. Also, I think F should be contravariant.

Guillaume Boisseau (Oct 24 2020 at 02:16):

Oh, I remember wondering about this!

Guillaume Boisseau (Oct 24 2020 at 02:16):

I think F has to be constant on the connected components of C

Guillaume Boisseau (Oct 24 2020 at 02:17):

Which makes it obviously functorial

Guillaume Boisseau (Oct 24 2020 at 02:20):

And I _think_ we have the following magic: constructing a particular F obviously requires AoC. However, I believe all the relevant Fs will be made equal by the coend. So the overall mapping may not require AoC

Guillaume Boisseau (Oct 24 2020 at 02:27):

Here's my reasoning for connected components. Take $\alpha: \int_x \int^y P(x, y)$. Each $\alpha_x$ is a connected component of $\Sigma_y P(x,y)$ (by which I mean category of elements). Naturality in $x$ means that if $x$ and $x'$ have a morphism between them, then $\alpha_x$ and $\alpha_{x'}$ will have the same set of ys, with no obvious reason to go between them. So I think the only reasonable choice is to pick a single $y$ per connected component in $C$. And then I believe we get nicely an element of $\int_x P(x,F x)$

Guillaume Boisseau (Oct 24 2020 at 02:39):

And indeed, all such Fs are related by a natural transformation that changes the y, which means that I don't need choice!

Guillaume Boisseau (Oct 24 2020 at 02:46):

Mapping the other way seems to work nicely without Set-specific shenanigans

Bartosz Milewski (Oct 24 2020 at 03:56):

I don't see why AoC would be needed. The action of F on objects is totally determined. The action on morphisms is subtle. The limit over x exists only if the colimits are functorial over x. It's straightforward to lift a morphism to a coproduct, but to lift it to a colimit, it must preserve equivalence classes. Essentially, if x's are connected than the y's must be connected too, otherwise the family of colimits is not functorial. At least that's what it looks to me at this point.

sarahzrf (Oct 24 2020 at 04:44):

sarahzrf said:

if you enrich over truth values, then ends and coends really are ∀ and ∃, btw

sarahzrf said:

pick C and D to be discrete preordered sets, and this gives you axiom of choice

sarahzrf said:

so unless im missing something, if this works in Set without choice, it's going to have to be for reasons that are special to Set

@Bartosz Milewski see above

Bartosz Milewski (Oct 24 2020 at 06:09):

In constructive type theory, axiom of choice is a theorem. It's because the left hand side is proof-relevant, so it carries with itself the proof: the choice.

Reid Barton (Oct 24 2020 at 14:19):

I'm trying to understand what happens when $C$ and $D$ are one-object groupoids $C = BG$, $D = BH$. Then, the profunctor $P$ amounts to giving a set with commuting actions of $G$ and $H$. We could think of one of $G$ and $H$ acting on the left, the other on the right (probably which way around it goes will depend on your conventions for profunctors or something).

On the left hand side, we first take the set of orbits under $H$, which still have a $G$-action because the original actions commuted, then take the $G$-fixed points. On the right hand side, it seems a bit hard to describe exactly what we have, but if we replace the coend by a coproduct, we get the disjoint union over all $F : G \to H$ of the set of those elements which are always fixed by simultaneously acting by $x \in G$ and $F(x) \in H$.

Reid Barton (Oct 24 2020 at 14:19):

Now, I'm pretty sure we can arrange for the left hand side to be nonempty while the right hand side (even with a coproduct instead of a coend) is empty.

Reid Barton (Oct 24 2020 at 14:23):

For example, take $G = \mathbb{Z}/2$ and $H = \mathbb{Z}$ and let them both act on $\mathbb{Z}/2$ by translation. The left hand side is a singleton because after taking the $H$-orbits, the single remaining orbit is fixed (necessarily) by $G$. On the other hand there are no nonconstant maps $F : G \to H$, so on the right hand side we only need to consider the zero map $F$. But no element of our set is fixed by acting simultaneously by $x \in G$ and by $F(x) = 0 \in H$.

Dan Doel (Oct 24 2020 at 14:50):

@Bartosz Milewski In constructive type theory, you can't accurately write down the propositional version without truncation (or some other modification). If you have truncation, it's not a theorem.

I don't know why people keep talking about the propositional version, though, because that isn't what the question was about, and the answer isn't necessarily the same.

Reid Barton (Oct 24 2020 at 14:52):

In homological algebra, we'd probably do something like, in addition to the term indexed by $\mathrm{Hom}(G, H) = \mathrm{Ext}^0(G, H)$, have a second term somewhere involving $\mathrm{Ext}^1(G, H)$ (which is nontrivial in this case $G = \mathbb{Z}/2$, $H = \mathbb{Z}$). But I don't know how to make sense of that in the original context.

Dan Doel (Oct 24 2020 at 15:01):

Prima facie, it seems like it's going to have a similar problem as the actual axiom of choice in HoTT. The statement is:

choose : (∀ x → ∥ Σ[ y ∈ B ] P x y ∥₂) → ∥ Σ[ f ∈ (A → B) ] (∀ x → P x (f x)) ∥₂

B and A → B are groupoids, so those truncations are actually doing something. And the problem is that the one on the left is adding higher path structure that the f on the right can't use.

Dan Doel (Oct 24 2020 at 15:03):

If B were a set it would be a theorem, though, I believe.

Reid Barton (Oct 24 2020 at 15:24):

(For those unfamiliar with h-levels, ₂ means ${}_{0}$.)

Dan Doel (Oct 24 2020 at 15:26):

Yeah, I was actually expecting it to be 0, but the library I'm using changed it, apparently.

Reid Barton (Oct 24 2020 at 15:30):

Dan Doel said:

So, the reason that the HoTT axiom of choice is no longer constructive is that truncation adds ways for the left-hand Π to be functorial, so it can essentially map connected points of $X$ arbitrarily, without worrying whether their image is connected in $Y$. However, the right-hand $f$ doesn't have that luxury, it must be an actual functorial mapping, and there is no obvious way to figure out this choice of structure. So, the worry would be that a coend in $\mathsf{Set}$ also allows the left hand end to be more lax in its assignments than an actual functor.

We can see how this plays out in the example I gave above. Given an element on the left-hand side, namely an $H$-orbit fixed by $G$, pick an element $a$ in the orbit. Since the $H$-orbit is fixed by $G$ it must mean that if we act on $a$ by any element $x \in G$, we get an element in the same orbit, that is, there must be some $y \in H$ whose action takes us back to the original element $a$. Then the element $a$ would be fixed by simultaneously acting by $x \in G$ and $y \in H$. However, the assignment $x \mapsto y$ is not a function because the choice of $y$ is not unique. In this case, we only get a function from $G = \mathbb{Z}/2$ to the quotient $\mathbb{Z}/2$ of $H = \mathbb{Z}$ (namely, the identity function) and there is no way to lift it to a group homomorphism from $G$ to $H$.

Bartosz Milewski (Oct 24 2020 at 17:22):

Let's talk about the role of truncation in the AoC. When we say that there is a family of non-empty sets, the proof-relevant version of it carries the proof of non-emptiness. How do you prove a set is non-empty? By producing an element of it. So the choice of an element from each set is already encoded in the proof of the left-hand side. So there's nothing to it.

Truncation, on the other hand states that there exist a proof of non-emptiness, but it's not provided. So you know that picking an element is possible, because you know the set is non-empty, but the choice of which element is up to you. And that's the rub: how do you make infinitely many choices?

sarahzrf (Oct 24 2020 at 18:20):

i dont know if id say "it's not provided"

sarahzrf (Oct 24 2020 at 18:20):

arguably it would be more accurate to say that it's provided but you're not allowed to care which one it is

sarahzrf (Oct 24 2020 at 18:23):

for example, note that (depending on how your system works) you likely can eliminate an ∃ and get an inhabitant out, you just need to make sure that your elimination descends to the truncation

sarahzrf (Oct 24 2020 at 18:23):

which is what you need to do, in order to prove, say, finite choice

Bartosz Milewski (Oct 24 2020 at 19:45):

@Reid Barton : This is a good example. The colimit on the left is a set of orbits of H acting on the set $P(\bullet , \bullet )$. In order to define the outer limit, this mapping $\bullet \to Set$ must be functorial. For that, the action of G must preserve the orbits of H. This is what I meant in my previous comment. Once we have that, we have the functor $F$.

Reid Barton (Oct 24 2020 at 20:06):

Bartosz Milewski said:

Once we have that, we have the functor $F$.

This last step doesn't work--you only get (for a given element $a$ of the original set) a well-defined map from $G$ to the quotient of $H$ by the subgroup that fixes $a$, and there might not be any way to lift this map to $H$ itself.

Dan Doel (Oct 24 2020 at 20:40):

@Bartosz Milewski Truncated things are still completely constructive, unless non-constructive axioms are added. The problem is as sarahzrf says. In fact, if things were just 'discarded', AoC would be somewhat more justifiable, because the consequent would just be completely discarded.

When you have $Π_{x:A} \Vert Σ_{y:B} P(x,y)\Vert$, you have something like a mapping from points of $A$ to points of $B$, but the paths of $B$ need not be used for paths of $A$, because truncation has added some. So, trying to use the mapping $x \mapsto y$ as a function/functor is invalid, because it may not preserve path structure. But, in $\Vert Σ_{f:A→B} ... \Vert$, constructively, we are still obligated to exhibit an actual function that properly respects path structure. It's not just, "one could exist."

Another way to look at it from the cubical presentation is that $A$ has intermediate points $p(i)$ between $x$ and $y$ when $p : x \equiv y$. In $A → B$, and intermediate point of $A$ must be mapped somewhere in $B$. But this is not the case for $A → \Vert B \Vert$, because truncation adds paths (and therefore intermediate points) between all points of $B$. So, AoC is asserting that even though we aren't given choices of points of $B$ for every point of $A$, we could somehow choose actual points of $B$ for every point of $A$, merely because the extra paths are eventually attached to points of $B$.

Dan Doel (Oct 24 2020 at 20:56):

The set-truncated version has the same problem, but one level up. There can be intermediate points in squares $p(i,j) : A$ that are not mapped to actual points in $B$, because set-truncation fills in all squares. So somehow choices must be made.

The reason it's not constructive/computable is the same reason as always. Because these things are 'filled in' in $\Vert B \Vert$ but not in $B$, there might not be enough structure in $B$ to act 'locally' at each point. So some kind of canonical representative needs to be calculated. Computably this only works out if you can do some kind of total search. And the various flavors of AoC are just asserting that 'a canonical representative exists,' without telling you what it is.

Dan Doel (Oct 24 2020 at 21:03):

If we know that $B$ is a(n h-)set, though, then every square was already filled in. So we could construct a functorial mapping by working with local data, and this is what the induction principle for truncation allows.

sarahzrf (Oct 24 2020 at 21:03):

(for the record, strictly speaking, there are notions of "computationally meaningful proof"—in realizability, say—where the behavior of ∃ is to "not provide a witness", and choice does tend to fail for reasons to do with this in these cases)

sarahzrf (Oct 24 2020 at 21:04):

(but that's not how, say, working in an intensional type theory, works)

sarahzrf (Oct 24 2020 at 21:04):

(i think there might be CMU-flavored type theories out there with this kind of ∃ behavior...)

Dan Doel (Oct 24 2020 at 21:05):

I'm not sure which thing you're talking about. If you make something propositional by actually throwing away information, then getting it back is another obstacle, yeah. :)

Dan Doel (Oct 24 2020 at 21:08):

There are also 'computationally meaningful' interpretations of the axiom of choice, but they work by changing the meaning of all the existential sorts of statements to a, "you can't prove that there isn't," sort of thing.

sarahzrf (Oct 24 2020 at 21:12):

well, you can do realizability stuff where a realizer for ∃x. φ(x) is literally just a realizer for φ(a) for some a, and the realizer itself doesn't need to indicate which a

sarahzrf (Oct 24 2020 at 21:13):

this probably works best in a classical metatheory...?

Dan Doel (Oct 24 2020 at 21:13):

I'm not sure. That might work for 'proof irrelevant' things.

Dan Doel (Oct 24 2020 at 21:17):

I think the problem is that you run into difficulty with the behavior of quotients and whatnot in those scenarios, although I don't know the details.

sarahzrf (Oct 24 2020 at 21:19):

actually wait ummm depending on how you phrase "choice" and how narrowly you define realizability, you may actually have choice of certain kinds

sarahzrf (Oct 24 2020 at 21:19):

ignore me, i dont actually know that much about realizability >.>

Reid Barton (Oct 24 2020 at 21:25):

Dan Doel said:

Bartosz Milewski In constructive type theory, you can't accurately write down the propositional version without truncation (or some other modification). If you have truncation, it's not a theorem.

I don't know why people keep talking about the propositional version, though, because that isn't what the question was about, and the answer isn't necessarily the same.

I think the comparison to the propositional version is indirectly relevant in the following sense.
Let's restrict the original question to the case where $C$ and $D$ are groupoids, for simplicity.
Then the coend $\int^D$ involves a hidden truncation, as well. The "better" version of this operation would produce a groupoid/1-type, but the Set-valued coend truncates this back to a set. Another way to say this is that the inclusion of sets in groupoids (or spaces) doesn't preserve this coend/colimit.
The inclusion of sets into spaces does preserve some colimits, including for example all coproducts. So that's why when $C$ and $D$ are merely sets, the original map really is an isomorphism (the "constructive axiom of choice").

Reid Barton (Oct 24 2020 at 21:27):

The fact that the "constructive axiom of choice" does hold (HoTT book theorem 2.15.7) makes me think that, at least when $C$ and $D$ are groupoids, the original map ought to be an isomorphism if we interpret everything as happening in spaces.
However, it's not clear to me how this actually works in the example I gave above.

Reid Barton (Oct 24 2020 at 21:32):

A similar thing happens between Prop and Set too--if you have an "axiom of unique choice" then the inclusion of Prop in Set preserves disjoint coproducts, and then the $\forall \exists$ version of the statement holds when the coproducts on the left are disjoint (which just gives you the original axiom of unique choice back).

Dan Doel (Oct 24 2020 at 21:45):

Well, I understand that. One of your earlier messages was what made me think of the set-truncated version in HoTT, which makes the answer reasonably obvious.

However, when you do move to the groupoid-truncated case, it becomes a theorem, since the inputs were groupoids by hypothesis (and the truncations can just be removed). So one can't just assume that it doesn't work for all truncations because it doesn't work for the prop one. One of the enrichments actually is sufficiently special, just not the set one.

Guillaume Boisseau (Oct 25 2020 at 14:13):

@Bartosz Milewski The coend does not give me a choice of y for every x, it gives me an equivalence class of ys for every x. So there's a choice to be made, if you're trying to construct a particular F. However I have outlined that since you don't need to construct a particular F, you never end up needing to make such a choice. Of course, I've only been working with the non-enriched case; no idea how to generalize beyond

Guillaume Boisseau (Oct 25 2020 at 14:15):

Also I hoped my outline of a proof of equivalence would be an answer to your initial question, but I seem to have missed something

Dan Doel (Oct 25 2020 at 17:06):

Oh, I guess that must mean it can be reduced to only requiring excluded middle rather than choice in the details of set theory.

Bartosz Milewski (Oct 27 2020 at 21:32):

@Reid Barton : I finally got to analyzing your counter-example (I don't have much experience with profunctors on groupoids, so I had to visualize a few examples first). So the image of the profunctor $P(\bullet, \bullet)$ is a two-element set. There are two morphisms in C, forming additive group modulo 2. Their action on the set is: identity and flip. Morphism in D are integers from Z. The even ones act as identity, and odd ones as flip. On the left, we first take the colimit, which is our set with identifications that form orbits of Z. There is only one such orbit, so we get a singleton set as the colimit. The limit of this colimit is again the singleton. The problem is on the right hand side. We want to construct a functor F. On morphisms, it must map G to H preserving group structure (composition). There is only one such map, taking both morphisms to zero. The end must satisfy the wedge condition, which degenerates to a simple equation $id\, x = flip\, x$, which cannot be satisfied. The colimit of an empty set is empty, which is not the same as the left hand side. (Sorry for the verbosity.)

I wonder if there are some restrictions on categories or profunctors that would make it work.