Today, I learnt about the relation between inner product space and normed space which parallelogram law holds. Then I had wondered about something like this:
Let $A$, $B$ are 2 types of structures.
Let $(X,f)$ be an instance of $A$. It's known (1) $\lambda\overset{def}{=}P(f)$ ($P$ is kind of functor) can induce structure $B$ on $X$, i.e $(X,\lambda)$ is an instance of $B$. Moreover, by referring to properties related to $A$ only, one can derive the formula (2) $f=Q(\lambda)$.
Let $(Y,\mu)$ be an instance of $B$. It's also known that the formula (3) $g\overset{def}{=}Q(\mu)$ can induce structure $A$ on $Y$, i.e $(Y,g)$ is an instance of $A$. Moreover, by referring to properties related to $B$ only, one can derive the formula (4) $\mu=P(g)$.
Then, one can obtain:
$f\overset{P}{\rightarrow}\lambda\overset{Q}{\rightarrow}Q(\lambda)=f$, equality by formulas (2) and (3).
$\mu\overset{Q}{\rightarrow}g\overset{P}{\rightarrow}P(g)=\mu$, equality by formulas (1) and (4).
Is there a term for such (type of) "mutual definition"? Or can we simply say that $A$ is identical with $B$?
