Capture the discussion on the "general division problem" for posterity
Case Study:
Suppose you have a query Qs:S->R and a schema migration with mappings F:X->S and G:X->T.
We want the query Qt:T->R.
Further suppose that F is not surjective, i.e. information will be lost.
In that case it is not possible to obtain the coquery for F which would be used to compose Qt
Qt = [ toCoQuery F ; Qs ]
In general this is appropriate as a particular query Qs may require the lost data.
There may be queries that do not make use of the lost data and should be legitimately migrated.
This suggests the following formulation...
Qs = [ toQuery F ; Qt ]
The general setup:
Schemas A, B, C
Q1: A-Inst --> B-Inst Q2: B-Inst --> C-Inst Q3: A-Inst --> C-Inst
i.e. Q3 = [ Q1 ; Q2 ]
{note: symbols in bold are not a precisely queries, but are still a functors.}
David Spivak said....
Case "determination":
If you are given Q1 and Q3, and Q2 unknown then
Q2(J):=eval (Q3, coeval (Q1, J)).
This will always come with a natural map
c: eval(Q2, eval(Q1, J)) --> eval(Q3, J)
given by the counit of Q1.
If eval(Q1) is fully faithful (basically, "not lossy") then c will be an iso.
Case "choice":
Now suppose you are given Q2 and Q3, and Q1 unknown then
Q1(J):=coeval(Q2, eval(Q3, J)).
Then there is a natural map
u: eval(Q3, J)--> eval(Q2, eval(Q1, J))
given by the unit of Q2.
If coeval(Q2) is fully faithful then u will be an iso.