Just a naive question about univalent foundations. As far as I understand, we want to define our mathematical types like sets, groups, categories, etc. such that structurally identical objects are equal in the sense of internal equality.
But are we free to choose what kind of isomorphisms we are interested in? For example, can we define both, the type of categories with ismorphisms as equality, and the type of categories with equivalences as equality? Or the type of topological spaces with homotopy equivalences as equality, and the type of topological spaces with homeomorphisms as equality?
How would these differences actually look like in the definition?
Yes, you're free to define a category however you like, as long as it obeys the axioms of a category. The isomorphisms come from that. However, the type of objects of the category has its own identity type (as every type does) and this may not match if your morphisms don't preserve the structure inherent in the situtation.
For example, if we define a topological space as a set together with a collection of subsets etc., then an equality between two topological spaces will be an equality between the underlying sets and an equality between the collection of subsets (transporting as necessary using the equality between the sets).
Given that an equality between two sets is (corresponds to) a bijection by the univalence axiom and that a bijection induces a bijection between the collections of opens sets if and only if it's continuous and has a continuous inverse, this means that an equality is precisely the same as a homeomorphism. Homotopy equivalence can't correspond to equality since such equivalences don't induce a bijection on the underlying sets.
If we want the identity type to match the isomorphisms if they don't already, we can use the Rezk completion to produce a fully-faithful, surjective on objects embedding of any category into a univalent category.