A sketch for the proof of formal\conceptual duality in category theory From what I understand, the language of category theory consists of:

*

*a set of of $0$-ary functions $a,b,f,g,\dots$;

*three unary functions, $\operatorname{dom},\operatorname{cod}$ and $\operatorname{id}$, and a binary function $\circ$;

*a binary predicate  $=$.

The axioms should be the following, where $x,y,z$ are variables as usual:

*

*$\operatorname{dom}(y\circ x)=\operatorname{dom}(x)\land \operatorname{cod}(y\circ x)=\operatorname{cod}(y)$;

*$\operatorname{id}(x)\circ y=y\land \ y\circ \operatorname{id}(x)=y$;

*$((z\circ y)\circ x)=(z\circ( y\circ x))$.

An interpretation $\mathcal I$ of the theory relies on two  (disjoint) sets  $\mathbf A_0,\mathbf A_1$. Some $0$-ary functions are interpreted as elements of $\mathbf A_0$, others as elements of $\mathbf A_1$; $\mathcal I(\operatorname{dom}),\mathcal I(\operatorname{cod})$ are maps $\mathbf  A_1\to \mathbf A_0$, $\mathcal I(\operatorname{id})$ is a map $\mathbf A_0\to \mathbf A_1$, and $\mathcal I(\circ):\mathbf A_1\times_{\mathbf A_0} \mathbf A_1\to  \mathbf A_1$. Finally $\mathcal  I(=)$  is the subset of  $(\mathbf A_0\cup \mathbf A_1)^2$ consisting of pairs of  equal elements. The only problem that I  see is that, fixed an interpretation $\mathcal I$, $\mathcal I(t)$   is not well defined for any term $t$ (I'm assuming that all terms  are grounded,  i.e. not containing variables): that's why I  didn't put the quantifiers  before  the  axioms, since they must  be true only replacing the variables  with terms whose interpretation is well  defined. It  wouldn't seem a big issue to me, as one usually says, for example,  that if $g\circ f$ is the identity then $g$ is a retraction,  without really specifying that $f,g$ are composable arrows.
An interpretation $\mathcal I$ in $\mathbf A_0,\mathbf A_1$ yields an interpretation $\mathcal I^{op}$, again in $\mathbf A_0,\mathbf A_1$, as follows:

*

*$\mathcal I^{op}$ and $\mathcal I$ coincide on the $0$-ary functions;

*$\mathcal I^{op}(\operatorname {dom}):=\mathcal I(\operatorname{cod}),\ \mathcal I^{op}(\operatorname {cod}):=\mathcal I(\operatorname{dom})$;

*$\mathcal I^{op}(\operatorname{id}):=\mathcal I(\operatorname{id})$;

*$\mathcal I^{op}(\circ)$ can be obtained from these diagrams: $\require{AMScd}$ $$\begin{CD}
\mathbf A_1\times_{\mathbf A_0} \mathbf A_1@>p_1>> \mathbf A_1\\
 @Vp_2VV @VV\mathcal I(\operatorname{dom})V \\
\mathbf A_1@>>{\mathcal I(\operatorname{cod})}> \mathbf A_0
\end{CD}$$ $$\begin{CD}
\mathbf A_1\bar \times_{\mathbf A_0} \mathbf A_1@>q_1>> \mathbf A_1\\
 @Vq_2VV @VV\mathcal I^{op}(\operatorname{dom})=\mathcal I(\operatorname{\operatorname{cod}})V \\
\mathbf A_1@>>{\mathcal I^{op}(\operatorname{cod})=I(\operatorname{dom})}> \mathbf A_0
\end{CD}$$ $$\begin{CD}
\mathbf A_1\bar \times_{\mathbf A_0} \mathbf A_1@>q_2>> \mathbf A_1\\
 @Vq_1VV @VV{\mathcal I(\operatorname{dom})}V \\
\mathbf A_1@>>\mathcal I(\operatorname{\operatorname{cod}})> \mathbf A_0
\end{CD}$$ The first two  are cartesian squares, so the commutativity of the third one induces a map $\sigma:\mathbf A_1\bar \times_{\mathbf A_0} \mathbf A_1\to\mathbf A_1 \times_{\mathbf A_0} \mathbf A_1$, and $\mathcal I^{op}(\circ)$ is $\mathcal I(\circ)$ precomposed with $\sigma$. Briefly, $\mathcal I^{op}(\circ)(a,a'):=\mathcal  I(\circ)(a',a)$, for all $a,a'\in \mathbf A_1$ such that $\operatorname{dom}(a)=\operatorname{cod}(a')$.

Any term $t$ yields a term $t^{op}$, obtained by replacing $\operatorname{dom}$ with $\operatorname{cod}$ and viceversa, and by replacing $g\circ f$ with $f\circ g$ for every pair of (sub)terms $f,g$. Thus also a statement $S$ (a formula not containing variables) yields a statement $S^{op}$.
Semantical duality. If, for a statement $S$ and an interpretation $\mathcal I$ in $\mathbf A_0,\mathbf A_1$, $\mathcal  I(S)$ is true, then $\mathcal I^{op}(S^{op})$ is true.

Since, for two statements $P,Q$, $(P\land Q)^{op}$ coincides with $P^{op}\land Q^{op}$, and similarly for the other connectives, it suffices to  show that $\mathcal  I(t_1)=\mathcal  I(t_2)$ implies that $\mathcal  I^{op}(t_1^{op})=\mathcal  I^{op}(t_2^{op})$ on two  terms $t_1,t_2$:  this holds because  $\mathcal  I(t_1)=\mathcal  I^{op}(t_1^{op})$, and so the same for $t_2$. In fact, since $\mathcal  I$ and $\mathcal  I^{op}$ coincide  on $0$-ary functions, one can proceed  by induction: $$\mathcal  I(\operatorname{dom}(t))=\mathcal  I(\operatorname{dom})(\mathcal I(t))=\mathcal I^{op}(\operatorname{cod})(\mathcal I(t))=\mathcal I^{op}(\operatorname{cod})(\mathcal I^{op}(t^{op}))=\mathcal I^{op}(\operatorname{cod}(t^{op}))=\mathcal I^{op}(t_1^{op})$$  if $t_1=\operatorname{dom}(t)$, for a term $t$; a similar argument holds if $t_1=\operatorname{cod}(t)$, while if $t_1=s\circ t$: $$\mathcal I(s\circ t)=\mathcal I (\circ)(\mathcal I(s), \mathcal I(t))=\mathcal I^{op}(\circ)(\mathcal I(t),\mathcal I(s))=\mathcal I^{op}(\circ)(\mathcal I^{op}(t^{op}),\mathcal I^{op}(s^{op}))=\mathcal I^{op}(t^{op}\circ s^{op}).$$ In general, this  proves also  that if $\mathcal  I(t)$ is well defined, then $\mathcal I^{op}(t^{op})$ is too.

It follows that, if $S$ is true for any interpretation, in which is well defined, the same holds for $S^{op}$: if $\mathcal  I(S^{op})$ is  well defined, $\mathcal I^{op}(S)$ is  well defined,  so true by hypothesis; then $\mathcal  I(S^{op})$ is true.
Syntactic duality. If in some propositional calculus one can prove a statement $S$ by the axioms, then one can prove also $S^{op}$.

Expliciting the terms occurring in a statement,  as $S=S(t_1,\dots,t_n)$, one has $S^{op}=S(t_1^{op},\dots,t_n^{op})$; so  it is  evident that,  if one can infer $S$ from another statement $T$,  applying the  same rules one can infer $S^{op}$ from $T^{op}$. Since all the axioms are self-dual, if one can prove $S$ from them, can also prove $S^{op}$.

What do  you think about these arguments? I feel  like the boundaries  between formality and "inconsistency" are subtle in this department,  so I'd like to know if what I wrote actually makes  sense. Thanks in advance.
 A: I have not seen an explict formulation such as yours before and I have not had time to scrutinize it (its also unclear whether or not I have the expertise to do so!) but I have a few things to say that may be helpful. They do not fit in the comments so I will have to give them as an "answer". However, I hope someone more knowledgeable than I comes along"
It is legitimate to have two collections of $0$-ary functions, one collection $O$ representing your objects and the other $A$ representing your arrows. These are called multi-sorted theories, and they are equivalent to a one sorted theory. So choose what ever is easiest to work with. Now, I'm a bit rusty on the details, but a multi sorted theory with two sorts $X$ and $Y$ is equivalent to a theory with one sort $X\sqcup Y$, provided we add two predicates $P_x$ and $P_y$ so that $P_x(a)$ if, and only if, $a$ is an $X$.
In the standard definition of a category, you will see the author specify a collection of objects and a collection of arrows. Thus I think a multi-sorted theory is important here. So I think you will want a collection $O$ and a collection $A$, of $0$-ary functions.
On your point that the interpretation $I$ may not be well defined: I'm not sure this is true. Since $\circ$ is defined only on $A_1\times_{A_0}A_1$, $f\circ g$ is not a term unless $(f,g)\in A_1\times_{A_0}A_1$.
Also, I'll include a screenshot of Awodey's explanation of duality. I think it will be helpful. His approach can be shown rigourously by induction on the length of proof and induction on formula

A: Echoing, I think, @IsAdisplayName, I'm not really sure quite what is supposed to be gained by the rather unnecessarily heavy-handed presentation of the basic ideas that are more snappily there in e.g. Awodey's presentation, or others. Indeed, the ideas are even more briskly -- but I hope still sufficiently -- spelt out in my notes Beginning Category Theory §6.2 (downloadable from https://www.logicmatters.net/categories).
Overdoing the techie apparatus, as always, can run the danger of obscuring rather than clarifying underlying simple concepts/results. A good moral is: sufficient unto the day is the formalisation thereof!
