Here is the classical Seifert-van Kampen theorem . How do we state it in homotopy type theory? It seems that this MathOverflow question is relevant.
Here is a way to state it: 1-truncation commutes with (homotopy) colimits.
We want to talk about fundamental groupoids because everybody knows that it’s better than fundamental groups. But there is a great way to define groupoids in HoTT : types of h-level 3. Moreover, taking the fundamental groupoid is the same thing as taking the truncation. Then of course we don’t want to talk about open subsets or strict colimits, so we talk about homotopy colimits.
The main problem in this statement is the definition of general homotopy colimits. We may want a notion of colimit very general where the diagram is any (infinity,1) category (or some kind of infinity-graph) and it’s not clear how to define this. But whatever we do, homotopy pushouts should be a special case of homotopy colimits, and given that the 2-sphere is the homotopy pushout of two points along a circle, van Kampen’s theorem proves that the 2-sphere is simply connected. Moreover, modulo technical issues it should not be that difficult to prove, because truncation is a left adjoint and left adjoints preserve colimits (the usual proof works, at least for pushouts).
Actually there is another issue, in order to get something more useful we probably need to prove that a pushout of connected 1-types corresponds to the usual amalgamated sum in the category of groups (something like that). I guess that once we have a definition of K(G,1) spaces this will just be something to check, I’m not sure how difficult it will be.