> You'll see why it's useful to have a formal justification for treating isomorphic objects as equal (this is called "univalence"), which is something you may have even been doing informally/subconsciously all along.

Would you be able to discuss how this compares to quotienting? It sounds similar, but I assume has very important differences. I have, very formally, been doing quotienting. I identify an equivalence relation, quotient it, prove that the properties and operations of interest are well-defined when lifted to the equivalence classes, and then work exclusively at the level of the equivalence classes and the lifted operations. Say, when I work exclusively with reals, which are equivalence classes of Cauchy sequences, or with cosets in group theory.