  Category theory unifies mathematical concepts, aiding comparisons across
structures by incorporating objects and morphisms, which capture their
interactions. It has influenced areas of computer science such as automata
theory, functional programming, and semantics. Certain objects naturally
exhibit two classes of morphisms, leading to the concept of a double category,
which has found applications in computing science (e.g., ornaments, profunctor
optics, denotational semantics).
  The emergence of diverse categorical structures motivated a unified framework
for category theory. However, unlike other mathematical objects, classification
of categorical structures faces challenges due to various relevant
equivalences. This poses significant challenges when pursuing the formalization
of categories and restricts the applicability of powerful techniques, such as
transport along equivalences. This work contends that univalent foundations
offers a suitable framework for classifying different categorical structures
based on desired notions of equivalences, and remedy the challenges when
formalizing categories. The richer notion of equality in univalent foundations
makes the equivalence of a categorical structure an inherent part of its
structure.
  We concretely apply this analysis to double categorical structures. We
characterize and formalize various definitions in Coq UniMath, including
(pseudo) double categories and double bicategories, up to chosen equivalences.
We also establish univalence principles, making chosen equivalences part of the
double categorical structure, analyzing strict double setcategories (invariant
under isomorphisms), pseudo double setcategories (invariant under
isomorphisms), univalent pseudo double categories (invariant under vertical
equivalences) and univalent double bicategories (invariant under gregarious
equivalences).
