I have just read Grayson's introduction on homotopy type theory as a possible foundation for mathematics. It is very enlightening about what all the fuss is about, but I am left with some doubts. Forgive my naiveté, I am not expert in type theory at all.

When one uses ZFC as a foundation for mathematics, one evenutally moves to doing informal reasoning, knowing that it is always possible, although slightly tedious, to formalize all arguments. I am not sure about how to perform this step in HTT.

Let me take the example of Grayson, who shows how to define a group in HTT. First, he defines

- a type $P$ is a proposition iff it has at most one element (that is, the type $\prod_{p : P} \prod_{q : P} p = q$ is inhabited) - which, if existent, is called a proof of $P$
- a type $S$ ia a set iff for all $s: S$ and $t: S$ the type $s = t$ is a proposition

Then a group is a tuple $(G, e, i, m, \alpha, \lambda, \rho, \lambda', \rho', \iota)$ where

- $G$ is a type
- $e: G$, $i: G \to G$, $m: G \times G \to G$
- $\alpha$ is a proof of the identity stating associativity, and so on for $\lambda, \rho, \lambda', \rho'$ which prove left and right identity of $e$ and existence of left and right inverses
- $\iota$ is a proof that $G$ is a set (according to Grayson, it is a theorem that this fact is itself a proposition)

So far, so good: I am inclined to believe that with a little ingenuity one can in fact define most (all?) usual concepts in mathematics.

Now, I would like to go on proving theorems about groups. The simplest non-trivial theorem I can think of is Lagrange theorem: if $G$ is a finite group and $H < G$ a subgroup, then $|H|$ divides $|G|$. The intuitive proof is very short: for every coset $C$ of $H$ and any $c \in C$, multiplication by $c$ is a bijection $H \to C$, and $G$ is partitioned into cosets.

It is clear to me how to formalize this in ZFC, but I would be lost trying to do that in HTT. I have two kind of doubts:

1) Do all steps work as well? It seems to me that one uses the notion of subset. Is there such a notion in HTT? I guess there are no subtypes, so it would seem no subsets as well. I guess that one can define a subgroup as a triple $(H, f, p)$ where $H$ is a group, $f \colon H \to G$ and $p$ is a proof that $f$ is injective. But eventually we are doing something like "counting elements" - is this justified?

2) Even logic has changed into this new setting: proof are themselves objects of this mathematical universe. I guess I need to have something like a constructive proof to make this work out? Does it matter that I have to choose arbitrary elements $c \in C$ to find a bijection?

Sorry for the vague question: I am trying to understand what it would be like to do mathematics knowning in the back of your head that one can formalize thing into HTT, and it is not obvious to a beginner like me