From 1e6765533cb0c855a57c696868cc1db0073492ae Mon Sep 17 00:00:00 2001 From: Sergei Winitzki Date: Mon, 21 Oct 2019 21:37:29 -0700 Subject: [PATCH] The text needs to use `a`, `b` consistently with code and formulas --- src/content/3.10/ends-and-coends.tex | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/content/3.10/ends-and-coends.tex b/src/content/3.10/ends-and-coends.tex index 4730c9a9..cdb735da 100644 --- a/src/content/3.10/ends-and-coends.tex +++ b/src/content/3.10/ends-and-coends.tex @@ -418,17 +418,17 @@ \section{Profunctor Composition} Let's explore further the idea that a profunctor describes a relation --- more precisely, a proof-relevant relation, meaning that the set $p\ a\ b$ represents the set of proofs that $a$ is related -to $b$. If we have two relations $p$ and $q$ we can +to $b$. If we have two relations $p$ and $q$, we can try to compose them. We'll say that $a$ is related to $b$ through the composition of $q$ after $p$ if there exist an -intermediary object $c$ such that both $q\ b\ c$ and -$p\ c\ a$ are non-empty. The proofs of this new relation are all +intermediary object $c$ such that both $q\ a\ c$ and +$p\ c\ b$ are non-empty. The proofs of this new relation are all pairs of proofs of individual relations. Therefore, with the understanding that the existential quantifier corresponds to a coend, and the Cartesian product of two sets corresponds to ``pairs of proofs,'' we can define composition of profunctors using the following formula: -\[(q \circ p)\ a\ b = \int^c p\ c\ a\times{}q\ b\ c\] +\[(q \circ p)\ a\ b = \int^c p\ c\ b\times{}q\ a\ c\] Here's the equivalent Haskell definition from \code{Data.Profunctor.Composition}, after some renaming: