Practice: Mappings That Preserve Structure

(a) Fifteen.

A triple $(a,b,c)$ is composable when the target of $c$ is the source of $b$, and the target of $b$ is the source of $a$. Enumerating over the six arrows under that condition gives 15 composable triples, and associativity $a\circ (b\circ c)=(a\circ b)\circ c$ holds in all fifteen, so the structure is a category.

Most of the fifteen involve at least one identity and are immediate once the identity laws hold. The triples worth attention are those built from $f$ and $g$, where the composite $gf$ is actually consulted.

(b) Why a subset settles nothing.

Associativity is universally quantified: it claims the equation holds for every composable triple. A single failing triple refutes the claim outright, so the negative case is decided by one counterexample.

The positive case has no such shortcut. Triples that pass constrain only themselves. Nothing about the axioms lets agreement on one triple propagate to another. A sample that passes therefore leaves the claim exactly where it started: undecided, because the unchecked triples are precisely where a counterexample would hide.

This is why a verification should report the count. "Associativity holds" is an assertion; "associativity holds, checked on all 15 composable triples" is a verification, because a reader can confirm the enumeration was complete.

(a) Identity law.

$F({\mathrm{id}}_A)={\mathrm{id}}_X$, and ${\mathrm{id}}_{F(A)}={\mathrm{id}}_X$ since $F(A)=X$ ✓.

$F({\mathrm{id}}_B)={\mathrm{id}}_X$, and ${\mathrm{id}}_{F(B)}={\mathrm{id}}_X$ since $F(B)=X$ ✓.

$F({\mathrm{id}}_C)={\mathrm{id}}_Y$, and ${\mathrm{id}}_{F(C)}={\mathrm{id}}_Y$ since $F(C)=Y$ ✓.

All three objects check.

(b) Composition law.

The pair that carries content is $(g,f)$, the only pair of non-identity arrows that composes:

Equal ✓.

The remaining composable pairs each involve an identity, $({\mathrm{id}}_B,f)$, $(f,{\mathrm{id}}_A)$, $({\mathrm{id}}_C,g)$, $(g,{\mathrm{id}}_B)$, $({\mathrm{id}}_C,gf)$, $(gf,{\mathrm{id}}_A)$, and the three identity-with-itself pairs. Every one of these is satisfied automatically once part (a) holds, since both sides reduce to the image of the non-identity arrow. They should be listed, and they contribute no information.

Both laws hold, so $F$ is a functor.

(c) Why collapsing is permitted.

The definition requires exactly two things: that identities go to identities, and that the image of a composite equals the composite of the images. Nothing requires $F$ to be injective on objects or on arrows, and nothing requires a non-identity arrow to have a non-identity image.

The distinction the laws draw is between losing information and being inconsistent. $F$ loses information: knowing $F(f)={\mathrm{id}}_X$ does not let you recover $f$, and knowing an object maps to $X$ does not say whether it was $A$ or $B$. That is permitted, and the constant functor, every object to one object, every arrow to its identity, is the extreme case, still a functor.

What is forbidden is assigning $gf$ something that contradicts the assignments to $f$ and $g$. $F$ never does: whatever it discards, it discards consistently, so the two routes to an image of a composite always agree.

This is why satisfying the laws is a floor rather than a merit. A functor can be entirely uninformative and still be a functor; what it cannot be is self-contradicting.

(a) The composition law on the pair $(g,f)$.

Since ${\mathrm{id}}_Y\ne h$, they are distinct arrows of $\mathcal{D}$, the law fails, and $G$ is not a functor. This is the pair to choose because it is the only composable pair of non-identity arrows. Pairs involving an identity are satisfied automatically once the identity law holds, so checking those first would consume effort and return nothing. (b) What the colleague's evidence establishes. Their claims are correct as stated. Every object does have an image, and every arrow does land correctly: $f:A\to B$ maps to $h:X\to Y$ with $G(A)=X$ and $G(B)=Y$; $g:B\to C$ maps to ${\mathrm{id}}_Y:Y\to Y$ with $G(B)=G(C)=Y$; $gf:A\to C$ maps to ${\mathrm{id}}_Y$, which, note, requires $G(A)=X$ and $G(C)=Y$, and ${\mathrm{id}}_Y$ runs $Y\to Y$, so this last assignment is in fact already ill-typed. Taking their claim at face value for the arrows where it does hold, the point stands. What these checks establish is the typing condition: that images of arrows have endpoints consistent with the object map. That condition is necessary, and its role is enabling rather than deciding. It is what makes the composite $G(g)\circ G(f)$ a defined arrow, so that the composition law can be stated at all. A mapping failing it is not a candidate; a mapping passing it is a candidate whose status is still open. Why their checks cannot decide: the object map and the endpoint condition each examine one assignment at a time. The composition law is a constraint relating three assignments jointly, what $G$ does to $f$, to $g$, and to $gf$. An inconsistency among three choices is invisible to any check that looks at them individually, which is exactly the situation here: each of $G(f)$, $G(g)$, $G(gf)$ is individually unobjectionable, and the trouble is only in their relationship. This is the general shape of the error. The conditions that are easy to verify are not the ones that decide, and a mapping can pass everything inspection offers while failing the one law that carries the meaning.

(a) The conclusion is unsupported.

Because $P$ and $Q$ are constant functors, $P(n)={\mathrm{id}}_X$ and $Q(n)={\mathrm{id}}_Y$ for every arrow $n$, whatever $n$ happens to be. So the two routes are

and they agree for a reason that has nothing to do with which arrow was chosen. The arrow $n$ does not appear in either result.

The check was also insensitive to $\alpha$: replacing $h$ by any other arrow $X\to Y$ would give agreement just the same, since both sides would reduce to that arrow. No assignment could have failed.

A check whose outcome is fixed in advance confirms that the procedure was carried out correctly, both routes evaluated, results compared, and carries no information about the condition being checked. The example is degenerate, and reporting it as evidence about naturality's difficulty mistakes the exercise for the result.

(b) What would make it evidence.

The verification needs functors that act differently on arrows, so the two routes could in principle diverge. Then agreement is a fact about the particular transformation rather than a consequence of the shape of the example.

A case that meets this: take the list functor, where $\mathrm{map}f$ genuinely depends on $f$. The transformation reverse satisfies

and it holds because reversing rearranges positions without examining elements.

That this is a real constraint is shown by sort, which has the same type and fails: sort inspects elements, so mapping before sorting can produce a different order than sorting before mapping, as soon as $f$ does not preserve the ordering. Two transformations of identical shape, one natural and one not, which is what a non-degenerate check looks like.

The general point. When reporting a verification, ask whether the check could have come out the other way. If not, say so: an unfailable check is worth recording as a confirmation of method, and is not evidence about the thing checked.

(a) map id returns $[c,b,a]$.

The identity law requires map id = id, so map id applied to $[a,b,c]$ should give $[a,b,c]$. This implementation reverses, producing $[c,b,a]$. The law fails, and it fails on the simplest possible input. No clever function is needed to expose it, only a container with more than one element.

(b) The rewrite changes the result.

Before the rewrite, map f then map g: the first reverses to $[f(c),f(b),f(a)]$, the second reverses again, giving

Two reversals cancel, so the original order is restored.

After the rewrite, map (g . f) is a single map and reverses once:

The two results are reverses of one another, so they differ whenever the container has more than one distinct element.

The optimisation is valid only because the composition law is assumed: map g. map f = map (g. f) is precisely that law. With the law broken, the rewrite is unsound, and the program's output depends on whether the optimiser fired, which may vary with build flags, inlining decisions, or compiler version. That is the reason such bugs are hard to trace: the source code is unchanged, and the behaviour depends on a transformation nobody wrote.

(c) Why the tests missed it, and what would catch it.

Reversing a single-element container is the identity on it, so every law the suite could check is satisfied vacuously by the only inputs it supplies. The tests are not weak in coverage of lines, map runs every time, but in coverage of the property: they exercise the one input shape on which a reversing map is indistinguishable from a correct one.

A test that catches it checks the laws as laws: map id xs == xs and map g (map f xs) == map (g . f) xs, over containers with at least two distinct elements, ideally property-based over randomly generated containers and functions. The law is the specification, and testing anything narrower than the law tests something other than what the optimiser relies on.

(a) The defect: incomplete quantification.

The composition law is a claim about every composable pair. The writer checked two, and stopped. The pair carrying the content, $(g,f)$, the only pair of non-identity arrows that composes, was never examined.

The flaw is in the scope of the check, not in any individual claim. Every sentence in the submission is true, which is what makes the error instructive: a verification can consist entirely of correct statements and still establish nothing, if what it quantified over was not what the law quantifies over.

(b) What a complete verification finds.

Since ${\mathrm{id}}_Y\ne h$, the composition law fails and $G$ is not a functor. One pair decides it.

(c) What the two performed checks contributed: nothing.

Both $({\mathrm{id}}_B,f)$ and $(g,{\mathrm{id}}_B)$ involve an identity arrow. Once the identity law holds, which the writer had already established, such pairs are satisfied automatically: both sides reduce to the image of the single non-identity arrow. So these checks could not have failed, and their agreement was guaranteed before they were run.

This compounds the error rather than mitigating it. The writer performed two checks, obtained two confirmations, and reasonably felt the verification was progressing, but the confirmations were empty, and the feeling of progress came from work that carried no information. Worse, selecting the easy pairs is a natural thing to do, which is why the error recurs.

The lesson for conducting a verification. Identify in advance which checks could come out either way, and do those. Report the full list of what was checked, so a reader can see whether the informative cases were among them. A verification that names its scope can be audited; one that reports only its conclusion cannot.

(a) How much freedom the typing condition leaves. Fix an object map. For an arrow $n:P\to Q$ of $\mathcal{C}$, the typing condition requires $H(n):H(P)\to H(Q)$, so the available images are exactly the arrows of $\mathcal{D}$ from $H(P)$ to $H(Q)$. Counting those in $\mathcal{D}$: | from → to | arrows available |
|---|---|
| $X\to X$ | 1 (namely ${\mathrm{id}}_X$) |
| $Y\to Y$ | 1 (namely ${\mathrm{id}}_Y$) |
| $X\to Y$ | 1 (namely $h$) |
| $Y\to X$ | 0 | Every hom-set of $\mathcal{D}$ has at most one arrow. So once the object map is chosen, the typing condition does not merely constrain each image. It determines it, whenever an image exists at all. (b) The construction cannot succeed, and here is why. Suppose $H$ satisfies the typing condition, and let $(g,f)$ be any composable pair, $f:A\to B$ and $g:B\to C$. Then: - $H(g\circ f)$ is an arrow $H(A)\to H(C)$, by the typing condition applied to $g\circ f$;
- $H(g)\circ H(f)$ is a composite $H(A)\to H(B)\to H(C)$, hence also an arrow $H(A)\to H(C)$. Both sides therefore lie in the same hom-set of $\mathcal{D}$, and every hom-set of $\mathcal{D}$ has at most one element. Two arrows in a set of size at most one are equal. So

necessarily, for every composable pair, for every typed $H$ whatever. The composition law cannot fail in this $\mathcal{D}$. ∎ The requested construction is impossible, and the impossibility is the answer. Note what it depends on: not on $\mathcal{C}$, and not on the object map chosen, but only on $\mathcal{D}$ being thin, having at most one arrow between any two objects. Any thin category as codomain forces every typed mapping that respects identities to be a functor. (This is the same fact met in the order-theory setting: a partial order is a thin category, which is why a monotone map between two orders is automatically a functor and needs no separate composition check.) What a failing example requires. A codomain with two distinct parallel arrows. Take ${\mathcal{D}}^{\prime }$ with objects $X$, $Y$ and two arrows $h_1,h_2:X\to Y$ alongside the identities. Setting $H(A)=X$, $H(B)=X$, $H(C)=Y$, $H(f)={\mathrm{id}}_X$, $H(g)=h_1$, $H(gf)=h_2$ satisfies the typing condition and the identity law, and gives

A genuine failure, and it needed the extra arrow. (c) Which assignment must change. The image of the composite, $H(gf)$. The assignments to $f$ and to $g$ jointly determine what $H(gf)$ is required to be, namely $H(g)\circ H(f)$, which is fully computed from them. $H(gf)$ is the only one of the three free to disagree with the others, so it is the only one whose value the law constrains given the rest. That said, "must change" describes the logic, not the diagnosis. A failure is an inconsistency among three choices, and repairing it means deciding which choice was the mistake. The composite may be right and one of the parts wrong. What the law tells you is that they cannot all three stand; which to revise is a question about what the mapping was meant to do.

(a) The structure. Each schema representation is a category: objects are schema states, arrows are migrations, composition is applying migrations in sequence, and the identity arrow at a schema state is the null migration. Composition is associative because applying migrations in sequence is, and the null migration is a genuine identity, so the axioms hold. The translation $T$ is a candidate functor between these two categories. In the team's terms: - The identity law says $T$ sends the null migration to the null migration, translating "do nothing" yields "do nothing".
- The composition law says $T(m_2\circ m_1)=T(m_2)\circ T(m_1)$, translating a combined migration gives the same result as translating the parts and applying them in sequence. Their working assumption is the composition law. It is not an incidental convenience they happen to rely on; it is the substantive requirement, stated in their own vocabulary. (b) What the evidence establishes. Every table having an image is the object map. Foreign keys mapping to foreign keys with matching endpoints is the typing condition. Together these establish that $T$ is a well-formed candidate: the composite $T(m_2)\circ T(m_1)$ is a defined migration, so the law can be stated. They establish nothing about whether it holds. This is exactly the failure mode of the mapping $G$ in the worked example: a sound object map, correct endpoints on every arrow, and still not a functor, because $G(g\circ f)={\mathrm{id}}_Y$ while $G(g)\circ G(f)=h$. The team's checks are of precisely the kind that cannot detect that discrepancy. Each examines one assignment at a time, while the composition law constrains three jointly. (c) The check. For every composable pair $(m_1,m_2)$, compute $T(m_2\circ m_1)$ and $T(m_2)\circ T(m_1)$ and compare the resulting target schema states. Separately, check $T(\text{null})=\text{null}$ at every schema state. The quantification is the point: composable pairs, not a sample. One failing pair refutes the claim; a passing sample leaves it undecided, because nothing propagates agreement from a checked pair to an unchecked one. Two practical qualifications. Pairs in which one migration is the null migration are satisfied automatically once the identity law holds and should not be counted as evidence. They are the analogue of the identity pairs that made the flawed verification in the diagnosis exercise look productive. And if the pairs are too numerous to enumerate, the claim must be established by an argument over how $T$ is constructed, not by testing; the report should say which was done, since "we tested it" and "we proved it" support different confidences. (d) The production failure. If the law fails, a sequence of migrations and the corresponding combined migration produce different target schemas. Concretely: a database migrated incrementally ends in a different state from one migrated in a single step; or replaying the migration history from scratch disagrees with the schema currently deployed; or two environments that applied the same migrations in different groupings diverge. It resists diagnosis for four reasons. Each individual migration passes every check the team performs, so no migration looks suspect. The divergence appears only on paths that combine migrations in a particular way, and the triggering grouping may be one no test exercises. Nothing raises an error at the time. The inconsistency is silent, surfacing later as data that does not match the schema anyone believes is deployed. And the natural response, re-examining the migrations individually, looks in the only place the defect is guaranteed not to be. (e) The normalise claim is naturality. Let $F$ be the identity functor on the source category and let $T$ be the translation, both taking schema states to schema states and migrations to migrations. normalise supplies, for each schema state $S$, an arrow ${\nu }_S$. The rewrite of $S$ into canonical form. A family of arrows indexed by objects, one per object, relating two functors: that is a natural transformation, and the commuting claim is its naturality condition. The equation. For every migration $m:S_1\to S_2$,

reading: translate then normalise equals normalise then translate. (Stated for whichever pair of functors the team actually means; the shape is the same.) What it quantifies over: migrations, not schema states. This is the part teams get wrong, because normalise is defined per schema state, so it is natural to check it per schema state. The condition is indexed by arrows. A family can behave correctly at every schema state taken alone and still fail the square for some migration, that is precisely the situation the condition exists to detect, and checking only the states would miss it. Telling a real verification from an empty one. Ask whether the check could have failed. If $T$ or the surrounding functors act trivially on migrations, mapping every migration to a null migration, say, then both routes collapse to $\nu$ alone, the migration $m$ drops out of both sides, and the squares commute whatever normalise does. Agreement then reports the shape of the example, not a property of normalise. The same happens if the team tests only on schema states where normalisation is already a no-op: $\nu =\mathrm{id}$ makes both routes $T(m)$ identically. A genuine check uses migrations that normalise actually interacts with, ones that touch the structures canonicalisation rewrites, so the order could matter. The diagnostic question is whether some migration in the test set would have exposed a difference had one existed. If none would, the verification has confirmed the procedure and established nothing about the claim, and the report should say so rather than recording a pass. Their assumption is load-bearing: it licenses the inference that two deployment paths agree, and real deployments rest on it. A claim that something is structure-preserving is worth exactly as much as the check behind it, and the checks they performed are the ones that cannot fail on a mapping of this kind.