An equivalence of categories which looks like Voevodsky's Univalence Axiom Let $\mathcal{C}$ be a category. Consider the full subcategory $\mathrm{Isom}(\mathcal{C})$ of $\mathrm{Mor}(\mathcal{C})$ whose objects are isomorphisms $A \xrightarrow{\cong} B$. It has a full subcategory $\mathrm{Id}(\mathcal{C})$ whose objects are the identities $A \xrightarrow{\mathrm{id}_A} A$. Now I claim that the inclusion
$\mathrm{Id}(\mathcal{C}) \to \mathrm{Isom}(\mathcal{C})$
is an equivalence of categories. In fact, it is fully faithful by construction and it is essentially surjective since every isomorphism $A \to B$ is isomorphic to $A \xrightarrow{\mathrm{id}_A} A$ in $\mathrm{Isom}(\mathcal{C})$. (Of course, we could as well also write down a pseudo-inverse functor.)
I have used this equivalence of categories a lot, often without really thinking about it.
Is there any (formal) connection between this equivalence of categories and Voevodsky's Univalence Axiom in Homotopy Type Theory? The latter roughly states that the canonical map
$\mathrm{Id}(A,B) \to \mathrm{Equiv}(A,B)$
is an equivalence for types $A,B$.
 A: First things first: your observation is essentially the fact that $\mathbf{Iso}(\mathcal{C})$ is a path object for $\mathcal{C}$. More precisely, observe that for any category $\mathcal{C}$, we have a factorisation
$$\mathcal{C} \to \mathbf{Iso}(\mathcal{C}) \to \mathcal{C} \times \mathcal{C}$$
of the diagonal functor $\Delta : \mathcal{C} \to \mathcal{C} \times \mathcal{C}$ where $\mathbf{Iso}(\mathcal{C}) \to \mathcal{C} \times \mathcal{C}$ is an isofibration and $\mathcal{C} \to \mathbf{Iso}(\mathcal{C})$ is an injective-on-objects equivalence, so we indeed have a path object in the sense of model categories. In particular, the fibres of $\mathbf{Iso}(\mathcal{C}) \to \mathcal{C} \times \mathcal{C}$ parametrise paths between "points" (i.e. objects) in $\mathcal{C}$, as one expects.
On the other hand, the univalence axiom says that there is a classifying space for types in which the space of paths between any two points is canonically equivalent to the space of equivalences between the corresponding types. There is an obvious generalisation of this if we replace "type" with "object in a category", and that leads to Rezk's notion of completeness. 
Thus, in order to make a connection between $\mathbf{Iso}(\mathcal{C})$ and univalence, we need a notion of classifying space for objects in $\mathcal{C}$. There are several candidates:


*

*The set $\operatorname{ob} \mathcal{C}$.

*The nerve of $\operatorname{iso} \mathcal{C}$, the maximal subgroupoid of $\mathcal{C}$.

*The nerve of $\mathcal{C}$ itself.


Obviously, $\operatorname{ob} \mathcal{C}$ will not work in general. Less obviously, the nerve of $\mathcal{C}$ also does not work in general. But the nerve of $\operatorname{iso} \mathcal{C}$ does have the required property, more or less by definition.
Somehow, the above is not very interesting, because we constructed the classifying space so that the "univalence" axiom is satisfied. It is much more interesting to think about the general situation where the classifying space is "built-in". 
Let $\mathcal{S}$ be a nice category of "spaces", e.g. simplicial sets, or even groupoids. A precategory or Segal object in $\mathcal{S}$ is a simplicial object $X_{\bullet}$ satisfying the Segal condition:


*

*For all $n \ge 2$, the canonical morphism
$$X_n \to \mathrm{ho}{\varprojlim} \left( X_0 \leftarrow X_1 \rightarrow X_0 \leftarrow \cdots \rightarrow X_0 \leftarrow X_1 \rightarrow X_0 \right)$$
is a weak equivalence in $\mathcal{S}$.


In the case where $X_0$ is discrete, we can replace $\mathrm{ho}{\varprojlim}$ with $\varprojlim$. There is a notion of equivalence of precategories, but these do not have to induce weak equivalences of the $0$-th spaces – so in some sense, the $0$-th space is underdetermined. 
There is a notion of equivalence in a precategory $X_{\bullet}$, and this determines a subspace $X_\mathrm{eq} \subseteq X_1$ consisting of those connected components whose points are equivalences. Of course, the degeneracy operator $X_0 \to X_1$ factors through $X_\mathrm{eq}$. A category or complete Segal object in $\mathcal{S}$ is a precategory $X_{\bullet}$ that satisfies Rezk's completeness axiom:


*

*The canonical morphism $X_0 \to X_\mathrm{eq}$ is a weak equivalence in $\mathcal{S}$.


Rezk-completeness has the following pleasant consequence: a morphism of categories is an equivalence of precategories if and only if it is a degreewise weak equivalence. Moreover, as the name suggests, every precategory admits a Rezk completion, i.e. is equivalent to a category.
Finally, we can tie this back to univalence: the univalence axiom can be interpreted as saying that the precategory of types is Rezk-complete. This is quite convenient, because Rezk-completeness is preserved by many constructions.
Addendum. Remarkably, the definition of Rezk-complete categories in $\mathbf{Grpd}$ was already more-or-less present in [Hofmann and Streicher, The groupoid interpretation of type theory, §5.5], all the way back in 1996! By comparison, [Rezk, A model for the homotopy theory of homotopy theory] appeared on arXiv only in 1998.
