Leibniz Abstraction, Structure Identity and Univalence

In mathematics, one gets used to thinking of a particular mathematical object - say a group, or a graph, or a partial order, or a field, or a topological space in abstract terms. That is, given the model $(X,R_1,\dots )$ one "forgets" the specific nature of the carrier set $X$, and one focuses only on properties of the mathematical model/structure, which are invariant under isomorphism. This means that one is, in a sense, thinking of some "entity" which all isomorphic copies "have in common".

So, for example, if our models $G_1=(V_1,E_1)$ and $G_2=(V_2,E_2)$ are isomorphic graphs, then one imagines that there is some other thingy -- call it $\widehat{G_1}$ -- such that ${\hat{G}}_1={\hat{G}}_2$. Obviously, the carrier sets $V_1$ and $V_2$ can be distinct. But this is "abstracted away". If our models are isomorphic partial orders ${\mathbb{P}}_1=(X_1,{⪯}_1)$ and ${\mathbb{P}}_2=(X_2,{⪯}_2)$, then we imagine that there are corresponding "abstract structures" ${\hat{\mathbb{P}}}_1$ and ${\hat{\mathbb{P}}}_2$ such that ${\hat{\mathbb{P}}}_1={\hat{\mathbb{P}}}_2$.

More generally, we imagine we have some map,

$\mathcal{A}\mapsto \hat{\mathcal{A}}$

taking us from graphs, orderings, groups, linear spaces, topological spaces, etc., etc., to abstract graphs, orderings, groups, linear spaces, etc., etc. such that

${\hat{\mathcal{A}}}_1={\hat{\mathcal{A}}}_2$ iff ${\mathcal{A}}_1\cong {\mathcal{A}}_2$.

holds. I call this principle Leibniz Abstraction. But, unfortunately, no one knows that these abstract "thingies" $\hat{\mathcal{A}}$ are ... But whatever they are, they are not models, with a carrier set. Their carrier set has been abstracted away, somehow.

Vladimir Voevodsky's Univalence Axiom, as I understand, is an attempt to make this very intuitive idea mathematically precise. There are many formulations, including in the book on Homotopy Type Theory, of course. Here is a formulation from Ulrik Buchholtz, from a 2013 talk on "Univalent Foundations and the Structure Identity Principle":

Univalence Axiom (Voevodsky)
For types $A$ and $B$, the identity type $I{d}_U(A,B)$ is equivalent to the type $Eq(A,B)$ of (homotopy) equivalences between $A$ and $B$.

(I think that the "Structure Identity Principle" amounts to what I call "Leibniz Abstraction" above; certainly, this is what has been discussed a lot by philosophers of mathematics for decades. Particularly structuralist philosophers of mathematics, like Shapiro, Hellman and Resnik.)

Now I'm fairly sure that this overlaps very closely with the following: one can define "thingies" ${\hat{\mathrm{\Phi }}}_{\mathcal{A}}$ such that Leibniz Abstraction holds, for set-sized mathematical models $\mathcal{A},\mathcal{B}$ as follows:

Leibniz Abstraction
${\hat{\mathrm{\Phi }}}_{\mathcal{A}}={\hat{\mathrm{\Phi }}}_{\mathcal{B}}$ iff $\mathcal{A}\cong \mathcal{B}$.

These entities are propositional diagrams.

The rough idea is this: let $\mathcal{A}=(A,R_1,\dots )$ be some mathematical object, with a set-sized carrier set/domain $A$ (and special or distinguished relations $R_i$). $\mathcal{A}$ can be a graph, a group, etc.

One can define a purely logical formula ${\mathrm{\Phi }}_{\mathcal{A}}(\overrightarrow{X})$, in a language $\mathcal{L}(\mathcal{A})$, possibly infinitary, with free (second-order) variables amongst $\overrightarrow{X}$, such that categoricity holds:

$\mathcal{B}\models {\mathrm{\Phi }}_{\mathcal{A}}(\overrightarrow{X})$ iff $\mathcal{B}\cong \mathcal{A}$. 

Thus the formula ${\mathrm{\Phi }}_{\mathcal{A}}(\overrightarrow{X})$ defines the isomorphism type (groupoid) of $\mathcal{A}$. The formula ${\mathrm{\Phi }}_{\mathcal{A}}(\overrightarrow{X})$ is called the diagram formula for $\mathcal{A}$. It is called this by analogy with the notion of a diagram in model theory. The diagram of a model $\mathcal{A}$ is a kind of "picture" of all the basic relationships between elements of the model $\mathcal{A}$, obtained by introducing a constant $c_a$ to name each $a\in A$. But the diagram formula ${\mathrm{\Phi }}_{\mathcal{A}}(\overrightarrow{X})$ itself does not contain any constants labelling domain elements, Rather, these have been existentially quantified.

Then we let ${\hat{\mathrm{\Phi }}}_{\mathcal{A}}$ be the propositional function expressed by the diagram formua ${\mathrm{\Phi }}_{\mathcal{A}}(\overrightarrow{X})$. Then Leibniz Abstraction follows. So far as I can tell, this also implements the intuitive idea that Univalence is intended to implement too: namely, the Structure Identity Principle.