domain: shs.hisphilso phys math

text:
Gabriel Catren

ON GAUGE SYMMETRIES, INDISCERNIBILITIES, AND GROUPOID-THEORETICAL EQUALITIES

Keywords: Principle of Identity of Indiscernibles, Homotopy Type Theory, Gauge Theories, Connections, Fiber Bundles

We shall analyze the intrinsic geometric structure of Yang-Mills theory from the standpoint provided by (what we shall call) the homotopic paradigm. This mathematical paradigm was mainly developed in the framework of (higher) category theory and homotopy type theory and relies on a groupoid-theoretical understanding of equality statements of the form a = b. From a philosophical perspective, we shall argue that the homotopic paradigm relies a) on a rejection of Leibniz's Principle of the Identity of Indiscernibles and b) on a constructivist understanding of propositions as types of proofs. We shall apply the homotopic reconceptualization of equalities to the equalities between the base points and the fibers of the fiber bundle associated to a Yang-Mills theory. We shall revisit in this framework the articulation (heuristically established in the framework of the so-called gauge argument) between gauge symmetries and the mathematical notion of connection. We shall argue that this homotopic-theoretic understanding of Yang-Mills theories paves the way toward an ontological interpretation of gauge symmetries, that is an interpretation according to which gauge symmetries-far from being nothing but a "surplus structure" resulting from a descriptive redundancy-rely on the intrinsic geometric structures of Yang-Mills theories.

Introduction

The understanding of the empirical and/or ontological status of gauge symmetries is probably the main philosophical problem posited by the gauge theories of the fundamental interactions. [START_REF] Adams | Primitive Thisness and Primitive Identity[END_REF] According to (what we shall call) the epistemic interpretations of gauge symmetries, the latter would be nothing but a mere mechanism by means of which we can get rid of the "surplus structure" [?] or descriptive redundancy associated with the different possible re-coordinatizations of a unique physical (i.e. coordinate-independent) state of affairs. The main argument that grounds this epistemic stance is that a physical state of affairs can be completely described by means of gauge invariant quantities (such as for instance the so-called Dirac observables, i.e. the functions on the reduced phase space obtained by "quotienting out" the gauge symmetries [?, ?]). The idea that gauge symmetries have per se no physical content arose for the first time in the context of the Kretschmann's objection against the physical scope of the principle of general covariance in general relativity [?, ?, ?]. The kernel of Kretschmann's objection is [START_REF] Adams | Primitive Thisness and Primitive Identity[END_REF] In this article we shall mainly address gauge theories of the Yang-Mills type (like electromagnetic theory) [?].

Hence, we shall understand by gauge symmetries the local symmetries of Yang-Mills theories, that is the elements in the group G of vertical automorphisms of a G-principal fiber bundle (called gauge group). These elements are also called active gauge transformations and should be distinguished from the passive gauge transformations that encode the gluing conditions between the different local charts of a fiber bundle atlas (see for instance [?, Ch.5] and Section N • ?? of this article for more details).

that pre-relativistic theories like Newtonian gravity can also be recasted in generally covariant terms. This seems to imply that the general covariance of general relativity is nothing but a mere formal feature (that is, an artifact of the chosen formulation) with no physical content. [START_REF] Aharonov | Significance of Electromagnetic Potentials in the Quantum Theory[END_REF] Purely epistemic interpretations of gauge symmetries were endorsed by some of the main actors in the history of gauge theories, like for instance Dirac. [START_REF] Alexander | The Leibniz-Clarke Correspondence, Together with Extracts from Newton's Principia and Opticks[END_REF] Now, the epistemic interpretation of gauge symmetries as mere descriptive redundancy is at odds with the fact that gauge symmetries do have theoretical and (direct or indirect) physical significance. [START_REF] Ambrose | A Theorem on Holonomy[END_REF] In particular, we shall here address one of the arguments used to highlight the physical status of gauge symmetries, namely the so-called gauge argument. Briefly, the gauge argument is a heuristic argument that shows that a Lagrangian with a global symmetry can be forced to be locally invariant by introducing gauge fields [?, ?, ?, ?, ?, ?, ?]. In Yang's succinct terms, "symmetry dictates interaction" [?]. In this way, the notion of local gauge invariance seems to be intertwined with a notion endowed with a clear physical status, the notion of fundamental physical interaction. The conceptual challenge posited by the gauge argument was clearly stated by Redhead in the following terms "[...] how can symmetry under a mere choice of conventional representation dictate any genuinely physical principle at all? " [?, p.503] From a mathematical standpoint, an important hallmark in the history of gauge theories is the realization of the fact that the gauge fields that encode the fundamental physical interactions can be mathematically described as connections on fiber bundles [?, ?]. We shall here pay particular attention to the fact that in his seminal article on the subject [?], Ehresmann introduced (in the wake of Cartan) connections on general fiber bundles alongside with groupoid-theoretical considerations about the equalities between different fibers (see also [?]). Ehresmann "was one of the founders of the theory of fiber bundles, independently of Whitney and Steenrod' ' [?, p.36] and the first to use groupoids in differential geometry (in the form of the so-called structure groupoid or gauge groupoid associated to a fiber bundle, which was introduced in his paper on connections on fiber bundles [?]). From the standpoint that we shall adopt here, we consider this relation between the theory of groupoids and the theory of connections on fiber bundles particularly interesting since it establishes a bridge between gauge theories and the conceptual and formal developments associated to what we shall call the homotopic paradigm in contemporary mathematics.

From a philosophical perspective, we shall argue that the homotopic paradigm engages two important ideas, namely [START_REF] Aharonov | Significance of Electromagnetic Potentials in the Quantum Theory[END_REF] For a discussion about the distinction between merely formal or artificial general covariance (like the one exhibited by pre-relativistic theories when properly formulated) and substantial general covariance see [?, ?, ?, ?]. For a generalization of Kretschmann's objection to general gauge theories see [?]. [START_REF] Alexander | The Leibniz-Clarke Correspondence, Together with Extracts from Newton's Principia and Opticks[END_REF] In his Lectures on quantum mechanics, Dirac writes "We have arbitrary functions of the time occurring in the general solution of the equations of motion with given initial conditions. These arbitrary functions of time must mean that we are using a mathematical framework containing arbitrary features, for example, a coordinate systems which we can choose in some arbitrary way, or the gauge in electrodynamics. As a result of this arbitrariness in the mathematical framework, the dynamical variables at future times are not completely determined by the initial dynamical variables, and this shows itself up through the arbitrary functions appearing in the general solution" [?, p.17]. More recently, Witten writes that "gauge symmetries are redundancies in the mathematical description of a physical system rather than properties of the system itself " [?]. [START_REF] Ambrose | A Theorem on Holonomy[END_REF] In contemporary philosophy of physics, the (direct or indirect) empirical significance of gauge symmetries was discussed by Brading and Brown [?], Friederich [?], Greaves and Wallace [?], Healey [?, ?], Kosso [?], and Teh [?] among others.

(1) a rejection of Leibniz's Principle of the Identity of Indiscernibles (PII in what follows) (Section N • ??) (2) a constructivist understanding of propositions as types of proofs (Section N • ??).

First, the homotopic paradigm extends the strict notion of equality (according to which the terms a and b in an equality a = b denote the same entity) to encompass equalities between numerically different and qualitatively equivalent entities. [START_REF] Anderson | Principles of relativity physics[END_REF] In what follows, this extended (or weakened in category-theoretic terms) notion of equality will be simply called equality. Second, the definition of propositions as types of proofs (which is explicit in the version provided by homotopy type theory) implies that an equality a = b has to be understood as the type of the concrete equivalences between a and b [?, ?] (e.g. paths for the equalities between points in a space, isomorphisms in category theory). The main new ingredient of the resulting understanding of equalities as equality types is that the possible existence of many equivalences between a and b is not understood as a dispensable proof-theoretic redundancy, but rather as an intrinsic homotopic structure (Section N • ??). Now, the notion of a multiplicity of objects related by possibly multiple equivalences is mathematically encoded in the categorical notion of groupoid (a category in which all morphisms are isomorphisms). This explains the entanglement between the notion of groupoid and the geometric notion of homotopy exploited in the framework of homotopy type theory. In the first part of this article (Sections N • ?? and ??), we shall propose a conceptual presentation of the main ideas of the homotopic paradigm that will be later relevant for the analysis of Yang-Mills theories. We shall argue against the validity of the PII in mathematics and revisit from a critical standpoint the attempts to save the PII by introducing weaker or relative "grades of discriminability" (Quine). We shall finally summarize the homotopic conception of equalities by proposing a new principle-the principle of equality types of indiscernibles-intended to occupy the place left vacant by the PII. [START_REF] Anel | The Geometry of Ambiguity. An Introduction to the Ideas of Derived Geometry[END_REF] In the second part of this article (Sections N • ??, ??, and ??), we shall revisit the geometric underpinnings of Yang-Mills theories in light of these homotopic ideas. We shall stress that the notion of G-bundle used in the mathematical description of Yang-Mills theories (being a numerical multiplicity of indiscernible copies S x of a symmetric standard fiber S) provides a paradigmatic example of a situation in which equality types are relevant. We shall argue that the thesis according to which gauge symmetries are nothing but a "surplus structure" associated to a descriptive redundancy is a particular instance of the thesis (sublated in the framework of the homotopic paradigm) according to which the structure of equivalences that prove an equality [START_REF] Anderson | Principles of relativity physics[END_REF] In what follows, the expressions strict equality (often used in mathematics) and numerical identity (used in philosophy in the context of discussions about Leibniz's principle) will be used as synonymous expressions. [START_REF] Anel | The Geometry of Ambiguity. An Introduction to the Ideas of Derived Geometry[END_REF] A comprehensive historical and philosophical analysis of the notions of individuality, distinguishability, and identity in physics from formal standpoints other than homotopy theory can be found in [?]. In particular, quasi-set theory (mainly developed by Krause, see for instance [?] and [?] for more philosophical discussions) was proposed as an alternative to set theory that allows to treat collections of "absolutely" indiscernible entities.

According to the arguments that we are proposing here, the homotopic paradigm can also be understood as a sublation of set theory intended to deal with absolute indiscernibilities. However, we claim that standard mathematical objects like Euclidean space are already composed of absolutely indiscernible entities (its points). On the contrary, Krause argues that "classical mathematics" only admits indiscernible elements with respect to "structures" with non-trivial automorphisms that can always be extended to rigid structures with absolutely discernible elements. According to Krause (following conjectures by Schrödinger [?, pp. 121-122], Post [?] and Manin [?, p.36]), it is only with quantum mechanics that the necessity to deal with absolute indiscernibilities becomes critical.

is a dispensable "surplus structure" associated to a proof-theoretical redundancy. To do so, we shall provide an ontological-oriented reading of the notion of gauge symmetry by stressing that the epistemic freedom to choose reference frames stems from the intrinsic geometric structures of the objects at stake (Section N • ??). We shall then propose an analysis of the different forms of equality types that arise in this geometric framework (Section N • ??). This analysis will naturally lead us towards the functorial definition of an Ehresmann connection (Section N • ??). By using this definition, we shall argue that an Ehresmann connection can be understood as the supplementary geometric structure that allows us to understand the fibers S x as internal structures of the points of the spacetime manifold M (which plays the role of the base space of the G-bundle) in a manner that is compatible with the identity types of both x and S x . Finally, we shall use the fact that G-valued holonomies define invariant observables to argue in favor of the indirect empirical significance of gauge symmetries. Mathematical physicists like Baez, Schreiber and collaborators have explored the relation between gauge theories and the homotopic paradigm, mainly in the direction of extending gauge theories to higher gauge theories [?, ?]. The relation between gauge theories and the homotopic paradigm has also been addressed from a more philosophical perspective by Catren [?], Dougherty [?, ?], Guay [?], Guay and Hepburn [?], and Ladyman and Presnell [?]. This article is an attempt to contribute to this new and promising approach to the foundations of gauge theories.

From Strict Equalities to Equalities Between Numerically Different Terms

The homotopic paradigm is a far-reaching refoundation of mathematics that has been mainly developed in the framework of (higher) category theory [?, ?] and, more recently, homotopy type theory [?] and derived geometry [?]. We shall not delve here into the mathematics of the homotopic paradigm, but rather try to focus on what we consider to be its main philosophical foundations (see also [?, ?, ?, ?, ?, ?]). We shall develop here and in the next section the thesis according to which the homotopic paradigm embodies two central ideas, namely:

(1) a plain rejection of Leibniz's PII, (2) a constructive understanding of propositions as types of proofs.

In this section, we shall consider the first point. Conceptually, the PII states that two numerically different entities cannot be qualitatively identical or indiscernibles, i.e. that they cannot have the same qualitative properties. In short, differences "solo numero" are not possible (see [?] and references therein). By using a second-order quantifier on some class of properties, the PII can be formulated by means of the expression

∀P (P a ⇔ P b) ⇒ (a = b).
The validity of this principe depends on the range of the second-order quantifier. If we include for instance the so-called haecceitas (i.e. the property x = a of being identical with a given entity a), then the PII becomes trivially true. [START_REF] Arntzenius | Space, Time, and Stuff[END_REF] According to the strongest non-trivial version of the principle, the range of the quantifier is given by the qualitative properties, i.e. the predicates with one free variable. Two entities are said to be qualitatively different or intrinsically discernible if at least one such predicate is true of one of the entities but not of the other. Qualitative properties define the so-called absolute discernibility [?, p.230] or strong discriminability [?]. Confronted [START_REF] Arntzenius | Space, Time, and Stuff[END_REF] If a and b share all properties, then we can deduce from a = a (which is trivially true) that a = b. Hence, the PII is trivially satisfied.

to the existence of mathematical structures including numerical multiplicities of indiscernible elements (e.g. points in a homogenous space), some philosophers have tried to preserve the validity of the PII by relaxing (in the wake of Quine's "grades of discriminability" [?, ?]) the properties being considered from qualitative properties to

• predicates with two free variables that are fulfilled by the two objects in only one order (relative discernibility) [?, p.211]8 • and two-place irreflexive predicates (weak discernibility) (see also [?, ?, ?]) [START_REF] Awodey | Category Theory[END_REF] .

These attempts to preserve at least some weakened form of the PII witness for a certain resistance to simply accept at face value the existence of numerical multiplicities of indiscernible entities in mathematics (see notably the debates around Keränen's "identity problem for realist structuralism" [?, ?, ?, ?] and Wüthrich's translation of Keränen's problem to spacetime physics [?, ?]). The rejection of the PII has been characterized as an "esoteric" possibility [?, p.328] based on the consideration of "metaphysical and physics-transcending" properties [?]. To counterbalance this resistance towards the possibility of rejecting the PII, it is worth noting here that Leibniz himself maintained that the PII-while being valid for metaphysical substances-is not valid in mathematics. Whereas substances are defined-according to Leibniz-by complete notions, mathematical entities are incomplete notions that result from operations of abstraction. The important point is that incomplete notions can have instantiations which are "perfectly similar " (see for instance [?, p.32]). In fact, we could say that the conclusion of the aforementioned debate concerning the "identity problem for realist structuralism" is that we have to accept-in the wake of Leibniz-the existence of differences solo numero in mathematics [?, ?, ?].

But let us analyze more carefully if we should accept with Leibniz the fact that the PII is not valid in mathematics or if we should try to force the validity of the PII by introducing subtler grades of discriminability. In order to address this question, let us consider the relation that the PII entertains with the problem of individuation, that is with the problem of deciding what confers individuality upon entities. The PII implies (at least in Leibniz's original version) that qualitative properties provide a sufficient criterion to individuate entities, i.e. there is no further individuation beyond the individuation provided by such properties. Accepting the validity of the PII seems to entail a commitment to an ontology according to which entities are nothing but bundles of properties without any underlying "substantial" support (like in Russell [?, Chapt.V] and Ayer [?]). This means that in order to individuate an entity we can (at least in principle) get rid of ante-predicative indexical signs and just give the complete list of its properties. [START_REF] Awodey | Structuralism, Invariance, and Univalence[END_REF] Let us revisit the example of the points in a homogenous space under this light. Such points are not endowed with different qualities by means of which we could intrinsically discern them. But they can be weakly discerned by predicates of the form "x is d miles apart from y". However, can one individualize a point in a homogeneous space by means of such relational predicates? The answer is no. If a person A chooses a point a of the space by pointing at it with their finger, there is no means to explain to another person that has closed their eyes what point has been selected by A. The specification of the distances between a and other points does not solve the problem since these other points cannot be individualized either. One can of course fix a coordinate system to individuate the points, but such a choice is arbitrary and there is no way to specify in a purely descriptive (non-indexical) manner which coordinate system has been chosen. The irreflexivity of a two-place predicate of the form "x is d miles apart from y" just witnesses for the fact that a homogeneous space is indeed a numerical multiplicity of points, i.e. that one is dealing with many points. Such predicates do not confer a qualitative individuation to the points, but just attest that the entities are numerically different. Heathcote has recently pointed out that Black had already rejected the possibility of saving the PII by using the notion of (what was later called) weak discernibility [?]. Arguing against the defender of the PII (called A in Black's paper [?]), Blacks claims that weak discernibility does not serve to distinguish one sphere from the other. It is worth here quoting Black's paper at lenght "A. [...] Each of the spheres will surely differ from the other in being at some distance from that other one, but at no distance from itself -that is to say, it will bear at least one relation to itself -being at no distance from, or being in the same place as -that it does not bear to the other. And this will serve to distinguish it from the other. B. Not at all. Each will have the relational characteristic being at a distance of two miles, say, from the centre of a sphere one mile in diameter, etc. And each will have the relational characteristic (if you want to call it that) of being in the same place as itself. The two are alike in this respect as in all others. A. But look here. Each sphere occupies a different place; and this at least will distinguish them from one another. B. [...] To say the spheres are 'in different places' is just to say that there is a distance between the two spheres ; and we have already seen that will not serve to distinguish them. [...] your assertion that the spheres occupied different places said nothing at all, unless you were drawing attention to the necessary truth that different physical objects must be in different places. [...] to say that the spheres occupy different places is to say no more than they are two spheres." [?, p.75] As Black's clearly argues, weak discernibility only restates the fact that there are two spheres. Heathcote concludes that "[...] for even in a weak sense there is no discerning going on. Weak countability might have been a more accurate name." [?]. [START_REF] Awodey | A Proposition is the (Homotopy) Type of its Proofs[END_REF] The case of a homogeneous space (which could be understood as a continuous field of infinitely small spheres) is analogous in the sense that weak discernibility only restates the fact that we are dealing with a numerical multiplicity of indiscernible entities. We can thus conclude that the weak notion of discernibility used to separate points in a homogenous space does not provide purely descriptive "intrinsic denominations" [?, p.214] by means of which one could avoid using indexical signs or demonstratives. [START_REF] Awodey | A Proposition is the (Homotopy) Type of its Proofs[END_REF] The fact that weak discernibility only attests for the numerical difference between the corresponding entities has also been pointed out by van Fraassen and Peschard in the following terms: "The condition of weak discernibility certainly entails distinctness. But first, such a predicate as 'is one metre from some other point but not from itself' also applies to all points, and so does not express a difference between them. [...] What Saunders, following Quine, effectively pointed out is a condition which entails that there is more than one entity of the given kind, without implying that there are specifiable differences that distinguish them." [?, p.19].

The impossibility of completely getting rid of indexical signs-and the concomitant impossibility to completely reduce thisness to suchness [?]-has been stressed by Weyl in the following terms: "A conceptual fixation of points by labels [...] that would enable one to reconstruct any point when it has been lost, is here possible only in relation to a coordinate system, or frame of reference, that has to be exhibited by an individual demonstrative act. The objectification, by elimination of the ego and its immediate life of intuition, does not fully succeed, and the coordinate system remains as the necessary residue of the ego extinction" [?, p.75] To sum up, the theses that we are endorsing here are a) that mathematics cannot get rid of indiscernible entities and b) that the homotopic paradigm is the furthest development up to now of this emancipation of mathematics from the grips of the PII. Rather than trying to avoid the supposedly "esoteric" or "metaphysical" indiscernibilities by introducing relative or weak grades of discriminability, mathematics has moved forward by accepting the existence of indiscernibles at face value and by constructing new mathematical tools capable of formalizing the very structure of these indiscernibilities. The groundbreaking step was made with the invention of the notion of group by the French mathematician E. Galois in the beginning of the XIX century. We could say that the homotopic paradigm-by grounding mathematics on the generalization of the notion of group given by groupoids (rather than on sets)-is the most recent development of Galois' attempt to invent a mathematical "theory of ambiguity" (as Galois himself dubbed it [?, p.94]) or (we would rather say) a mathematical theory of indiscernibles.

The rejection of the PII opens new possibilities for the understanding of equality statements of the form a = b. Propositions of this general form are in a sense paradoxical, since they affirm an equality between terms a and b that are ostensibly different. One possible interpretation of equality statements that preserves the validity of the PII is the nominalistic interpretation endorsed by Frege (at least in the period of the Begriffsschrift [?, §8]) and Quine (see for instance [?, §35, p.208] and [?, p.107]). For both philosophers, a statement of the form a = b means that a and b are just different names that refer to the same entity. Now, if by contrast one no longer clings to the PII, then the use of the sign = can be expanded or weakened from strict or numerical equalities (where in the last instance any entity is only equal to itself) to equalities between two numerically different and qualitatively identical entities a and b (like two points in a homogeneous space or two isomorphic objects in a category). We could then say that the homotopic paradigm relies on an expansion of the equality relation from strict numerical identity to indiscernibility. An equality between numerically different and indiscernible entities will be simply called equality in what follows. 12 12 One could still try to interpret equalities as weaker equivalences encoding partial similarities between discernible objects. By doing so, one could introduce equalities between numerically different objects while preserving the validity of the PII. In fact, equivalence relations define particular cases of groupoids. Now, the fact the groupoids (and therefore equalities) can be used to encode partial similarities between discernible objects does not eliminate the fact that certain mathematical objects (e.g. homogeneous spaces) are composed of elements that are absolutely indiscernible, i.e. that were not obtained from discernible objects by means of an abstraction process (a complementary discussion of this point can be found in [?, Sect.N

• 3]).
It is worth addressing here a possible misunderstanding, namely that the idea according to which two indiscernible objects a and b are equal is a restatement (or an updating) of the PII. [START_REF] Ayer | The Identity of Indiscernibles[END_REF] This would be completely at odds with the thesis advocated here, namely that the homotopy paradigm relies on a rejection of the PII. However, this conflation between a) the PII and b) the expansion of the equality relation from strict or numerical equalities to equalities between numerically different indiscernible entities relies on a conflation between numerical and qualitative equality. According to the homotopic notion of equality, qualitative indiscernibility provides the correct notion of equality conveyed by the sign =. This means that the equality = might relate entities that are numerically different and qualitatively identical. Now, this homotopic notion of equality should be distinguished from the numerical equality appearing in Leibniz's principle. In other terms, indiscernible entities a and b are "equal" in the sense of being related by the homotopic equality =, but certainly not in the sense of being one and the same entity (numerical identity). This point has been explained (for the particular case of the univalence axiom in homotopy type theory) by Awodey in the following terms: "[...] this [the Univalence Axiom] is best thought of as expanding the notion of equality to that of equivalence, rather than collapsing that of equivalence to strict identity. That is to say, [the Univalence Axiom] does not say that all equivalent types are strictly the same." [?] In this context, the notion of numerical identity persists in the form of equalities of the form a = a, i.e. of equalities in which both terms are numerically the same. Equalities of this form might be literally non-trivial when we use different names to denote both sides of the equality. We can therefore have "equalities" between a and b where a and b are just different names of the same thing. We could say that the non-trivial scope of such "equalities" is merely meta-linguistic. In homotopy type theory, this meta-linguistic relation of synonymity is introduced in the form of the so-called judgmental or definition equality (denoted ≡ or = def ). [START_REF] Baez | Torsors Made Easy[END_REF] In turn, the expanded notion of equality between entities that might be numerically different is called propositional equality (and denoted =). Now, meta-linguistic equalities are always grounded on a numerical identity, i.e. on identities of the form a = a. In homotopy type theory, this is encoded by the fact that definitional equality a ≡ b implies propositional equality a = b. [START_REF] Baez | Categorification[END_REF] The important point [START_REF] Ayer | The Identity of Indiscernibles[END_REF] This is in fact what Baez claims in a post of the n-Category café blog about the univalence axiom in homotopy type theory. This axiom encodes the idea according to which the equality relation = for homotopy types is given by the qualitative indiscernibility defined by homotopy equivalences. Baez writes that the univalence axiom can be understood "as a sophisticated updating of Leibniz's Principle of the Identity of Indiscernibles." 15 If a ≡ b, we can freely substitute a by b. Since a = a is always true, we obtain the true proposition a = b. We have here used that the identity principle a = a is always true. In category theory every object a in a category C is endowed with a trivial self-identity ida. In homotopy type theory, the so-called introduction rule of the identity is that the reciprocal is not true: the fact that a = b (indiscernibility) does not imply a ≡ b (numerical identity), i.e. that a and b denote the same entity. This can be understood as a rephrasing of the fact that the PII does not hold in this framework.

The equality-as-indiscernibility interpretation of the notion of equality used in homotopy type theory has been criticized by Ladyman and Presnell in [?]. We shall not engage here in a detailed discussion of the arguments proposed in [?], but we shall make some preliminary comments. We shall informally understand the equality-as-indiscernibility interpretation of the groupoidtheoretical notion of equality as a mutual correspondence between the notion of propositional equality and the notion of indiscernibility. This means a) that equality should entail indiscernibility and b) that indiscernibility should entail equality. In homotopy type theory the indiscernibility of the equals is a consequence of the so-called path induction [?, Sect.1.12.1] (see [?] for justification of path induction on "pre-mathematical grounds") and plays the role of what is usually called Indiscernibility of Identicals (or Substitutivity of Identicals). Regarding the equality of the indiscernibles, we can consider the property "is in the same connected component of a". If two tokens a and b of the type A are indiscernible, they should in particular have this property in common. Therefore, a and b have to be in the same connected component of A. But by definition this means that a and b can be joined by a path, i.e. that they are equal in the homotopic sense of the term. Hence, indiscernibility implies equality. The property "is in the same connected component of a" is nothing but the homotopic version of the so-called haecceitas, i.e. of the property "is equal to a". Since this property makes the PII trivially valid, it is usually discarded from the quantification over predicates used to define the notion of indiscernibility. In particular, this is what is done by Ladyman and Presnell in [?]. However, the homotopic version of the property "is equal to a" encodes the non-trivial topological fact that b can be joined to a by means of a path. We could say that haecceitas are homotopically detrivialized. Moreover, we are not using this homotopic version of the property "is equal to a" to prove the PII. As we said before, the statement according to which indiscernibility implies (homotopic) equality cannot be understood as a restatement of the PII (as Ladyman and Presnell do in [?, Sect.6.6 & Appendix]). Ladyman and Presnell choose a formulation of the PII according to which the fact that two tokens a and b of a type A are "'exactly alike' (i.e. they have all their properties in common)" implies that the equal type Id A (a, b) is inhabited, i.e. that a and b are equal. However (as we have explained above), the equality at stake in the homotopic claim "indiscernibles are equal" does not refer to the numerical identity used in the formulation of Leibniz's principle, but rather to the fact that a and b can be related by equivalences. In this sense, the equality-asindiscernibility interpretation of the homotopic notion of equality does not entail a commitment to the PII, but rather encodes the fact that indiscernibles can be numerically different.

From Equalities to Equality Types

We have addressed in the previous section the transition from strict or numerical equalities (where the two terms related by the equality denote the same entity) to equalities between numerically different indiscernibles. The second important ingredient of the homotopic paradigm (which appears explicitly in the framework of intuitionistic type theory and homotopy type theory) is the constructivist principle (also known as Curry-Howard correspondence) according to type specifies that for every token a of a type A, there is a distinguished element (denoted ref la) of the identity type a = a corresponding to the trivial self-identity. which a proposition is the type of its proofs [?, ?, ?]. [START_REF] Baez | An Invitation to Higher Gauge Theory[END_REF] According to the usual classical conception of propositions, a proposition is a statement that is either true or false (such propositions are called mere propositions or truth values in homotopy type theory [?] and ideal propositions in the rest of this article). In this framework, a proof can be understood as a sort of epistemic surplus structure that becomes irrelevant once we know that a proposition is true. Like in the case of Wittgenstein's ladder, one is supposed to throw away the ladder after having climbed up it [?, 6.54, p.89]. Moreover, the possible existence of inequivalent proofs is understood as a mere proof-theoretic redundancy. By contrast, according to the constructivist definition used in intuitionistic type theory [?] and homotopy type theory [?], a proposition is a type whose tokens are the concrete proofs of the corresponding statement. We could say that the type is the abstract statement shared by all the concrete demonstrative presentations of the statement. Whereas ideal propositions make abstraction from the concrete proofs, the structure of (possibly multiple inequivalent) proofs is for the constructivists part of the propositional type itself. We could say in a Hegelian manner that-according to the constructivist stance-the result (the truth value) cannot be severed from the process (the proofs).

We could think in a first instance that the constructivist definition of propositions as types is just a philosophical reminder of the fact that mathematics is a concrete human practice in which there are no truths without proofs. [START_REF] Baez | Gauge Fields, Knots and Gravity[END_REF] However, the constructivist definition of a propositionfar from being just a meta-mathematical stance about mathematical activity-has far reaching intra-mathematical consequences. As we shall now see, severing the result (the statement being proved) from the process (the proofs) removes essential-homotopic-information. The key point is that a proposition might have multiple inequivalent proofs. Such a non-trivial structure of proofs-far from being a proof-theoretic redundancy-can be understood as the very internal structure of the proposition qua type of its proofs. In some cases, the truncation of the internal proof-theoretic structure of a proposition might even lead to pathologies requiring some form of regularization.

We shall now focus on a certain kind of propositions, namely propositions given by equalities of the form a = b. As any propositions, equalities can be treated either as ideal propositions or as types of proofs (we shall see examples of both possibilities below). An equality a = b understood as the type of its proofs will be called from now on an equality type. We shall consider in particular an example that will play a central role in the analysis of Yang-Mills theories that we shall propose in the next sections. Namely, what does it mean to say that two figures a and b in the Euclidean space are equal? Remarkably enough, the answer can already be found in Euclid's Elements. The Notion 4 of the Elements states: "Things which coincide with one another are equal to one another " [?, p.155]. This "axiom of congruence" conveys the idea according to which two geometric figures are equal if they can be superposed (see the commentary of this notion in [?, pp.224-231] and [?]). In other terms, the hypothetical equality between two figures can be (dis)proved by trying to superpose them by means of a concrete motion. [START_REF] Barrett | Holonomy and Path Structures in General Relativity and Yang-Mills Theory[END_REF] It is worth noting that and central to Brouwerian intuitionism, that the meaning of a proposition does not derive from an absolute standard of truth external to the mind, but resides rather in the evidence for its assertability in the form of a mental construction or proof. Thus the central thesis of the 'propositions-as-types' doctrine is that each proposition is to be identified with the type, set, or assemblage of its proofs" [?]. [START_REF] Barrett | Holonomy and Path Structures in General Relativity and Yang-Mills Theory[END_REF] This definition of geometric equality is commented by E. Cartan in the following terms: "If indeed one tries to clarify the notion of equality, which is introduced right at the beginning of Geometry, one is led to say that this understanding of the notion of equality already presupposes that the terms being equal are in general numerically different. [START_REF] Bell | Types, Sets and Categories[END_REF] This definition of geometric equality is explicitly constructive since it specifies what has to be done in order to prove an equality statement. In particular, we could say that every motion that transports one figure a on the top of the other figure b can be understood as a concrete proof of the fact that the proposition a = b is true. Likewise, two points a and b in a space M are qualitatively equal (albeit numerically different) if there is a path γ : a → b between them (i.e. a map γ : [0, 1] → M with γ(0) = a and γ(1) = b). In this way, each path γ between two points a and b in a space M can be interpreted as a concrete equivalence between a and b that provides a particular proof of the equality a = b. [START_REF] Belot | Understanding Electromagnetism[END_REF] The existence of such a path means that a and b are in the same connected component of the space M . If a and b were in different connected components of M , then the property of belonging to a certain connected component would define an individuating predicate that would distinguish any such point (which means that two points in different connected components are not only numerically different but also qualitatively different). In this way, the homotopic approach applied to the equalities between the points of a space amounts to

• preserving the numerical difference between qualitatively equal points (homotopic notion of equality), • encoding these qualitative equalities by means of multiple concrete equivalences given by paths between the points (equalities as types).

However, rather than clinging to this homotopic approach, we can alternatively truncate the equality types and come back to the classical regime of ideal equalities. We call truncation the operation by means of which a numerical multiplicity of equal objects (in our example, the points a in the same connected component of M ) is substituted with a single equivalence class [a] (this operation is called decategorification in [?]). [START_REF] Belot | Symmetry and Gauge Freedom[END_REF] From a conceptual standpoint, the truncation two figures are equal when one can go from one to the other by a specific geometric operation, called a motion" (quoted in [?, p.19]). [START_REF] Bell | Types, Sets and Categories[END_REF] By saying that "no two things can be more equal" than a pair of parallel lines [?], Recorde (the sixteenthcentury Welsh mathematician that invented the equals sign =) seems to suggest that there is no equality relation finer than the relation of indiscernibility between numerically different things. As Shulman noted in a post of the n-Category café blog, one might have thought "that a pair of parallel lines would obviously be more equal if they were the same line". [START_REF] Belot | Understanding Electromagnetism[END_REF] It is worth clarifying at this stage the relations between different terms introduced thus far, namely the terms token, proof, equivalence, isomorphism, automorphism (or symmetry), and path. The general term token denotes any instantiation or term of a type. In the particular case in which the type is a proposition, the tokens of the type are given by the proofs of the proposition. This notion of proof might seem vague but it acquires a precise definition in each concrete context. For instance, when the proposition is an equality a = b, the proofs of the proposition are given by the concrete equivalences between a and b. When the proposition is of the form a = a, the concrete self-equivalences of a are called identifications. Identifications are also called automorphisms or symmetries of a. In turn, the seemingly vague notion of equivalence takes different forms in different mathematical frameworks. In category theory, the concrete equivalences between two objects in a category are given by the isomorphisms between them. In the geometric semantic used in homotopy type theory, a type and its tokens are schematized by means of a space and the points of the space respectively. In this framework, the concrete equivalences between any two tokens of the type are given by the paths between the corresponding points. As we shall see, the equivalences between two paths with the same endpoints are given by the homotopies between the paths. If we truncate the structure of 2-equivalences between paths given by these homotopies, the equivalences between points are just given by homotopy classes of paths. [START_REF] Belot | Symmetry and Gauge Freedom[END_REF] According to Baez and Dolan's characterization of the decategorification of a category: "We 'decategorify' a category by forgetting about the morphisms and pretending that isomorphic objects are equal. We are left with operation combines two operations. By means of these operations it is possible to go back from equality types to equalities (idealization) and from equalities to identities (strictification). These two operations are the following:

• an idealization that forgets the multiple concrete equivalences between two equal objects (which yields a set of objects endowed with an equivalence relation encoding the ideal equalities), • a strictification of the equalities, which amounts to pass to the quotient defined by the equivalence relation. By doing so, each numerical multiplicity of equal objects is amalgamated into a numerically unique object, the equivalence class (thereby enforcing the PII). [START_REF] Black | The Identity of Indiscernibles[END_REF] In the geometric example of the points in a connected space, the truncation amounts to abstract away all the concrete equivalences between the points of M and only retain the equivalence classes of identical points. [START_REF] Brading | Are Gauge Symmetry Transformations Observable?[END_REF] The result of the truncation is a set of equivalence classes of identical points called 0-homotopy set and denoted π 0 (M ). The π 0 (M ) captures the 0-homotopy type of M and discards all the higher homotopic information about the space (a friendly introduction to homotopy types can be found in Given a set of entities we can inquire about the possible qualitative identities between some of them. We have considered in the previous paragraphs the qualitative identities between points in a space. We can now iterate the process and inquire about the possible equivalences in the set of equivalences/paths between two fixed points a and b in the same connected component. This requires to consider whether any two paths γ 1 , γ 2 : a → b with same endpoints are qualitatively identical or not, i.e. to evaluate the truth value of the "higher" equality γ 1 = γ 2 . In order to do so, we can apply once again Euclid's axiom of congruence to the geometric figures given by the paths themselves: two paths with the same endpoints are equal if there is a "motion" by means of which one of them can be transported to the other one. In this case, such a "motion" is given by a continuous deformation between the paths that preserves the endpoints. This kind of motion between paths is formalized by the notion of homotopy (see [?] for a historical analysis of a mere set: the set of isomorphism classes of objects. [...] Decategorification is a straightforward process which typically destroys information about the situation at hand." [?]. [START_REF] Black | The Identity of Indiscernibles[END_REF] The truncation operation can be understood as a projection of a groupoid to the underlying equivalence relation (idealization) followed by a quotient by the equivalence relation (strictification). In the case of the strictification operation, many objects are projected to the same object if they are indiscernible. This amounts to force the validity of the PII in tne sense that numerically different and indiscernible objects are amalgamated into a single object (the equivalence class). In the case of the idealization operation, many equivalences are projected to the same equivalence if they have the same source and target. Whether the equivalences are themselves indiscernible or not is completely irrelevant to define this projection. these topics). [START_REF] Cap | Parabolic Geometries I. Background and General Theory[END_REF] Homotopies can be understood as 2-equivalences between 1-equivalences (paths) between points and can be represented by diagrams of the form:

a b γ 1 γ 2 h
If the space M has holes that obstruct the existence of equivalences between certain paths, then such paths are not homotopic, i.e. they are not qualitatively equal. In this case, they provide inequivalent proofs of the corresponding equality a = b. Hence, two points a and b in the same connected component can be equal in different inequivalent manners if the space M is not simply connected. This description of the equalities between paths instantiates the homotopic notion of equality in the sense that (1) it preserves the numerical differences between indiscernible paths, (2) it relates them by concrete 2-equivalences given by homotopies (equalities as types).

But we could alternatively impose the classical regime of strict and ideal equalities at this higher level. This amounts to making abstraction from the 2-equivalences (idealization) and removing the numerical differences between qualitatively equal paths by only retaining the equivalence classes of homotopic paths (strictification). By means of this truncation, we obtain a quotient set of different equivalence classes [γ] of homotopic paths that define inequivalent proofs of the equality a = b. It is worth noting that in this case we have a sort of mixed approach: we have used equality types for the equalities between points but we have truncated the equality types for paths. This shows that the truncation is an operation that can be applied in a chirurgical manner only from a given level on.

By considering the set of points of M as objects and the equivalence classes [γ] of homotopic paths as morphisms we can define a category. [START_REF] Catren | Geometric Foundations of Classical Yang-Mills Theory[END_REF] It is worth noting that the consideration of homotopy classes of paths as morphisms (rather than the paths themselves) is required to define the category structure. If we just considered paths as morphisms, then the composition would not be associative. Indeed, (λγ)δ and λ(γδ) (where λ : c → d, γ : b → c, and δ : a → b are three composable maps), far from being strictly equal, differ by a smooth reparametrization. This lack of a strict associativity is no longer a problem if we consider homotopy classes of paths as morphisms. The paths (λγ)δ and λ(γδ) are homotopic paths, i.e. they define the same equivalence class [(λγ)δ] = [λ(γδ)]. Moreover, given a path γ : x → y, one can define the reverse path γ -1 .

= γ(1 -t) : y → x such that γ -1 • γ : x → x is homotopic to the identity. Hence, the [START_REF] Cap | Parabolic Geometries I. Background and General Theory[END_REF] More precisely, two paths γ 1 , γ 2 : a → b are homotopic if there exists a smooth map (called an homotopy)

h(s, t) : [0, 1] × [0, 1] → M
such that h(0, t) = γ 1 and h(1, t) = γ 2 (while the parameter s spans all the paths that interpolate between γ 1 and γ 2 , the parameter t runs along each path). [START_REF] Catren | Geometric Foundations of Classical Yang-Mills Theory[END_REF] The identities idx are given by the equivalence classes of paths homotopic to the constant paths γ(t) = x for all t ∈ [0, 1] (i.e. the contractible loops). The composition of morphisms [γ] and

[δ] satisfying δ(1) = γ(0) is given by the expression [γ] • [δ] . = [γ • δ],
where γ • δ denotes the concatenation of paths up to a suitable reparameterization. More precisely, if γ, λ : [0, 1] → M are two paths in M such that γ(1) = λ(0), then

λ • γ = γ(2t), if 0 t 1 2 . λ(2t -1), if 1 2 t 1. (1)
definition of inverses also requires to consider homotopy classes of paths as morphisms (rather than the paths themselves). It follows that all morphisms are reversible (where [γ] -1 = [γ -1 ]), that is isomorphisms. A category in which all morphisms are isomorphisms is called a groupoid.

Conceptually, groupoids provide the mathematical notion that formalizes the notion of equality types. Indeed, a groupoid is a multiplicity of objects where any two objects can be equal (in the sense of being indiscernible), and where such an equality can be concretely proved by multiple isomorphisms. A groupoid is generally depicted as a set of objects G 0 and set of morphisms G 1 related by the source and target maps s, t : G 1 ⇒ G 0 that send each morphism in G 1 to the corresponding source and target in G 0 . The existence of trivial identities id x , the reversibility of paths, and the partial composition can be understood as the categorical expressions of the reflexivity, the symmetry and the transitivity of the equality relation defined by the isomorphisms respectively. The notion of groupoid can be extended to higher groupoids by considering that the isomorphisms (or 1-equivalences) themselves might be related by 2-equivalences, which might be in turn related by 3-equivalences, and so on and so forth. By unfolding (or resolving) this structure of higher equivalences all the way up, we arrive to the notion of ∞-groupoid [?]. The hierarchy of objects, equivalences, 2-equivalences and so on, can be alternatively truncated at any level n by considering equivalence classes of n-equivalences rather than explicitly considering the n + 1-equivalences between them. This amounts to idealizing and strictifying equalities at the level n (and all the higher levels). [START_REF] Catren | Geometric Foundations of Cartan Gauge Gravity[END_REF] In particular, the 0-homotopy set π 0 (M ) of M was obtained by truncating the equality types between the points of M . Instead, one can keep the equality types between points and truncate the equalities between paths (by amalgamating homotopic paths into equivalence classes), thereby obtaining the fundamental groupoid Π 1 (M ) of M . In other terms, the fundamental groupoid Π 1 (M ) is the groupoid whose objects are the points of M and whose isomorphisms are the homotopy equivalence classes [γ] of paths with same endpoints [?, p.8]. The fundamental groupoid of M captures the 1-homotopy type of M and discards the higher homotopic information about M . By passing to the next level, one can use equality types for both points and paths. This requires to keep the numerical multiplicities of homotopic paths and explicitly consider the 2-equivalences between them. Classical (strict and ideal) equalities are now only applied at the level of the homotopies by defining the 2-equivalences as homotopy classes of homotopies between paths (which requires to introduce homotopies between homotopies or 3-equivalences). By doing so, we obtain the so-called fundamental 2-groupoid Π 2 (M ) of M , which encodes its 2-homotopy type (see for instance [?]). If we continue this process all the way up-i.e. if we unfold all this structure of higher equivalences without using classical equalities at any level-we obtain the fundamental ∞-groupoid Π ∞ (M ) of M (which encodes its full homotopy type). Whereas the whole homotopy type contains information about all the homotopy groups of the space, the n-homotopy type only encodes the homotopy groups π i (M ) for i n. This means that the imposition of strict and ideal equalities-far from merely removing proof-theoretic redundancies or epistemic surplus structure-truncates intrinsic topological information about the space M .

The truncation of this homotopic structure might lead to pathologies (e.g. "bad quotients" resulting from group actions with isotropies, problems to define smooth moduli spaces of algebraic varieties with automorphisms in algebraic geometry [?, ?], etc.). We could in fact understand important chapters of the homotopic paradigm (notably the theory of stacks in algebraic geometry) as attempts to regularize these pathologies by a) keeping the numerical multiplicities of indiscernible entities and b) by encoding these indiscernibilities by means of concrete equivalences. [START_REF] Catren | Klein-Weyl's Program and the Ontology of Gauge and Quantum Systems[END_REF] Table 1 summarizes the relation between the different homotopy groupoids and the treatment of the equalities between points, paths, homotopies, etc. (either as classical -strict and ideal-equalities or as equality types) at the different levels of the hierarchy. The point that we want to stress here is that whereas elements in a numerical multiplicity of indiscernible objects lack "intrinsic denominations" [?, p.214] or a well-determined "suchnesses" [?] given by individualizing properties, the numerical multiplicity itself might be highly structured (where this homotopic structure is encoded in the corresponding ∞-groupoid). In the terms of homotopy type theory, we would say that this structure characterizes the type of the indiscernible objects. In this way, the mathematical domestication of indiscernibilities has proceeded not by trying to break the indiscernibilities by means of weak or relative "grades of discriminability", but rather by introducing mathematical notions capable of encoding the very global structure of the numerical multiplicities of indiscernible objects. In this sense, the theory of ∞-groupoids can be understood as the ultimate development of the "theory of ambiguity" started by Galois. We could say that the stances that consider the "primitive thisness" [?] of indiscernibles as an esoteric or metaphysical notion that has to be eradicated at all costs remain to a large extent pre-Galoisian. [START_REF] Catren | Klein-Weyl's Program and the Ontology of Gauge and Quantum Systems[END_REF] An example of such pathologies is given by the "bad quotients" associated to group actions with non-trivial isotropies. Given a group action G × X → X on a space X we can either pass to the quotient set X/G of equivalence classes of elements related by the group action (this amounts to impose the PII) or preserve the numerical multiplicity of elements of X and explicitly consider the equivalences given by the group action (which defines the so-called action groupoid [?, p.7]). By construction, the action groupoid keeps track of the equivalences between the elements in a group orbit. By defining the quotient space as the stack presented by such an action groupoid, it is possible to avoid the problems associated to non-smooth quotient spaces defined by group actions with non-trivial isotropies (see for instance [?, ?] and references therein).

In Table 2, we describe the four combinations resulting from the two independent enrichments of the notion of equality that we have discussed (from strict or numerical equalities verifying the PII to equalities between numerically different and qualitatively equivalent entities [START_REF] Catren | Homotopic Identities and the Limits of the Interpretation of Gauge Symmetries as Descriptive Redundancy[END_REF] and from ideal equalities-i.e. equalities understood as ideal propositions-to equality types as types of equivalences). We have included in this table examples of the different combinations. [START_REF] Corfield | Modal Homotopy Type Theory[END_REF] While general groupoids provide the formal notion that combines the two enrichments of the notion of equality [START_REF] Catren | Homotopic Identities and the Limits of the Interpretation of Gauge Symmetries as Descriptive Redundancy[END_REF] In the categorical framework used in [?], what we have called strict or numerical equality and equality are called equality and isomorphism respectively. We prefer here to think of isomorphisms as an expanded notion of equality in order to converge with the use of these notions in homotopy type theory. Given two terms x, y of a type A, we can construct the equality type Eq A (x, y), i.e. the type of proofs that x = y. This notion of equality can be understood as an expansion of the classical strict equality. The strict equality is preserved in homotopy type theory since there is always a canonical proof of x = x associated to the trivial self-identity of x. The particular case of the expanded notion of equality given by the strict equality attests for the reflexivity of the expanded notion. As Shulman says in a post of the n-Category Café, "[...] in type theory, the 'identity types' are the only notion of sameness we have. (Well, there is 'definitional equality', but it doesn't serve all the same purposes, being a judgment rather than a proposition.) There is nothing stricter than homotopic/isomorphic/equivalent for which we need to reserve the word 'equality'. [...] Coming from a set-theoretic background, one naturally expects that in addition to a notion of 'isomorphism' between structures, there is also a notion of 'equality', but this is not the case in univalent foundations. [...] Separating 'isomorphism' from 'equality' linguistically seems to me to be liable to promote this confusion." [START_REF] Corfield | Modal Homotopy Type Theory[END_REF] It is worth noting that the transitions a) from strict to extended equalities and b) from ideal equalities to equality types are conceptually unrelated. The transition from strict to extended equalities can be understood as a rejection of the validity of the PII. In turn, the transition from ideal equalities to equality types is grounded on the constructivist understanding of propositions as types of proofs. The validity (or not) of the PII and the propositions-as-types correspondence are very different conceptual issues and (at least in principle) they are unrelated. In particular, the propositions-as-types correspondence concerns any kind of propositions (and not only equalities). In turn, a position with respect to the Leibnizian problem regarding the existence of difference solo numero does not entail any commitment with respect to the ideal/constructivist alternative. We can endorse the PII and still understand the identity a=a as an identity type of proofs (e.g. groups) and we can also reject the validity of the PII and still understand equalities of the form a=b as mere propositions (e.g. equivalence relations).

into the notion of equality type, the other three notions of equality are instantiated by particular cases of groupoids: groupoids with only identity morphisms for ideal strict equalities (sets), groupoids with at most one isomorphism between any two objects for ideal equalities (groupoids defined by equivalence relations), and groupoids without isomorphisms between numerically different objects for strict equality types (groupoids defined by groups or, more generally, skeletal groupoids). Whereas groups provide a paradigmatic example of the transition from ideal equalities to equality types, equivalence relations provide a paradigmatic example of the transition from strict equalities to equalities between numerically different indiscernible entities. In this sense, groupoids can be understood as a common generalization of groups and equivalence relations.

Let us consider this understanding of the notion of groupoid in more detail.

The so-called delooping groupoid BG defined by a group G-a groupoid with one object a and an automorphism a → a for each g ∈ G-instantiates the transition from ideal (strict) equalities to (strict) equality types, i.e. the case where no numerically different objects are equal (strictness), but where equality type a = a might admit many proofs given by the automorphisms or the symmetries of a. The example of groups provides maybe the most surprising philosophical consequence of the constructivist understanding of equalities as equality types of equivalences, namely the detrivialization of the identity principle a = a. Far from being a trivial proposition that would require no proof, the identity principle becomes an entity-dependent statement that might admit a non-trivial structure of proofs. [START_REF] Dirac | Lectures on Quantum Mechanics[END_REF] In turn, this example clarifies the relationship between the notion of symmetry and the ontological category of identity (where ontological makes reference to the thesis according to which, in Quine's terms, there is "no entity without identity" [?, p.23]). We could say that objects with symmetries have non-trivial identities, where this non-triviality results from their internal structure. But even structureless objects might have non-trivial identities. Indeed, the 1 st -homotopy group π 1 (M, x) of a space M based at x encodes the identity of the structureless point x. Indeed, each homotopy class of loops based at x provides a proof of the equality type x = x. This identity is purely external so to speak in the sense that it depends on the global topology of the space M .

On the other hand, the category defined by an equivalence relation instantiates the transition from strict equalities to equalities between indiscernibles, i.e. the case where numerically different objects might be isomorphic (i.e. equivalent) but where there are no multiple isomorphisms between objects. Briefly, whereas groups define groupoids BG with one single object but many automorphisms, equivalence relations define groupoids with multiple objects related (at most) by a single isomorphism between any two of them. Finally, general groupoids combine both groups and equivalence relations in the sense that a groupoid might have both multiple equivalences (like in groups) and multiple objects (like in equivalence relations) (for a description of groupoids as a generalization of both groups and equivalence relations see [?]).

In order to conclude this brief presentation of the main ideas of the homotopic paradigm, let us summarize the homotopic conception of equalities as equality types by means of the following principle, which is intended to replace of the PII: [START_REF] Dirac | Lectures on Quantum Mechanics[END_REF] It is worth noting that the identity principle continues to be necessarily true in the sense that (as we have mentioned before) there is always a canonical proof of a statement of the form a = a given by the trivial selfidentity (e.g. the identity morphisms in category theory, the constant paths in homotopy, the canonical proof of the reflexivity of equality in intensional type theory, etc.).

Principle of Equality Types of Indiscernibles: Rather than mistaking indiscernibility for numerical identity, expand and typify the notion of equality to encompass numerically different indiscernibles related by concrete equivalences.

On Gauge Symmetries

In the next sections we shall use the new conceptual tools provided by the homotopic paradigm to revisit the link (first established in the framework of the gauge argument) between gauge symmetries and gauge fields. As we have explained in the introduction, whereas the notion of gauge symmetry is usually presented as an epistemic notion, gauge fields describe fundamental physical interactions (with their undeniable empirical significance). In order to bridge the gap between the epistemic and ontological dimensions related by the gauge argument, we shall start by proposing a presentation of gauge symmetries that underlines their intrinsic geometric nature. To do so, we shall revisit the geometric structures underlying Yang-Mills theories, namely the theory of G-fiber bundles [?]. [START_REF] Dougherty | Sameness and Separability in Gauge Theories[END_REF] A G-bundle E π -→ M is a family of equal copies S x of a standard fiber S parameterized by the space(time) M , where S has symmetries encoded by the so-called structure group G (which means that S is endowed with a left G-action G × S → S 32 ) [?, Def.10.1, p.86]. In Leibnizian terms, a G-bundle E π -→ M is a numerical multiplicity of symmetric objects S x that are qualitatively indiscernible. Given an open covering {U i } of M , a G-bundle can be presented by means of a fiber bundle atlas

(U i , ψ i : π -1 (U i ) -→ U i × S)
defined by a family {ψ i } of local trivializations. The transition functions (also called passive gauge transformations)

ψ ij : U i ∩ U j → G (2)
that define the gluing between the different local charts (U i , ψ i ) of the fiber bundle atlas are defined by the expressions

ψ i • ψ -1 j : U j × S| Uij -→ U i × S| Uij (3) (x, s) → (x, ψ ij (x)s)
and satisfy the cocycle conditions ψ ii (x) = id G (for each x ∈ U i ) and ψ ij (x)ψ jk (x) = ψ ik (x) for each x ∈ U i ∩ U j ∩ U k (where the last conditions guarantee that the transition functions are compatible on the triple intersections). [START_REF] Dougherty | Sameness and Separability in Gauge Theories[END_REF] Yang-Mills theories can be analyzed in two interdependent levels. First, Yang-Mills theories are theories that describe dynamical connections on (associated and principal) fiber bundles over spacetime. The so-called gauge group G of local gauge transformations is the group of vertical automorphisms of the corresponding G-principal bundle (where G is the structure group of the bundle). Second, one can define the configuration space A of the theory as the space of such connections and apply the theory of constrained Hamiltonian systems developed by Dirac to the resulting phase space [?, ?] (see [?, ?] for a more philosophical approach and [?] for a groupoidtheoretical discussion about the definition of the configuration space of a gauge theory). In what follows, we shall restrict the analysis of Yang-Mills theories to the geometric level given by fiber bundles with connections. Philosophical analysis of Yang-Mills theories from the standpoint provided by the theory of fiber bundles has also been proposed in [?, Chap.6], [?], [?, Chap.3, pp.78-103], and [?]. [START_REF] Dougherty | The Hole Argument, take n[END_REF] A group action ρ : G × S → S defines a group homomorphism ϕ : G → Aut(S) from G to the group of automorphisms or symmetries of S given by ϕ(g) = ρ(g, -) : S → S.

A matter field is given by a section ϕ : M → E of a G-bundle, where the standard fiber S is typically given by a vector space. A value σ(x) ∈ S x can be interpreted as the internal state of the field σ at x. [START_REF] Dybjer | Intuitionistic Type Theory[END_REF] In order to address the gauge argument, let us consider first the notion of gauge symmetries. To do so, we shall follow an idiosyncratic presentation coming from Ehresmann's original paper on connections on fiber bundles [?]. The interest of this particular presentation is that it leads naturally to the notion of structure groupoid associated to a fiber bundle, thereby stressing the intimate relation between the theory of groupoids and the theory of fiber bundles (regarding this relation see also [?]).

The notion of gauge symmetry is usually understood in purely epistemic terms, that is as a freedom to change the local frames on each fiber in a spacetime-dependent manner. In the wake of Ehresmann, we shall understand by frame on a fiber S x a concrete equivalence between the standard fiber S and S x , i.e. an isomorphism p : S → S x . We shall say that the element p -1 (l) ∈ S is the label of l ∈ S x in the frame p. In the terms of the previous sections, a frame can be understood as a particular proof of the equality type S = S x .

If we have copies S x of an entity S with symmetries (i.e. of an entity with a non-trivial identity), then there are many possible equivalences between the copies and the original, i.e. many frames p : S → S x . Given a frame p and a group element g ∈ G (a symmetry of S), we can obtain another frame by composing the frame with the group action. In other terms, the action of G on the standard fiber S induces a right action on the set of frames Eq(S, S x ) given by the following composition Eq(S, S x ) × G → Eq(S, S x ) (

-→ S x , g) → (pg : S g -→ S p -→ S x ). 4) (S p
In this way, it follows from the non-trivial identity of S that the equality types S x = S admit many proofs. The point that we want to stress here is that the multiplicity of local frames at x is a consequence of the intrinsic fact that each S x is an identical copy of a symmetric structure S. As Auyang notes, "[t]he fiber has an intrinsic structure [emphasis ours] determined by the local symmetry group [...]" [?, p.60]. And this intrinsic geometric structure is such that there are many equivalences-i.e. many frames-between a fiber S x and the standard fiber S. We could say that the epistemic freedom to choose different frames in a local manner (i.e. different equivalences p : S → S x for each x) follows from the intrinsic geometric structure underlying Yang-Mills theories.

In this sense, the situation is not really different from physical theories with global symmetries. For instance, the fact that physics in a Minkowski spacetime is invariant under Poincaré transformations is not a mere epistemic observation about the subjective freedom to choose different reference frames, but rather a consequence of the intrinsic symmetries of flat spacetime. In this sense, considerations about the relativity of reference frames are derivative from the objective geometric structure of the corresponding geometry. The fact that a Poincaré transformation has no observable effect when applied on the whole universe does not mean that such a transformation is deprived of any intrinsic meaning or (indirect) empirical content. In fact, we should conclude exactly the opposite: the fact that a given transformation does not produce any observable effect witnesses for an intrinsic feature of the corresponding entity, namely its symmetric [START_REF] Dybjer | Intuitionistic Type Theory[END_REF] For a philosophical discussion of the fundamental difference between sections-that take values in the numerically different indiscernible spaces Sx-and functions-that take values in a single space-see [?].

nature under a particular group. And the observable quantities are invariant under the objective group of symmetries of Minkowski spacetime. For the particular case of special relativity, this point has been clearly stressed by Maudlin in the following terms "First, the notion of [...] an inertial frame of reference, is derivative rather than fundamental. Each of these concepts can only be defined by reference to some objective geometrical structure of spacetime itself, in order to make sense of the qualifier 'inertial'. So we ought to begin with the intrinsic geometry, not with coordinate systems or reference frames" [?, p.67] But special relativity is not a Yang-Mills theory. However, we can understand the transition from special relativity to Yang-Mills theories in terms of two generalizations, namely (1) from special relativity to general relativity, (2) from general relativity to Yang-Mills theories. [START_REF] Earman | Tracking Down Gauge: An Ode to the Constrained Hamiltonian Formalism[END_REF] The first generalization amounts to pass from the homogeneous Minkowski spacetime to spacetimes that are not necessarily homogeneous. This generalization can be performed by using the Minkowski spacetime as a local model of a general spacetime. This description of the transition from special to general relativity is particularly clear in the gauge-theoretic formulation of general relativity that uses the theory of Cartan connections (see [?, ?, ?] for a mathematical presentation of the theory of Cartan connections and [?, ?, ?] for more philosophical discussions). The important point is that this localization of the symmetries of Minkowski spacetime does not alter the interpretation of these symmetries as an intrinsic feature of this particular geometric structure. In fact, Minkowski spacetime with its global symmetries is a particular solution of general relativity. [START_REF] Earman | Two challenges to the requirement of substantive general covariance[END_REF] It is worth noting here that this transition from special to general relativity requires equipping the corresponding bundle with a non-canonical supplementary structure, namely a Cartan connection. The problem posited by the non-canonicity of the connection is solved by treating the connection as a dynamical object that locally depends on the density and flux of energy and momentum in the spacetime manifold.

Second, the transition from general relativity to Yang-Mills theories can be mathematically understood as a generalization from the theory of Cartan connections to the theory of Ehresmann connections. The central point of this generalization is that the fibers of the corresponding associated bundle of a Yang-Mills theory are not tangent to the base space of the bundle as it is the case in general relativity (this difference explains the main formal difference between Cartan and Ehresmann connections, namely the presence of a soldering form as a component of a Cartan connection [?]). More precisely, general relativity (at least in the gauge-theoretic formulation of the theory based on the theory of Cartan connections) is based on principal fiber bundles whose structure groups are symmetry groups of spaces that can be isomorphically mapped to [START_REF] Earman | Tracking Down Gauge: An Ode to the Constrained Hamiltonian Formalism[END_REF] In [?], the gauge argument is analyzed from the more standard perspective provided by the transition from a theory with a global symmetry without gauge fields to a theory with a local symmetry and gauge fields. The analysis proposed in that article addresses in particular the ontological commitments associated to the notion of global symmetry. [START_REF] Earman | Two challenges to the requirement of substantive general covariance[END_REF] the tangent spaces to spacetime by means of a soldering form. By contrast, Yang-Mills theories are based on principal fiber bundles whose structure group are not constrained in this way. All in all, the transition from special relativity to Yang Mills theories can be conceptually understood as a localization of the symmetries (which requires to equip the bundle with a Cartan connection) followed by a generalization of the fibers from fibers of the associated bundle that are tangent to the base space (or, more precisely, that can be isomorphically mapped to the tangent spaces by means of a soldering) to more general fibers (where this last generalization entails a generalization from Cartan to Ehresmann connections). [START_REF] Earman | The implications of general covariance for the ontology and ideology of spacetime[END_REF] The point that we want to stress here is that these two generalizations do not modify the fact that the symmetries of the fibers are part of their objective geometric structure. In particular, passing from global to local symmetries does not modify the fact that epistemic considerations about reference frames derive from the intrinsic symmetries of the geometric structures at stake. The new ingredient brought forth by this localization is the fact that we have to deal with equal copies S x of a symmetric structure S, where the intrinsic symmetries of S entail the existence of multiple frames p : S → S x . The empirical significance of Yang-Mills theories-which includes the experimental verifications of the standard model of elementary particles-relies in part on these objective geometric structures with their intrinsic symmetries.

Let us consider now the notion of G-principal fiber bundle. The sets Eq(S, S x ) of frames defined at all the spacetime locations x in M define the fibers P x of the G-principal bundle of local frames P → M . A G-principal bundle is a G-bundle where the standard fiber is G itself and the left action of G on G is the left translation [?, Def.10.2, p.87]. By construction, each fiber Eq(S, S x ) is isomorphic to the structure group G in a non-canonical manner. The expression (??) defines a right G-action on each fiber Eq(S, S x ) that is free37 and transitive [START_REF] Ehresmann | Les connexions infinitésimales dans un espace fibré différentiable[END_REF] . A set endowed with a free and transitive action of a group G is called a G-torsor or a G-principal (i.e. free) homogenous (i.e. transitive) space [?]. A G-torsor is a set X such that for any x, y in X, there is a unique g in G such that xg = y. This means that any two elements of the G-torsor are identified by the group action in a unique manner. We could say that a G-torsor X is a set X of indiscernible elements where the structure of these indiscernibilities is encoded in the group G. In particular, the set Eq(S, S x ) of frames at x is a right G-torsor. If we fix an element p 0 in Eq(S, S x ), we can define a map

κ p0 : G → Eq(S, S x ) (5)
g → p 0 g, which is surjective (since the action is transitive) and injective (since the action is free). Then, G and Eq(S, Sx) are isomorphic in a non-canonical manner. Each non-canonical isomorphism κ p0 is defined by specifying which element p 0 in Eq(S, S x ) will play the role of the neutral element in G. In Baez's terms, "A torsor is a group that has forgotten its identity [or neutral element]"

[?]. Conceptually, the notion of G-torsor encodes the fact that only relative differences matter in the presence of indiscernibilities. All frames in a fiber Eq(S, S x ) are exactly alike, but the transformation between any two frames is a well-defined group element. Given a principal fiber bundle P → M and a left action G × S → S of G on a space S, P × G S → M is a G-bundle "associated" to P [?, 10.7, p.90]. Here P × G S denotes the set of G-equivalence classes [(p, v)], where the G-right action that relates different representatives in a class is given by (p, v)g = (pg, g -1 v). Now, this bundle associated to P via the left action of G on S is nothing but the G-bundle E → M that we started with. [START_REF]The Thirteen Books of Euclid's Elements. Trans. from the text of Heiberg with introduction and commentary[END_REF] Conceptually, G-principal fibre bundles P → M can be understood as bundles of frames and associated fiber bundles P × G S → M can be understood as bundles of geometric objects that admit different coordinate representations in terms of the frames in P (and the corresponding labels in S). The adjective geometric in the expression geometric object stresses that an element in an associated bundle provides a frame-independent description of the object. This intrinsic description is given by an equivalence class of pairs of frames in P and labels in S.

Let us consider now the notions of passive and active gauge transformations. The transition functions (??) (that are sometimes called passive gauge transformations) define the global gluing between the different local charts (U i , ψ i ) of a fiber bundle atlas of a G-principal bundle P → M . But the same expressions can be used to relate different local trivializations ψ 1 i and ψ 2 i on the same open set U i . In this case, we shall have transition functions

ψ ii : U i → G
that define the transformations

ψ 1 i • (ψ 2 i ) -1 : U i × S -→ U i × S (6) (x, s) → (x, ψ ii (x)s)
Whereas in the case (??), the transition functions relate different local charts of the same fiber bundle atlas, in the case (??) they relate different fiber bundle atlases defined by different local trivializations. It is worth noting that in physics, the expression passive gauge transformation is not used in general to describe transformations between coordinate descriptions defined on different open sets U i and U j , but rather refer to transformations between different coordinate descriptions on the same open set U i . Given a G-principal fiber bundle P → M , one can define a local trivialization on U i by specifying a local section σ i : U i → P that selects a particular frame p for each x ∈ M . The local trivialization defined by the section σ i is given by ψ i (x, σ i (x)) = (x, id G ) and ψ i (x, σ i (x)g) = (x, g). Given two local sections σ 1 i and σ 2 i , the transition function between the corresponding local trivializations ψ 1 i and ψ 1 i will be given by

ψ ii : x → g(x), where g(x) is such that σ 2 i (x) = σ 1 i (x)g(x)
. [START_REF] Frege | Begriffsschrift, A Formula Language, Modeled Upon that for Arithmetic[END_REF] Conceptually, a local trivialization [START_REF]The Thirteen Books of Euclid's Elements. Trans. from the text of Heiberg with introduction and commentary[END_REF] Each element in P × G S over x defines an element in the fiber Sx of E. Indeed, given an element [(p : S → Sx, v)] we can evaluate p in v and obtain an element p(v) in Sx. If we consider another representative (pg, g -1 v) of [(p : S → Sx, v)], the evaluation still gives the same result, that is pg(g -1 v) = p(v) in Sx. In turn, an element w in a fiber Sx of E → M defines the equivalence class (p, p -1 (w)) in P × G S → M , where p can be any frame in Px (different frames define different representatives of the same equivalence class). [START_REF] Frege | Begriffsschrift, A Formula Language, Modeled Upon that for Arithmetic[END_REF] If the G-principal fiber bundle P → M is endowed with an Ehresmann connection, a local trivializing section σ i can be used to pullback the connection A ∈ Ω 1 (P ) ⊗ g and the curvature F ∈ Ω 2 (P ) ⊗ g g-valued forms on P to M (where g is the Lie algebra of G). By doing so, one obtains the usual local forms for the vector potential

A i = σ * i A ∈ Ω 1 (U i ) ⊗ g and the field strength F i = σ * i F ∈ Ω 2 (U i ) ⊗ g respectively.
If one modifies the local trivializing section σ i by means of a passive gauge transformation, the corresponding vector potentials and field is defined by selecting a particular frame σ i (x) = p : S → S x in the fiber P x of the principal bundle for each x ∈ U i in a continuous manner (in physics jargon, this is called fixing the gauge). In turn, a passive gauge transformation is defined by selecting a transformation g ∈ G of the frame σ i (x) for each x.

Passive gauge transformations should be distinguished from the so-called active gauge transformations given by the vertical automorphisms of the principal fiber bundle P → M . [START_REF] French | Identity in Physics. A Historical, Philosophical, and Formal Analysis[END_REF] The group G = Aut v P of vertical automorphisms of P → M is called gauge group. Whereas passive gauge transformations relate descriptions defined by different local trivializations (i.e. they change the "gauge"), active gauge transformations are intrinsic automorphisms of the corresponding principal fiber bundle. If we fix a local section σ i : U i → P , we can establish a correspondence between active gauge transformations and passive ones. Given a vertical automorphism Φ, we have Φ(σ i (x)) = σ i (x)g(x), thereby defining a transition function ψ ii : x → g(x), i.e. a passive gauge transformation. Reciprocally, given a transition function ψ ii : x → g(x) we can define a vertical automorphism of P by Φ(σ i (x)) = σ i (x)g(x) (where the action of Φ on other elements of the same fiber are defined by equivariance). If the principal bundle P → M is trivial one can define a global section σ : M → P and establish an identification between the gauge group and the group of G-valued functions on M . However, this identification between active and passive gauge transformations can only be established when the G-principal bundle is trivial. Moreover, it is not canonical since it depends on the election of the global section σ.

In order to conclude this section, let us note that the absolute internal value of a matter field ϕ : M → E in the internal space of states S x is deprived of an intrinsic physical meaning. Let us choose a frame p : S → S x and let us consider the G-orbit of the element p -1 (ϕ(x)) ∈ S that represents ϕ(x) in the frame p. The internal state ϕ(x) is indiscernible with respect to all the elements in the same fiber S x of the form p(gp -1 (ϕ(x))) for every g ∈ G. This means that ϕ(x) cannot be discerned from the internal states in the same fiber related to ϕ(x) by the symmetry transformations encoded in G. By the same token, let us consider two internal states ϕ(x) and ϕ(x ) in two infinitesimally distant locations such that there exist frames p : S → S x and p : S → S x satisfying that p -1 (ϕ(x)) and p -1 (ϕ(x )) are in the same G-orbit in S. Such states cannot be intrinsically compared. This means that it is not possible to assert whether a field ϕ that takes these internal values changes or not when passing from x to x . It follows that the notion of spatiotemporal variation of a field is partially deprived of an intrinsic physical meaning. In principle, it is not evident how one could extract intrinsic physical information from a theory of fields that take their values in internal spaces of states with symmetries.

Equality Types in Fiber Bundles

A G-bundle-being a numerical multiplicity of qualitatively identical fibers S x -provides a paradigmatic example of a mathematical structure that violates the PII and requires an extended notion of equality. Moreover, there are many possible proofs of the equalities S x = S y . This means that the correct notion of equality adapted to the notion of G-bundle is that of equality type. Since (as we have seen) equality types are formalized by groupoids, there seems to be a close relation (pointed out by Ehresmann in his seminal 1950 paper [?]) between fiber bundles and strengths transform according to the usual formulas for gauge transformations used by physicists (see for instance [?, Th.5.4.1, p.272]). [START_REF] French | Identity in Physics. A Historical, Philosophical, and Formal Analysis[END_REF] A vertical automorphism of P π -→ M is a diffeomorphism Φ : P → P of P that preserves the fibers (i.e. π • Φ := π) and that is G-equivariant (i.e. Φ(pg) = Φ(p)g).

groupoids (regarding the relation between these two notions see also [?]). In order to continue bridging the gap between gauge symmetries and gauge fields, we shall now consider in more detail the equality types defined by the fibers of a G-bundle and introduce the corresponding groupoids.

Given a G-bundle E → M , there are two different kinds of equalities that we can consider: the equalities between the points x of M (that we shall call bare points) and the equalities between (what we shall call) the structured points defined by the fibration, that is the points x ∈ M enriched with the internal structures S x . Both kinds of equalities can be understood ideally as ideal propositions that make abstraction from the proofs of the equalities or constructively as equality types whose tokens are the proofs of the propositions. Let us discuss these different possibilities.

Let us consider first the bare points of M . The equality x = y is true for any x, y in the connected manifold M . To begin with, these equalities can be understood as ideal equalities, which means that one makes abstraction from the multiple concrete equivalences that prove them. Such ideal equalities between the bare points are encoded in the so-called pair groupoid of M [?, p.7]

M × M ⇒ M. (7)
Each point of M is an objet in this groupoid and every possible pair (x, y) defines a reversible arrow x → y. Given that the composition of two composable arrows (x, y) and (y, z) is given by the arrow (x, z) (transitivity) and that there is a unique reflexive arrow (x, x) for each x (reflexivity), the arrow (y, x) is necessarily the inverse of (x, y) (symmetry). Thus the pair groupoid just encodes the maximal equivalence relation between the bare points of M (where maximal means that any two points are equivalent). This equivalence relation encodes the fact that any point of M is equivalent (we shall say equal ) to any other point, i.e. that all points are indiscernible. Since this maximal equivalence relation makes abstraction from the multiple concrete proofs of such equalities (given by the smooth paths in M ), it just encodes the ideal equalities x = y for any two x, y ∈ M (as we have explained in Section N • ??, equivalence relations provide the paradigmatic case of ideal equalities between numerically different indiscernible entities related at most by single equivalences).

On the other hand, we have already seen that this ideal description of equalities can be enriched in a constructivist manner by considering the paths γ : x → y in M as concrete proofs of the equality type x = y. Moreover, we have seen that homotopic paths γ, γ : x → y define equivalent proofs of such an equality. If one only considers the first level of equivalences provided by paths (and makes abstraction from the concrete homotopies between homotopic paths by just considering equivalence classes of homotopic paths), then this system of concrete equivalences between the points of M is encoded in the fundamental groupoid Π 1 (M ). As it is summarized in the Table 1 in Section N • ??, the definition of the fundamental groupoid Π 1 (M ) mixes different treatments of equalities: whereas the equalities between points are understood as equality types, the numerical multiplicities of homotopic paths are amalgamated into single homotopy classes.

It is worth noting that we have a morphism of groupoids between the fundamental groupoid Π 1 (M ) ⇒ M and the pair groupoid M × M ⇒ M , which is given by the identity on the objects in M and the map on the arrows

s × t : Π 1 (M ) → M × M (8)
[h] → (s(h), t(h))

that sends each arrow in Π 1 (M ) (each homotopy class [h] of paths) to its source and target [?, p.12]. This morphism projects all the homotopy classes of paths that have the same endpoints x and y to the same element (x, y) in M × M . Conceptually, this morphism of groupoids encodes the idealization operation (described in Section N • ??) by means of which the multiple proofs of an equality type x = y (i.e. all the homotopy classes of paths between x and y) are projected to the ideal proposition stating that x and y are equal. The fiber of the projection (??) over an element (x, y) ∈ M × M provides the resolution of the ideal equality between x and y into the corresponding concrete equivalences.

Let us now consider the equalities between the structured points defined by the G-bundle E → M (that is, the bare points x ∈ M enriched with the internal fibers S x ). Once again, all the fibers S x are indiscernible, i.e. the equalities S x = S y are true for any x and y. This results from the facts that all the fibers S x are isomorphic to the standard fiber S and that M is a connected space. Now, from a constructivist standpoint we have to consider the equalities S x = S y not as ideal equalities but rather as equality types. This means that the equality S x = S y will be understood as the equality type whose tokens are given by the concrete isomorphisms between S x and S y . Since the standard fiber S has non-trivial symmetries encoded by the structural group G, any two fibers S x and S y can be identified in many different ways and no equivalence is privileged. We shall now introduce a groupoid that encodes these multiple equivalences between the fibers of the G-bundle E → M . Given the G-principal bundle P π -→ M , we can define the Ehresmann structure groupoid associated to P ([?, p.34], [?, p.9]) [START_REF] Friederich | Symmetry, Empirical Equivalence, and Identity[END_REF] :

P × G P ⇒ M. ( 9
)
Here M is the manifold of objects (interpreted now as the fibers S x of E → M labeled by the points of M ) and P × G P is the manifold of isomorphisms between such objects. An arrow in P × G P is given by an equivalence class [(p y , p x )] (where p y ∈ P y and p x ∈ P x ) under the right G-action given by (p y , p x ) • g = (p y g, p x g) (see [?, p.9] and [?, p.32] for a more conceptualoriented description of this groupoid). In other terms, the equivalence classes are defined by the equivalence relation (p y , p x ) ∼ (p y g, p x g). Each arrow [(p y , p x )] ∈ P × G P defines the following equivalence between the copies S x and S y of S:

p y • p -1 x : S x p -1 x --→ S py -→ S y . (10)
So, given two frames p x : S → S x and p y : S → S y , the composition p y • p -1

x provides an equivalence between S x and S y , i.e. a proof of the equality type S x = S y .

As it was the case for the fundamental groupoid Π 1 (M ) ⇒ M , the structure groupoid P × G P ⇒ M is also endowed with a morphism of groupoids to the pair groupoid M × M ⇒ M . This projection is given by the identity on the objects in M and the following map between the arrows:

P × G P → M × M [(p 2 , p 1 )] → (π(p 2 ), π(p 1 )) ( 11
)
42 This groupoid is called gauge groupoid in references [?, ?].

where π : P → M . If we interpret the points x of M as labels of the fibers S x , then this morphism of groupoids also encodes the idealization operation by means of which the multiple proofs of an equality type S x = S y (the concrete equivalences between the structured points S x and S y ) are projected to the ideal proposition merely stating that S x and S y are equal.

It is also worth noting that in this context the spacetime M plays the role of a principle of numerical (rather than qualitative) individuation. In Weyl's terms "Since the mere Here is nothing by itself that might differ from any other Here, space is the principium individuationis. It makes the existence of numerically different things possible which are equal in every respect" [?, p.131] The fact that the fibers S x are in different spatiotemporal positions does not break their qualitative indiscernibility, since all the points of M are alike. Far from defining a qualitative property by means of which we could discern the fibers, the position in M merely provides a numerical individuation. The fact that the equalities S x = S y hold means that spacetime parameterizes indiscernible entities, even if they have different positions in M . This point was also clearly stressed by Auyang as follows: "[...] in scientific discourse [...] we are faced with countless entities that are more or less the same qualitatively. [...] Most other proponents of the cluster view [entities qua bundles of properties] appealed to the spatial and temporal positions of the entities as their unique qualities. This move is also fraught with difficulties. For as Leibniz argued, space points are themselves qualitatively alike and contribute nothing to differentiation. [...] If we treat space points as distinct despite their identical qualities, then we have already gone beyond the concept of qualities. The notion of numerical identity has been smuggled in. Let us finally consider the relations between the groupoids introduced thus far. The pair groupoid M × M ⇒ M can be interpreted both as the groupoid that encodes the ideal equalities x = y between the bare points of M and the groupoid that encodes the ideal equalities S x = S y between the structured points of the G-bundle E → M . These two systems of ideal equalities encoded by the same pair groupoid M × M ⇒ M are constructively resolved in equality types by the fundamental groupoid Π 1 (M ) ⇒ M and the structure groupoid P × G P ⇒ M respectively. So we have a diagram of groupoids defined at the level of the morphisms as follows:

P × G P Π 1 (M ) / / M × M (12)
Given these relationships between groupoids, it is natural to ask what is the relationship between the concrete equivalences γ : x → y between two bare points of M encoded in Π 1 (M ) and the concrete equivalences S x → S y between the corresponding structured points encoded in P × G P . The answer is that there is no natural correspondence between these two collections of equivalences. The definition of a G-bundle over M is an enrichment of M that endows the bare points of M with an additional structure that in general (with exceptions such as the tangent bundle) is not related to the geometry of M . Therefore, it can be expected that the concrete equivalences between the bare points are not naturally correlated to the equivalences between the fibers attached to these points. As we shall see in the next section, such a correspondence between "external" equivalences between the bare points and "internal" equivalences between the fibers can be nevertheless defined by endowing the fiber bundle with an additional geometric structure, namely an Ehresmann connection.

On Connections

In Section N • ??, we have proposed an ontological-oriented interpretation of the notion of gauge symmetry. We have argued that gauge symmetries are not a mere epistemic feature resulting from the freedom to choose reference frames in a spacetime-dependent manner, but rather a consequence of the intrinsic geometric structure of Yang-Mills theories (that of a family of identical copies S x of a symmetric object S). We shall now address the other fundamental notion engaged by the gauge argument, namely the notion of gauge field. The discovery that fundamental interactions (i.e. gravitation, electromagnetism, and the nuclear strong and weak interactions) can be described by gauge fields was one of the most important breakthroughs of the XXth century physics.

In mathematics, gauge fields are presented as connections on fiber bundles. These connections are of different sorts depending on the interaction. [START_REF] Goldstein | The Historical Development of Group Theoretical Ideas in Connexion with Euclid's Axiom of Congruence[END_REF] The subtlety and richness of the notion of connection on a principal fiber bundle is attested by the multiplicity of possible equivalent mathematical definitions. An Ehresmann connection on a G-principal fiber bundle P → M can be defined as a horizontal equivariant smooth distribution on P , as a g-valued 1-form on P satisfying certain conditions (where g is the Lie-algebra of the structural group G), as a compatible family of local g-valued 1-forms A i ∈ Ω 1 (U i ⊂ M, g) on M defined with respect to a local trivialization, and as a section of the anchor of the Atiyah algebroid [?, ?, ?, ?, ?].

All the aforementioned definitions introduce connections at the infinitesimal level. These infinitesimal structures can be then integrated to define parallel transports along finite paths in M . Now, another avenue to introduce connections is to define them directly as a prescription for lifting finite paths γ : x → y in M to paths γ : p x → p y in the total space P of a G-principal fiber bundle P → M (see for instance [?] and [?, Sect.2.1]). Since the lifted path γ in P can be understood as an equivalence between the frames p x : S → S x and p y : S → S y (such frames are said to be horizontally equivalent), the composition p y • p -1

x : S x → S y defines an equivalence between S x and S y . This means that a connection could be understood as a map sending paths in M to elements in the structure groupoid P × G P , i.e. to equivalences between the corresponding fibers of E → M . In our terms, a connection could be understood as a particular enrichment of the equivalences between the bare points of M given by paths in M into equivalences between [START_REF] Goldstein | The Historical Development of Group Theoretical Ideas in Connexion with Euclid's Axiom of Congruence[END_REF] While in Yang-Mills theories the gauge fields are described by Ehresmann connections, in general relativity the gravitational field is described by means of a Cartan connection (see [?] for an analysis of the relation between the two kinds of connections).

the fibers attached to these points by the G-bundle E → M . However, things are not so simple. We shall now see why this is so and how to cope with this.

Since the fiber of the G-principal bundle P → M at each point x is given by a G-torsor P x , what we need is a correspondence (a lift) between each γ : x → y and an equivalence τ γ : P x → P y between the corresponding G-torsors. [START_REF] Greaves | Empirical Consequences of Symmetries[END_REF] Since we want to define the system of equivalences between fibers as an extension of the concrete equivalences between the bare points of M , we want this extension to preserve the categorical properties-namely, the identities and the compositions-of the equivalences between the bare points of M . More precisely, this lifting should obey the conditions (1) of lifting each constant path id x : x → x to the trivial self-identification id Px : P x → P x , that is

τ idx = id Px
(2) and of preserving compositions, that is

τ γ1•γ2 = τ γ1 • τ γ2 .
These requirements amount to ask that the lifting be defined by a functor -that we shall call parallel transport functor -from a groupoid of equivalences between the bare points of M to the category of G-torsors. The goal is to find a groupoid of equivalences between the bare points of M that provides a suitable domain for the parallel transport functor.

In Section N • ?? we have argued that the structure of equivalences between the bare points of M is encoded in the fundamental groupoid Π 1 (M ). So, it can be tempting to define the transport functor as a functor from the fundamental groupoid Π 1 (M ) to the category of Gtorsors. However, we shall now see that the equality criterion for paths used to define the fundamental groupoid Π 1 (M )-namely that homotopic paths are equal-is too coarse. Briefly, this equality criterion is purely topological in the sense that the presence of a hole between the paths is the unique kind of obstruction for two paths with same endpoints to be homotopic. In particular, this equality criterion establishes that all paths with the same endpoints are equal in a simply-connected space. By contrast, the notion of connection brings forth a differential obstruction for two paths to be equal, namely the curvature of the connection.

Indeed, the parallel transport along different homotopic paths does not depend on the path (or, equivalently, parallel transport only depends on the underlying homotopy class of the path) only if the curvature of the connection vanishes. This is a consequence of the Ambrose-Singer theorem ([?], [?, p.89]). The Ambrose-Singer theorem states that the Lie algebra hol p of the holonomy Lie group Hol p at a point p ∈ P of a principal fiber bundle π : P → M endowed with an Ehresmann connection is given by the curvature of the connection. [START_REF] Guay | Geometrical Aspects of Local Gauge Symmetry[END_REF] If the curvature is zero, then this Lie algebra is trivial. It follows that the component of the holonomy group connected to the identity (i.e. the restricted holonomy group encoding the holonomies of loops homotopic to the [START_REF] Greaves | Empirical Consequences of Symmetries[END_REF] A morphism of G-torsors f : X → Y is a morphism between the sets X and Y such that f (pg) = f (p)g for all p ∈ X and g ∈ G.

45 Given a point p ∈ P such that π(p) = x and the set Ωx(P ) of loops in M based at x, the holonomy group

at p is Holp = {g ∈ G/τγ (p) = pg, γ ∈ Ωx(P )} ⊂ G,
where τγ (p) denotes the parallel transport of p along the loop γ. The restricted holonomy group is

Hol 0 p = g ∈ G/τγ (p) = pg, γ ∈ Ω 0 x (P )
where Ω 0 x (P ) is the set of loops in M based at x that are homotopic to the identity.

constant loop based at π(p) [?, Th. 4.2, p.73]) is just the identity and that the holonomy group is discrete. Since the holonomy of loops homotopic to the identity is trivial (by the Ambrose-Singer theorem), the only non-trivial holonomies are those associated to homotopy classes that encircle holes of the base space M . In such a case (vanishing curvature and a non-simply connected manifold M ), we are in a generalized (since not necessarily Abelian) Aharonov-Bohm scenario [?, ?]. In particular, the Aharonov-Bohm effect properly speaking was interpreted as a physical manifestation-in the particular case of the Abelian electromagnetic gauge theoryof the holonomy associated to a situation in which there is no curvature but the space M is not symply-connected. [START_REF] Guay | Symmetry and Its Formalisms: Mathematical Aspects[END_REF] In the case of a flat connection, parallel transports along homotopic paths coincide. Hence, the equality criterion for paths used in the definition of the fundamental groupoid Π 1 (M ) (by which homotopic paths are equal) is good enough. However, the Ambrose-Singer theorem deals with the more general situation in which there might be not only holes but also curvature. In such a case, the restricted holonomy group is no longer trivial and homotopic paths might have different horizontal lifts. Since-according to the definition of the fundamental groupoid Π 1 (M )-homotopic paths are amalgamated in single equivalence classes, the parallel transport functor cannot be defined as a functor on Π 1 (M ). Thus, the definition of this functor requires to refine the equality criterion for paths used to define the fundamental groupoid (according to which homotopic paths are equal) so that equal paths have the same horizontal lifts. One extreme alternative would be to use a strict equality criterion according to which no two numerically different paths can be equal. This amounts to using the paths themselves (and not classes of paths) as equivalences between points. But this is not an option since-as we have mentioned in Section N • ??-compositions of paths are not strictly associative and the composition of a path with its reverse path is only homotopic to the identity path. Therefore, we need a non-trivial equality criterion for paths somewhere in-between the equality given by homotopies and the strict equality.

Happily, there is a refinement of the notion of homotopy equivalence between paths that satisfies the required conditions, namely the notion of thin homotopy [?] (see also [?, pp.9-10]). Roughly speaking, a thin homotopy is a homotopy that encloses zero area. In particular, paths related by a reparameterization are thin-homotopic. This guarantees that compositions and the reverse paths γ -1 can be used to define a category. On the other hand, it can be shown that parallel transports along paths that are thin-homotopically equivalent do not depend on the path [?, Prop.4.3, p.28]. This means that thin homotopies provide a satisfactory equality criterion for paths in M such that the transport functor is well-defined (in the sense that the lifting does not depend on the chosen representative in a thin homotopy class of paths). It is worth noting that the introduction of a connection does not break the indiscernibilities between the points of M , i.e. they continue to be equal or indiscernible. However, the presence of a connection forces us to refine the topological equality criterion for paths given by the homotopy equivalence. In this sense, a connection rigidifies the structure of equivalences of M from a purely topological structure to a finer differential structure in which homotopic paths are not necessarily equal.

If we take as objects the points of M and as morphisms the thin homotopy classes of paths, we obtain the structure of a groupoid called the path groupoid P 1 (M ) of M [?, Sect.2.1] (see [?] for a friendly introduction). We can now consistently define a parallel transport functor [START_REF] Guay | Symmetry and Its Formalisms: Mathematical Aspects[END_REF] Philosophical-oriented discussions of the Aharonov-Bohm can be found in [?, ?, ?]. The topological interpretation mentioned here was in particular advocated in [?]. In [?], Earman criticized this interpretation by arguing that simply-connectedness of M is an idealization. τ : P 1 (M ) → G-T or. (13) sending each object x ∈ M in P 1 (M ) to the G-torsor P x and every thin homotopy class of paths γ : x → y to an isomorphism τ γ : P x → P y of G-torsors. [START_REF] Hamilton | Mathematical Gauge Theory[END_REF] It can be shown that the specification of such a functor is equivalent to the definition of an Ehresmann connection on the G-principal bundle P → M by means of a g-valued 1-form A [?, Sect.4]. From a conceptual standpoint, this functorial definition allows to understand an Ehresmann connection as a lifting of the concrete equivalences between the bare points of M given by thin homotopy classes of paths into concrete equivalences between the corresponding fibers. Let's now fix a point x ∈ M and a frame p 0 in P x , and let's only consider thin homotopy classes of loops based at x. Then the parallel transport functor (??) gets restricted to a map between the group π 1 1 (M, x) of thin homotopy classes of loops based at x and the group Aut G (P x ) of G-equivariant automorphisms of P x . By using the fact that P x is a G-torsor, it can be shown that Aut G (P x ) = G. [START_REF] Healey | Gauging What's Real. The Conceptual Foundations of Contemporary Gauge Theories[END_REF] Hence, the parallel transport functor (??) defines a group homomorphism (usually called holonomy map)

hol x : π 1 1 (M, x) → G.
For connected manifolds, isomorphism classes of holonomy maps (satisfying certain smoothness conditions) are in a bijective correspondence with isomorphism classes of G-principal fiber bundles with connections [?, ?]. According to this description, a connection can be understood as a group homomorphism from the identity type of a point x ∈ M (defined by means of a criterion of identity for paths given by thin homotopies) to the group of symmetries G of the fibers S x , i.e. to the identity type of these fibers.

Whereas the non-trivial identity type of the structureless points x is purely external in the sense that it depends on the geometry of the space M , the non-trivial identity type of the fibers S x is purely internal in the sense that it depends on their intrinsic symmetries. These two identity types provide two canonical examples of groups: homotopy groups for "external" identities and symmetry groups for "internal" identities. In principle, these two identity types are completely unrelated. Thus, if we understand the fibers S x as structures attached to x by the fiber bundle structure, there is no reason to expect any correspondence between the identity of x and the identity of S x . But if we do want to understand the fibers S x as internal structures of the points x (thereby giving rise to what we have called structured points), then we could expect some kind of compatibility condition between the external identity of x and the identity of its internal structure S x . Precisely this compatibility condition is provided by the supplementary geometric structure on the fiber bundle given by the connection. Thanks to the connection, the external identity type of the point x becomes correlated to the identity type of its internal structure in the sense that each external proof of the fact that the bare point x is identical to itself entails an internal proof of the self-identity of S x . We arrive in this way to what we could consider to be the most synthetic conceptual characterization of a connection, namely as a geometric structure [START_REF] Hamilton | Mathematical Gauge Theory[END_REF] We are here making abstraction from certain important considerations about smoothness-stating, roughly speaking, that τ has to depend smoothly on the path-since they are not relevant for the present discussion. [START_REF] Healey | Gauging What's Real. The Conceptual Foundations of Contemporary Gauge Theories[END_REF] Let us consider a G-equivariant map f : Px → Px. We want to show that such a map is defined by a unique element in G. Since the G-action is transitive, f (p 0 ) = p 0 g. So we shall associate f ∈ Aut G (Px) with the group element g ∈ G. The G-equivariance guarantees that the expression f (p 0 ) = p 0 g completely defines the map f . Indeed,

f (p 1 ) = f (p 0 g 1 ) = f (p 0 )g 1 = p 0 gg 1 .
that allows us to understand the fibers S x of a G bundle E → M as internal structures of the points x of M in a manner that is compatible with the identity types of both x and S x . Whereas in a fiber bundle without a connection the fibers are merely attached to the points of M , the fibers become internal structures of the points of M when the fiber bundle is endowed with a connection.

In addition, connections are the supplementary geometric structure by means of which it is possible to extract well-determined differences out of indiscernible internal states. By paralleltransporting an element p x in a fiber P x around a loop γ in M that encircles a hole we obtain another element p x in the same fiber. Since the fiber is a G-torsor, the "difference" between p x and p x is given by the group element g ∈ G that transforms the frame p x into p x (i.e. p x = p x g). In this way, while elements in a G-torsor do not have an intrinsic determinacy, two indiscernible elements determine a unique discernible element of the group, that is their "difference" g. [START_REF] Healey | Perfect Symmetries[END_REF] Only differences-rather than absolute values-matter (see [?] for a nice discussion of this point). [START_REF] Heathcote | Five Indistinguishable Spheres[END_REF] In fact, this can be understood as a formal generalization of Leibniz's argument against absolute space in the Leibniz-Clarke correspondence [?, p.26] to the case of the internal spaces given by the fibers: whereas the position of a body in a homogeneous space is deprived of any intrinsic physical meaning (since all the spatial positions are indiscernible), only the relations-we would rather say the differences or the ratios-between bodies are physically meaningful, that is "observable". Hence, changing their absolute positions without changing their relative positions does not change anything, i.e. it does not produce any observable effect. [START_REF] Henneaux | Quantization of Gauge Systems[END_REF] However, the fact that all absolute positions are indiscernible does not mean that the numerical multiplicity of positions has to be removed. Rather than enforcing the PII by removing numerical multiplicities of indiscernibles, one has to explicitly take into account the concrete equivalences that prove these indiscernibilities and put into focus the corresponding groupoid-theoretical structure. As we have argued in Section N • ??, the presence of indiscernibilities does not call for a strictification enforcing the PII, but rather for mathematical notions capable of encoding the very structure of these indiscernibilities.

In the philosophical literature on Yang-Mills theories, the debate about the scope of gaugedependent (or indiscernible) quantities took in particular the form of a tension between fiber bundle interpretations (Maudlin [?, pp.94-103], Arntzenius [?]) and holonomy interpretations [START_REF] Healey | Perfect Symmetries[END_REF] In the case of a non-Abelian gauge theory, the gauge invariants are not given directly by the holonomies, but rather by the Wilson loops obtained by taking the trace of the holonomies (see for instance [?, pp.240-242]). [START_REF] Heathcote | Five Indistinguishable Spheres[END_REF] In this description, the transformation g is understood as a transformation between the frames px and p x .

But such a transformation can also be understood as a symmetry of the internal space of states Sx. Let us consider an internal state l ∈ Sx represented in the frame p by the label s ∈ S (i.e. p(s) = l). In the new frame p = pg, s will be the label of the state l = p(gs). So, we can equivalently interpret the situation either as if the frame had change from p to p = pg or as if the internal state l ∈ Sx had been transformed to a new state l whose label in the old frame p would be gs (similar arguments can be found in [?, p.514] and [?, p.709]). [START_REF] Henneaux | Quantization of Gauge Systems[END_REF] In [?], Rovelli defends the Leibnizian thesis that gauge symmetries-far from being mere mathematical redundancies-"reveal the relational structure of our world". Rovelli analyzes in particular a toy model in which the differences (relative distances) between gauge-dependent quantities ("absolute" positions in a homogeneous space) are gauge invariant. Rovelli's stance converges with the thesis defended here according to which only differences (we would say here "relations" of equivalence) between indiscernible relata are physically meaningful (see also [?] for a discussion of Rovelli's article). Rovelli enriches this relational stance with the observation that the Lagrangian description of the coupling of two such systems cannot circumvent the use of gauge-dependent variables.

(Belot [?, ?], Lyre [?], and Healey [?]) of Yang-Mills theories. Whereas the fiber bundle interpretations of gauge theories rely on the local and gauge-dependent gauge potentials, the holonomy interpretations rely on the use of non-local gauge invariants (Wilson loops). The bijective correspondence mentioned above between principal fiber bundles with connections and holonomy maps seems to suggest that we can simply recast gauge theories in terms of the invariant quantities defined by the holonomies. In turn, this suggests that gauge-dependencies are a dispensable surplus structure associated to a descriptive redundancy. Now, the terms of this debate seem to presuppose that gauge invariants can be safely severed from the multiplicities of indiscernibles whose very structure these invariants describe. From a conceptual standpoint, the analysis that we have proposed points towards an integrative vision in which the gauge-dependent and the gauge-invariant quantities are two sides of the same structure. The gauge invariants obtained by parallel transports around loops are given by group elements g ∈ G (or their characters in the case of a non-Abelian gauge theory). But the group G encodes the very structure of indiscernibilities of each fiber S x . The claim that only the group-valued holonomies are physically meaningful seems to forget that the structure group G-out of which the invariants are constructed -supervene on the existence of numerical multiplicities of indiscernibles. The individual elements in a G-torsor P x are indiscernible, but the G-torsor itself has a structure isomorphic to G. [START_REF] Keränen | The Identity Problem for Realist Structuralism[END_REF] We cannot ascribe an empirical significance to observable (or gauge invariant) quantities constructed out of the structure group G and at the same time discard the symmetries encoded by G as a mere descriptive redundancy. [START_REF] Kobayashi | Foundations of Differential Geometry[END_REF] The evident fact that no physical consequence of a gauge theory can depend on the arbitrary election of a reference frame does not mean that the intrinsic symmetries (or indiscernibilities) that are at the origin of this epistemic freedom are nothing but a descriptive redundancy or a mathematical surplus structure. According to this we began by associating to each point in the base space fibers with the same geometrical structure. Fiber bundle theory may imply that there is no absolute comparison between physical states like color charge at different points, but there are absolute identities of form at a more abstract level" [?, p.102]. [START_REF] Kobayashi | Foundations of Differential Geometry[END_REF] As we have explained in footnote 22, the aim of this article is to analyze the geometric underpinnings of Yang-Mills provided by the theory of connections on fiber bundles (rather than from the standpoint provided by the theory of constrained Hamiltonian systems associated to the symplectic reduction of the phase space of connections and conjugated momenta [?, ?]). However, it is worth making here a comment on the latter. The restriction of the original phase space of the theory to the constraint surface Σ and the subsequent projection to the reduced phase space (obtained by taking the quotient of Σ by the action of the gauge group G) seems to provide a gauge-independent description from which all the gauge-dependencies have been quotiented out. However, the homotopic paradigm provides (in the form of what has been called derived geometry) enhanced definitions of intersections and quotients that allow to regularize singularities arising from non-transversal intersections and quotients defined by group actions that are not free respectively [?]. For instance, the strategy to define smooth quotients is the one that we have summarized in the Principle of Equality Types of Indiscernibles (see also footnote 19 on "bad quotients"), namely to keep the numerical multiplicities of indiscernible elements supplemented with the equivalences provided by the group action (rather than passing to the quotient space of equivalence classes). In fact, it was progressively understood that the most efficient method to deal with gauge symmetries-the BRST formalism [?, ?]-was nothing but a particular implementation avant la lettre of these ideas. The moral of the BRST formalism is clear: rather than quotiening out the gauge symmetries we have to unfold them all the way up.

To do so we have to keep the numerical multiplicities of gauge-equivalent field configurations by supplementing them with the gauge transformations understood as 1-equivalences (encoded in the so-called ghosts), with gauge transformations between gauge transformations understood as 2-equivalences (encoded in the so-called ghosts of ghosts) and so on and so forth [?, Sect. 3.5].

interpretation, it is precisely the existence of gauge-invariant quantities constructed out of the G-valued holonomies that witness for the empirical significance of gauge symmetries.

Conclusion

In this article we have addressed the problem of understanding the epistemic and ontological status of gauge symmetries by revisiting the link (established for the first time in the form of the gauge argument) between gauge symmetries and gauge fields. We have analyzed these notions from the geometric standpoint provided by the theory of Ehresmann connections on fiber bundles. By doing so, we have tried to anchor the notion of gauge symmetry (with its epistemic overtones) to the intrinsic geometric structures of the objects at stake. In particular, we have decided to explore a suggestive fact in the history of gauge theories, namely that one of the founding mathematical papers on the underlying geometric structures-Ehresmann's 1950 paper Les connexions infinitésimales dans un espace fibré différentiable [?]-introduces the notion of connection on a fiber bundle alongside with groupoid-theoretical considerations. The philosophical interest of this link between connections and groupoids results from the fact that it allows us to establish a bridge between the problem of interpreting gauge symmetries and the far-reaching groupoid-theoretical refoundation of mathematics associated to what we have called the homotopic paradigm. This research program (of which this article is nothing but a preliminary attempt; see also [?, ?, ?, ?, ?]) aims to revisit the foundational problems posited by gauge theories in light of the formal and conceptual innovations brought forward by the homotopic paradigm.

In the first part of this article, we have argued that the homotopic paradigm relies-at least from a conceptual standpoint-on two pillars:

(1) a rejection of the PII and the concomitant extension of the notion of strict or numerical equality to equalities between numerically different and indiscernible terms (that we have simply called equalities), (2) a constructivist understanding of equalities a = b as equality types of equivalences a → b (where each equivalence provides a particular proof of the fact that the proposition a = b is true).

The combination of these two enhancements of the notion of strict equality yields the notion of equality type formalized by groupoids. We have summarized this conceptual underpinning of the homotopic paradigm by means of a principle intended to replace the PII, namely the Principle of Equality Types of Indiscernibles. According to this principle, we should not remove the numerical multiplicities of indiscernible elements by only considering equivalence classes (which amounts to enforce the PII), but rather encode the indiscernibilities by means of equality types whose tokens are the concrete equivalences between the indiscernible entities. The nontrivial structure of (higher) equivalences encoded by these equality types-far from being a dispensable "surplus structure" that could be removed in a harmless manner-encodes structural homotopic information.

In the second part of this article, we have argued that the underlying geometric structure of Yang-Mills theories provides a paradigmatic example of a situation in which equality types become relevant. Indeed, the notion of G-bundle used in Yang-Mills theories (1') requires to consider equalities S x = S y between the numerically different and indiscernible copies S x of a standard fiber S,

(2') requires to understand these equalities S x = S y as equality types that encode the multiple possible equivalences S x → S y (resulting from the symmetries of S) between different fibers.

We have then used this conceptual framework to revisit the notions of gauge symmetry and gauge field as well as the relation between them. To conclude, let us summarize the main points of this analysis:

• In order to equilibrate the epistemic-ontological imbalance between the notions of gauge symmetry (with its strong epistemic overtones) and gauge fields (i.e. the potentials of the fundamental physical interactions), we have insisted on the intrinsic geometric underpinnings of gauge symmetries. To do so, we have stressed that the subjective freedom to fix the gauge-that is, to choose frames (i.e. equivalences p : S → S x ) in a local manner-is derivative from the intrinsic symmetries of the standard fiber S (encoded by the structure group G). • The interpretation of the existence of multiple equivalences between any two fibers S x and S y as a "surplus structure" amounts to endorsing an ideal understanding of the equalities S x = S y as mere truth values, i.e. it amounts to interpreting the existence of multiple proofs of such equalities as a mere proof-theoretic redundancy lacking objective content. In this sense, the epistemic interpretation of gauge symmetries as mere descriptive redundancy is a particular instance of the ideal understanding of equalities put into question by the homotopic paradigm. Gauge-theoretic indiscernibilities are not a "surplus structure" resulting from the existence of multiple descriptions of a unique state of affairs, but rather an intrinsic structure associated to the non-trivial identity types of the fibers S x . • We have revisited the articulation (established by the gauge argument) between gauge symmetries and gauge fields by analyzing the relation between the equivalences between the bare points of M and the equivalences between the corresponding "internal" fibers S x . Since both the bare points x ∈ M and the fibers S x have non-trivial identity types, we have argued that we cannot understand S x as an internal structure of x (rather than as a structure merely attached to x) without taking into account the relation between their identities. Along this line, we proposed a conceptual description of connections according to which a connection is the supplementary geometric structure that makes compatible the external identity type of a bare point x of M and the identity type of the internal structure S x defined by the G-bundle. Thanks to this supplementary geometric structure, each proof of the self-identity of the bare point x entails a proof of the self-identity of the structured point S x . • Whereas a flat connection can be understood as an extension of the identity type of x to its internal structure S x , a curved connection forces us to redefine the identity type of x at the level of the equality criterion for paths. The fact of endowing the fiber bundle with a connection does not break the indiscernibilities between the points of M . However, the groupoid-theoretical structure of these indiscernibilities changes if the curvature is not zero. More precisely, the curvature of a connection measures the breaking of the topological criterion of equality between paths (with same endpoints) given by homotopy equivalence into a finer criterion of identity given by thin homotopy equivalence. So, the indiscernibility between homotopic paths is in general broken to thin homotopies.

• Rather than positing a sharp opposition between the epistemic and the ontological reading of gauge symmetries, we have argued that it is precisely the intrinsic character of the underlying geometric symmetries that guarantees to a certain class of observers a "democratic" access to it, which translates as an epistemic freedom to choose any local reference frame (in a certain G-orbit) to describe it. [START_REF] Kock | Principal Bundles, Groupoids, and Connections[END_REF] We have then argued that the gauge invariant quantities constructed from the G-valued holonomies provide "observables" that witness for the empirical significance of the indiscernibilities whose very structure is encoded by the group G.

  [?]). Each equivalence class [a] in the set corresponds to a connected component of M (the component containing the point a ∈ M ). If a and b are in the same connected component, then [a] = [b]. Whereas the expression a = b is an equality that relates numerical different entities (that are qualitatively identical), the expression [a] = [b] is a strict or numerical equality in the sense that [a] and [b] are just different names that denote the same equivalence class.

  [...] Ordinary qualities are insufficient for the notion of entities. [...] what the spatio-temporal augmentation amounts to is that an extra general concept besides qualities is required for the notion of individuals. Let us call the extra concept the numerical identities of entities" [?, p.125]

  [START_REF] Brading | Are Gauge Symmetry Transformations Observable?[END_REF] A similar situation in physics is analyzed by Wüthrich in [?]. Wüthrich translates Keränen's "identity problem for realist structuralism" [?] to the case of spatially homogeneous and isotropic spacetimes. Wüthrich argues that if all the points in a spatial hypersurface share the same properties (i.e. if they are indiscernible), then "the universe consists of only one point [...] according to even the weakest form of the Principle of the Identity of Indiscernibles."

Table 1 .

 1 Homotopy Groupoids

		Π 0 (M )	Π 1 (M )	Π 2 (M )	... Π ∞ (M )
	Equalities btw points	Class. eq. Eq. types Eq. types	Eq. types
	Equalities btw paths	Class. eq. Class. eq. Eq. types	Eq. types
	Equalities btw homotopies Class. eq. Class. eq. Class. eq.	Eq. types
	...	"	"	"	"

Table 2 .

 2 Forms of EqualitiesStrict or numerical equality (PII) Qualitative equality (-PII)

	Ideal equalities	Ideal strict equalities (ex.: sets)	Ideal equalities (ex.: equivalence relations)
	Equality types	Identity types (ex.: groups)	Equality types (ex.: general groupoids)

  A similar claim was made by Greaves and Wallace in the following terms: "[...] in any theory that has a 'local' symmetry group, the 'global' symmetries remain as a subgroup of that local symmetry group. [...] It is therefore logically impossible that all global symmetries, but no local symmetries, can have direct empirical significance" [?, p.61].

For instance, moments in time are relatively discerned by the proposition "x is earlier than y".

For instance, two points in a Euclidean space separated by one mile are weakly discerned by the predicate "x is a mile apart from y".

In the terms of Ladyman and Presnell, the PII "[...] may be understood as a kind of minimalism about identity: facts about individuation are exhausted by facts about indiscernibility" [?, p.16].

For a history of the idea of understanding propositions as types see [?].

In Bell's terms: "Underlying [the doctrine of propositions as types] is the idealist notion, traceable to Kant,

In the case of a (n + 1)-groupoid, the truncation of groupoids (that we have previously described in terms of an idealization followed by a strictification) is applied to each Hom-groupoid between n-isomorphisms. By doing so, we obtain a n-groupoid.

These two transitions (and specially the first one) were described by Auyang in the following terms: "Historically, general relativity is the first theory with local symmetry. In contrast to special relativity, where a single inertial frame applies across the world, in general relativity the orientations of the inertial frames are free to vary from point to point, and the differences in orientations carry information about the gravitation field. This is the idea that Weyl tried to generalize to the electromagnetic field and that, with the advent of quantum mechanics, blossomed into gauge field theories" [?, pp.[START_REF] Ehresmann | Les connexions infinitésimales dans un espace fibré différentiable[END_REF][START_REF]The Thirteen Books of Euclid's Elements. Trans. from the text of Heiberg with introduction and commentary[END_REF]

.[START_REF] Earman | The role of idealizations in the Aharonov-Bohm effect[END_REF] This means that if pg = p, then g is the group

identity.[START_REF] Ehresmann | Les connexions infinitésimales dans un espace fibré différentiable[END_REF] This means that for each pair p, p in Eq(S, Sx), there exists a g in G such that pg = p .

This point has been stressed by Maudlin in the following terms: "When we constructed the fiber bundles,

Acknowledgments

The research leading to these results has received funding from the CNRS in the framework of the Laboratoire International Associé (LIA) Identities, Forces, Quanta.

Bibliography