Practical example in using (homotopy) type theory
The answers and comments on this question show that there is still a ton of misinformation out there about HoTT.
The short answer (but much more time-consuming for you) is that you should read the HoTT Book, which was explicitly written to address this sort of question. To address the specific questions you asked, and the points raised in the other answers:
HoTT is not a structural set theory. Nor is it a material set theory; it is a type theory, a different kind of beast altogether. For an explanation of the differences, see this blog post of mine.
There absolutely is a notion of subset type (or subtype). The rules for subset types are explained in that blog post. Subsets of a type $A$ are usually encoded as their characteristic functions $P:A \to \rm Prop$. Given such a subset, one can always take its $\Sigma$-type $\sum_{x:A} P(x)$ which is a type with an injective function to $A$, but often it's easier and better to work directly with subsets than with such things. Of course, when you want a subset of a group to be itself a group, you'll need to consider it as a type in its own right, and you might find it easier to formulate Lagrange's theorem in terms of an arbitrary injective group homomorphism.
Constructive logic is a red herring if what you're wondering about is what mathematics looks like in HoTT versus in ZFC. It's true that HoTT is "by default" constructive due to its inheritance from type theory, but one can simply add the axioms of excluded middle and choice to obtain a mathematics that looks just like classical mathematics in most respects. (If you do want to be constructive, then as others have pointed out you have to be careful about the meaning of "finite" -- but this would also be true if you were trying to use a constructive set theory like IZF, and is irrelevant to doing mathematics in HoTT+LEM+AC.)
I think your question isn’t really about type theory or homotopy type theory, but instead about constructive mathematics. You’d have similar issues in dealing with picking representatives for an equivalence relation if you were working in a constructive version of ZF. There’s a bit of an art to working constructively. In this case, I suspect that what you need to think about is making sure you’re using the right notion of finite set. (Some notions of finite that agree nonconstructively might not agree constructively.)
HoTT differs from ZFC in several aspects and it is useful to separate them:
ZFC is a material set theory while HoTT is a structural one. This means that we cannot ask whether one set belongs to another (that is, there is not predicate $\in$). This implies that the notion of a subset also does not make sense. Subsets of a set $X$ must be replaced with (equivalence classes) of injective maps into $X$ (as you suggested). This is not a big problem in practice, it is just a different style of working with sets. If you want to learn more about differences between these approaches to set theory, Michael Shulman, Comparing material and structural set theories is a very nice source.
HoTT is constructive by default, but this does not mean that you cannot use classical logic. Actually, you can simply add the law of excluded middle and the axiom of choice to HoTT if you want to. The resulting theory will be consistent and very close to ZFC.
The basic objects of ZFC are sets while the basic objects of HoTT are homotopy types. If you are not interested in homotopy theory, you can simply ignore types which are not sets. The only problem is that the universe of sets (and groups, and so on) is not a set. This issue is not a big problem in practice since usually you do not need to talk about equality between sets (and the only difference between sets and types is that the equality between elements of a type is not a proposition, so it does not really work like ordinary equality).