This is came from when I'm formalizing lemma 1.3.11 of Basic Category Theory, I miss a precondition ( $H$ below must be a natural transformation in the lemma) and try to prove an impossible thing.

Let $F, G : \mathcal{C} \to \mathcal{D}$ be functors, and a family

H : (X : C) \mapsto F X \cong G X

Does $H$ must be natural?

Counterexample. [math-000T]

2025-06-18

The result is $H$ can be not natural.

This counterexample is given by Zhixuan Yang:

Let $\mathcal{C}$ be the two-object one-arrow category, and $\mathcal{D}$ be $Set$ , and

F, G : 0 \to 1 \mapsto 2 \xrightarrow{id} 2

where $2$ is the two elements set. For $0$ we choice $H(0) = id$ and $H(1) = \text{not}$ , then $H$ is not natural.