How to understand a principal bundle in Homotopy Type Theory In yang-Mills Theory, the interacting field is captured by a principal bundle $P$. In particular, let G the group which is homeomorphic to the fibers which it preserves upon acting on them. For fibers $P(x)$ and $P(y)$ of $P$ and $g$ an element of $G$ that acts on them, it is $p(x)g=p(y)$, hence $p(x)\sim p(y)$.
I want to translate the above in HoTT. I assume that there is a path $\gamma$ between x and y and in HoTT, this means that there is an identity type $\gamma: x=_U y$. One firstly notices that the interactive field  is expressed by the dependent type function $\varepsilon:\prod_{(x: U)} P(x)$ for some space $U$. Although the elements $p(x):P(x)$ and $p(y):P(y)$ belong to distinct types and therefore, an identity relation between them is not defined, a morphism which is an equivalence relation can be established between them, namely, there exists a function $ f: P(x) \rightarrow P(y)$.
Topologically, the function type can be treated by a path lifting in a fibration where $U$ constitutes the base space, $P(x)$ is the fiber over x and $\sum_{(x:U)} P(x)$ is the total space, where in logic this is translated as the existence of such a space of fibers. Lifting a path to the total space, it means that there is an identity type $lift: (x, p(x))=(y, f(p(x))$ in the total space. So there is no identity relation $p(x)=p(y)$ although there is an identity type $x=_Uy$.
Now, when G acts on the fibers, I suspect this means that there is a function $g: p(x) \rightarrow p(y)$ or there is an identity type $lift: (x, p(x))=(y, g(p(x))$. On the other hand, with regard to the automorphism group, for $p(x), q(x):P(x)$, there is an identity type in the total space $\sum_{(x:U_i)} P(x)$ so that $g, g': p(x)=_{P(x)}q(x)$.
My question is where exactly I am making the mistake in the above and in particular, I am not sure that $(x, p(x))=(y, g(p(x))$ when g acts on the fibers, rather just as I presented the automorphism case, it may be that $g$ is a morphism/path in an identity relation (between p(x) and p(y) (???)).
I hope I did not make any mistake on notations.
 A: One could try to emulate naively the usual definition. Namely, you could require a (continuous) action from your structure (topological) group $G$ on your total space $\sum_{x:B}P(x)$, namely a term $\phi$ of type 
$$\sum_{x:B}P(x) \times G \rightarrow \sum_{x:B}P(x)$$
, or its curryfication, ie a term of type 
$$\sum_{x:B}P(x) \rightarrow (G \rightarrow \sum_{x:B}P(x))$$
, satisfying the axioms of an action. You should also require the action to be free and transitive.
Finally, the action should preserve the fibers. With this last condition you should be careful. Indeed, you might require for all elements $x$ of $B$, $y$ of $P(x)$ and $g$ of $G$ an element of the identity type $pr1 (\phi((x,y),g)) =_{B} x$, where $pr1$ denotes the first projection out of the total space. But this identity type is a higher groupoid! Hence, in order to circumvent this you might require your base type $B$ to be a set, ie a type of hlevel 2, in this case the identity type above would be a (mere) proposition. You might also want to require that $P$ is a family of sets, ie for all $x$ of $B$ the type $P(x)$ should be a set, in this case you would be able to prove that your total space is a set.
This being said, it is probably not the right approach and I mentioned this naive one to show where some problems may arise if you mimic the usual definition without care. 
It might make more sense in the context of Homotopy Type Theory to follow the definition of principal bundles in terms of homotopy pullbacks.   
