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.

• The choice of the letter B to denote your base type/space might be a better choice than U to avoid a possible confusion in this context with a universe in your type theory. – Anthony Bordg Jun 6 '17 at 21:36

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.

• I am afraid I am new and I need more assistance. Why should I want to circumvent the construction of higher groupoids (in any case HoTT offers that and I assumed a topological space and the construction of infinite-categories) and move towards mere propositions. Moreover, what is the benefit of employing pullbacks? I suspect higher groupoids are constructed in the case of pullbacks as well. – Vicky Jun 7 '17 at 16:22
• In HoTT what one might want to formalize is the notion of an $\infty$-principal bundle. I believe (you should check, I'm not familiar with this notion) the notion of an $\infty$-principal bundle uses homotopy pullbacks. In this case even if higher groupoids show up it would not be problem since you will use the appropriate definition in this context. It may be still possible to formalize the notion of a mere principal bundle, but it would probably make sense only if one works with topological spaces, namely sets (ie types of hlevel 2) equipped with a topology. – Anthony Bordg Jun 7 '17 at 18:01
• Indeed, as explained in my answer if one would not require the base type to be a set, then the identity type used to express that the group action preserves the fibers could be a higher groupoid. This last fact means in particular that there might be many different elements in this identity type, ie some of them might be homotopic, some might not be. Thus, it is unreasonable to require randomly an element of this identity type. – Anthony Bordg Jun 7 '17 at 18:39