\(\newcommand{\textesh}{∫}\) \(\newcommand{\ensuremath}{}\)

Abstract

Higher inductive types can capture some concepts of differential geometry in two dimensions including connections, curvature, and vector fields. We define connections on higher inductive types. We then define tangent bundles and vector fields by looking at the special subclass of combinatorial manifolds, which are discrete in the sense of real cohesion (Shulman, 2017), drawing inspiration from the field of discrete differential geometry. We prove the Gauss-Bonnet theorem and Poincaré-Hopf theorem for combinatorial manifolds.

“It is always ourselves we work on, whether we realize it or not. There is no other work to be done in the world.” — Stephen Talbott, The Future Does Not Compute (Talbott, 1995)

1 Overview

We will define

• combinatorial 2-manifolds

• circle bundles, and principal circle bundles of tangent bundles

• vector fields,

and then observe emerging from those definitions the presence of

• connections

• curvature

• the index of a vector field,

and prove

• the Gauss-Bonnet theorem

• and the Poincaré-Hopf theorem.

We will consider functions \(M\to \mathrm{EM}(\ensuremath{\mathbb{Z}},1)\) where \(\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\) is the connected component in the universe of the Eilenberg-MacLane space \(\mathrm{K}(\ensuremath{\mathbb{Z}},1)\) which we will take to be \(S^1\), and where \(M\) is a combinatorial manifold of dimension 2, which is a simplicial complex encoded in a higher inductive type, such that each vertex has a neighborhood that looks like a disk with a discrete circle boundary (i.e. a polygon). We can call terms \(C:\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\) “mere circles.”

We will see in Section 3.3 that \(\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\) contains all the polygons. We will construct a map \(\mathop{\mathrm{\mathsf{link}}}:M\to\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\) that maps each vertex to the polygon consisting of its neighbors. Then we can consider the type of pointed mere circles \(\mathrm{EM_{\bullet}}(\ensuremath{\mathbb{Z}},1)\stackrel{\mathrm{def}}{=}\sum_{Y:\mathrm{EM}(\ensuremath{\mathbb{Z}},1)}Y\) as well as the first projection that forgets the point. This is a univalent fibration (univalent fibrations are always equivalent to a projection of a type of pointed types to some connected component of the universe (Christensen, 2015)). If we form the pullback

then we have a bundle of mere circles, with total space given by the \(\sum_{}\)-type construction. We will show that this is not a principal bundle, i.e. a bundle of torsors. Torsors are types with the additional structure of a group action. But if \(\mathop{\mathrm{\mathsf{link}}}\) satisfies an additional property (amounting to an orientation) then the pullback is a principal fibration, i.e. \(\mathop{\mathrm{\mathsf{link}}}\) factors through a map \(\mathrm{K}(\ensuremath{\mathbb{Z}},2)\to\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\), where \(\mathrm{K}(\ensuremath{\mathbb{Z}},2)\) is an Eilenberg-Mac Lane space.

We will argue that extending \(\mathop{\mathrm{\mathsf{link}}}\) to a function \(T\) on paths can be thought of as constructing a connection, notably one that is not necessarily flat (trivial). Moreover, lifting \(T\) to \(T_\bullet:M\to\mathrm{EM_{\bullet}}(\ensuremath{\mathbb{Z}},1)\) can be thought of as a nonvanishing vector field. There will in general not be a total lift, just a partial function. The domain of \(T_\bullet\) will have a boundary of circles, and the degree (winding number) on the disjoint union of these can be thought of as the index of \(T_\bullet\). We can then examine the total curvature and the total index and prove that they are equal, and argue that they are equal to the usual Euler characteristic. This will simultaneously prove the Poincaré-Hopf theorem and Gauss-Bonnet theorem in 2 dimensions, for combinatorial manifolds. This is similar to the classical proof of Hopf (Hopf, 1983), presented in detail in Needham (Needham, 2021).

1.1 Future work

The results of this note can be extended in many directions. There are higher-dimensional generalizations of Gauss-Bonnet, including the theory of characteristic classes and Chern-Weil theory (which links characteristic classes to connections and curvature). These would involve working with nonabelian groups like \(SO(n)\) and sphere bundles. Results from gauge theory could be imported into HoTT, as well as results from surgery theory and other topological constructions that may be especially amenable to this discrete setting. Relationships with computer graphics and discrete differential geometry (Crane et al., 2013) (Crane, 2010) could be explored. Finally, a theory that reintroduces smoothness could allow more formal versions of the analogies explored here.

2 Torsors and principal bundles

The classical theory of principal bundles tells us to look for an appropriate classifying space of torsors to map into.

If \((X,\phi),(Y,\psi):BG\) then a \(G\)-equivariant map is a function \(f:X\to Y\) such that \(f(\phi(g,x))=\psi(g,f(x))\). Denote the type of \(G\)-equivariant maps by \(X\to_G Y\).

Denote by \(*\) the torsor given by \(G\) actions on its underlying set by left-translation. This serves as a basepoint for \(BG\) and we have a group isomorphism \(\Omega BG\simeq G\).

In particular, to classify principal \(S^1\)-bundles we map into the space \(\mathrm{K}(S^1, 1)\), a type of torsors of the circle. Since \(S^1\) is a \(\mathrm{K}(\ensuremath{\mathbb{Z}},1)\), we have \(\mathrm{K}(S^1,1)\simeq\mathrm{K}(\ensuremath{\mathbb{Z}},2)\).

2.1 Bundles of mere circles

We find it illuminating to look also at the slightly more general classifying space of \(\mathrm{K}(\ensuremath{\mathbb{Z}},1)\)-bundles, that is bundles whose fiber are equivalent to \(\mathrm{K}(\ensuremath{\mathbb{Z}},1)\). We can understand very well when these are in fact bundles of circle torsors, which will in turn shed light on orientation in this setting.

We will follow Scoccola (Scoccola, 2020). We will state the definitions and theorems for a general \(\mathrm{K}(G,n)\) but we will be focusing on \(n=1\) in this note.

Scoccola uses two self-maps on the universe: suspension followed by \((n+1)\)-truncation \(||\Sigma||_{n+1}\) and forgetting a point \(F_\bullet\) to form the composition \[\mathrm{EM}(G,n)\xrightarrow[]{||\Sigma||_{n+1}} \mathrm{EM}_{\bullet\bullet}(G,n+1)\xrightarrow[]{F_\bullet}\mathrm{EM_{\bullet}}(G,n+1)\] from types to types with two points (north and south), to pointed types (by forgetting the south point).

Let’s relate this to orientation. Note that the obstruction in the theorem is about a map into \(\mathrm{EM_{\bullet}}(G,n+1)\) and further note that \(\mathrm{EM_{\bullet}}(G,n)\simeq \mathrm{K}(\mathop{\mathrm{Aut}}G,1)\) (independent of \(n\)). The theorem says that the data of a map into \(\mathrm{EM}(G,n)\) factors into data about a map into \(\mathrm{K}(G,n+1)\) and one into \(\mathrm{K}(\mathop{\mathrm{Aut}}G,1)\). Informally, \(\mathrm{EM}(G,n)\) is a little too large to be a \(K(G,n+1)\), as it includes data about automorphisms of \(G\).

In the special case of \(\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\) the conditions of the theorem are met when \(f_\bullet:M\to\mathrm{K}(\mathop{\mathrm{Aut}}\ensuremath{\mathbb{Z}}, 1)\) is contractible. \(\mathop{\mathrm{Aut}}\ensuremath{\mathbb{Z}}\) consists of the \(\ensuremath{\mathbb{Z}}/2\ensuremath{\mathbb{Z}}\) worth of outer automorphisms given by multiplication by \(\pm 1\). If we look at the fiber sequence \[\mathrm{K}(S^1, 1)\to \mathop{\mathrm{BAut}}S^1\to \mathrm{K}(\mathop{\mathrm{Aut}}\ensuremath{\mathbb{Z}}, 1)\] we see the automorphisms of the circle as an extension of the group of automorphisms that are homotopic to the identity (which are the torsorial actions) by the group that sends the loop in \(S^1\) to its inverse. This is another way to see that a map \(f:M\to \mathop{\mathrm{BAut}}S^1\simeq \mathrm{EM}(\ensuremath{\mathbb{Z}},1)\) factors through \(\mathrm{K}(S^1, 1)\simeq \mathrm{K}(\ensuremath{\mathbb{Z}},2)\) if and only if the composition to \(\mathrm{K}(\mathop{\mathrm{Aut}}\ensuremath{\mathbb{Z}},1)\) is trivial. This amounts to a choice of loop-direction for all the circles, and so deserves the name “\(f\) is oriented.” In addition the map \(\mathop{\mathrm{BAut}}S^1\to \mathrm{K}(\mathop{\mathrm{Aut}}\ensuremath{\mathbb{Z}}, 1)\) deserves to be called the first Stiefel-Whitney class of \(f\), and the requirement here is that it vanishes.

2.2 Pathovers in circle bundles

Suppose we have \(T:M\to\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\) and \(P\stackrel{\mathrm{def}}{=}\sum_{x:M}T(x)\). We adopt a convention of naming objects in \(M\) with Latin letters, and the corresponding structures in \(P\) with Greek letters. Recall that if \(p:a=_M b\) then \(T\) acts on \(p\) with what’s called the action on paths, denoted \(\ensuremath{\mathsf{ap}}(T)(p):T(a)=T(b)\). This is a path in the codomain, which in this case is a type of types. Type theory also provides a function called transport, denoted \(\mathsf{tr}(p):T(a)\to T(b)\) which acts on the fibers of \(P\). \(\mathsf{tr}(p)\) is a function, acting on the terms of the types \(T(a)\) and \(T(b)\), and univalence tells us this is the isomorphism corresponding to \(\ensuremath{\mathsf{ap}}(T)(p)\).

Type theory also tells us that paths in \(P\) are given by pairs of paths: a path \(p:a=_M b\) in the base, and a pathover \(\pi:\mathsf{tr}(p)(\alpha)=_{T(b)}\beta\) between \(\alpha:T(a)\) and \(\beta:T(b)\) in the fibers. We can’t directly compare \(\alpha\) and \(\beta\) since they are of different types, so we apply transport to one of them. We say \(\pi\) lies over \(p\). See Figure 1.

Lastly we want to recall that in the presence of a section \(X:M\to P\) there is a dependent generalization of \(\ensuremath{\mathsf{ap}}\) called \(\mathsf{apd}\): \(\mathsf{apd}(X)(p):\mathsf{tr}(p)(X(a))=X(b)\) which is a pathover between the two values of the section over the basepoints of the path \(p\).

3 Discrete manifolds

3.1 Abstract simplicial complexes

which attaches each \(k\)-simplex by taking the convex hull of the appropriate \(k+1\) points in \(|M_{\leq k-1}|\). The collection of vertical maps on the right gives a sequence of inclusion maps of skeleta \(|M_0|\xrightarrow[]{i_1}|M_{\leq 1}|\xrightarrow[]{i_2}\cdots\xrightarrow[]{i_n}|M_{\leq n}|=|M|\).

The link is easier to understand as all the neighboring vertices of \(v\) and the subcomplex containing these. See for example Figure 2.

In a 2-dimensional combinatorial manifold the link is a polygon. See Figures 3, 4, and 5 for some examples of 2-dimensional combinatorial manifolds of genus 0, 1, and 3.

A classical 1940 result of Whitehead, building on Cairn, states that every smooth manifold admits a combinatorial triangulation (Whitehead, 1940). So it appears reasonably well motivated to study this class of objects. See for example the classic book by Kirby and Siebenmann (Kirby & Siebenmann, 1977).

3.2 Higher inductive combinatorial manifolds

Instead of \(|M|:\mathsf{Top}\) we can use the simplicial complex to obtain \(\ensuremath{\mathbb{M}}:\mathsf{Type}\) by forming a sequence of homotopy pushouts:

For example in dimension 1 we could take the triangle with vertices \(\{v_1, v_2, v_3\}\) and edges \(\{e_{12}, e_{23}, e_{31}\}\) and form a polygon \(C_3\):

In dimension 2 we could fill in maps from \(C_3\) into our higher type by adding faces (hence reusing the object we just built above):

The types \(C_3\) and \(\ensuremath{\mathbb{M}}_1\) are 1-types, \(\ensuremath{\mathbb{M}}_2\) is a 2-type, and the rest are sets. The map \(\partial_0\) maps each pair \((e, S^0)\) to the pair of points this edge connects. Similarly, \(\partial_1\) maps each \((f, C_3)\) to the triangle that this face bounds. The \(h_i\) are the proofs of commutativity, and the two squares are also both homotopy pushouts. Note that the pushouts could be re-expressed as HIT constructors.

Whereas in geometric realization we use both \(\Delta^i\) and \(\partial\Delta^i\) to attach simplices, in this homotopy picture we need an explicit construction of “\(\partial\Delta^i\)” as a type equivalent to an \(i-1\)-dimensional sphere and the filling of this sphere with \(i\)-dimensional stuff has moved into the proof of commutativity. So in dimension \(n\) the picture would be

It’s useful to define types that remember all or some of the data in these diagrams:

The name “presented type” is inspired by von Raumer (Raumer, 2015), where he uses such a structure in dimension 2 to construct double groupoids and crossed modules in type theory.

The maps \(*_i:M_i\to\ensuremath{\mathbb{M}}_i\) pick out hub terms for each vertex, edge, face, and so on. Each of these higher faces has this designated point and a family of paths joining that point to the entire boundary. This is a hub and spoke model, with the maps \(*_v\) etc. giving us the hubs. When we work with \(\mathsf{MType}^{[n]}\) we may access the vertices and faces, and the explicit paths inside the pushouts.

Going forward we will stick with 2-dimensional complexes, where forming the link of a vertex gives us a map \(\ensuremath{\mathbb{M}}_0\to\ensuremath{\mathsf{Gon}}\) exactly when the complex is a combinatorial manifold, which by Corollary 2 means we have a map \(\mathop{\mathrm{\mathsf{link}}}:\ensuremath{\mathbb{M}}_0\to\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\). Extending this map to all of \(\ensuremath{\mathbb{M}}\) and exploring what we obtain is the main purpose of this note.

3.3 Polygons

The 1-type \(C_3\) we created earlier by pushing out the combinatorial data of a set-based simplicial triangle is clearly an example of a type of marked presented polygons \(C_n, n:\ensuremath{\mathbb{N}}\). The standard HoTT circle itself is usually given as a HIT and is a non-example of a combinatorial manifold since it lacks the second vertex of the edge:

Denote by \(\ensuremath{\mathsf{Gon}}\) the set of marked presented \(n\)-gons for some natural number \(n\). We’ll see below that the realization of an \(n\)-gon is a mere circle, i.e. we have a forgetful map \(\ensuremath{\mathsf{Gon}}\to \mathrm{EM}(\ensuremath{\mathbb{Z}},1)\).

3.4 Adding and removing points from polygons

Recall that given functions \(\phi,\psi:A\to B\) between two arbitrary types we can form a type family of paths \(\alpha:A\to\mathcal{U}\) by \(\alpha(a)\stackrel{\mathrm{def}}{=}(\phi(a)=_B\psi(a))\). Transport in this family is given by concatenation as follows, where \(p:a=_A a'\) and \(q:\phi(a)=\psi(a)\) (see Figure 6): \[\mathsf{tr}(p)(q) = \phi(p)^{-1}\cdot q\cdot \psi(p)\] which gives a path in \(\phi(a')=\psi(a')\) by connecting dots between the terms \(\phi(a'), \phi(a), \psi(a), \psi(a')\). This relates a would-be homotopy \(\phi\sim\psi\) specified at a single point, to a point at the end of a path. We will use this to help construct such homotopies.

Proof. (Compare to (Univalent Foundations Program, 2013) Lemma 6.5.1.) In the case of \(C_1\) we will denote its constructors by \(\ensuremath{\mathsf{base}}\) and \(\ensuremath{\mathsf{loop}}\). For \(C_2\) we will denote the points by \(v_1, v_2\) and the edges by \(\ell_{12}, r_{21}\). For \(C_3\) and higher we will denote the points by \(v_1,\ldots,v_n\) and the edges by \(e_{i,j}:v_i=v_j\) where \(j=i+1\) except for \(e_{n,1}\).

First we will define \(f:C_2\to C_1\) and \(g:C_1\to C_2\), then prove they are inverses. \[\begin{aligned} f(v_1)=f(v_2)&=\ensuremath{\mathsf{base}}&\quad g(\ensuremath{\mathsf{base}})&=v_1\\ f(\ell_{12})&=\ensuremath{\mathsf{loop}}&\quad g(\ensuremath{\mathsf{loop}})&=\ell_{12}\cdot r_{21}\\ f(r_{21}) &= \ensuremath{\mathsf{refl}}_{\ensuremath{\mathsf{base}}}& & \\ \end{aligned}\]

We need to show that \(f\circ g\sim \ensuremath{\text{id}}_{C_1}\) and \(g\circ f\sim\ensuremath{\text{id}}_{C_2}\). Think of \(f\) as sliding \(v_2\) along \(r_{21}\) to coalesce with \(v_1\). This may help understand why the unfortunately intricate proof is working.

We need terms \(p:\prod_{a:C_1}f(g(a))=a\) and \(q:\prod_{a:C_2}g(f(a))=a\). We will proceed by induction, defining appropriate paths on point constructors and then checking a condition on path constructors that confirms that the built-in transport of these type families respects the definition on points.

Looking first at \(g\circ f\), which shrinks \(r_{21}\), we have the following data to work with: \[\begin{aligned} g(f(v_1))=g(f(v_2))&=v_1\\ g(f(\ell_{12}))&=\ell_{12}\cdot r_{21}\\ g(f(r_{21})) &= \ensuremath{\mathsf{refl}}_{v_1}. \end{aligned}\] We then need to supply a homotopy from this data to \(\ensuremath{\text{id}}_{C_2}\), which consists of a section and pathovers over \(C_2\): \[\begin{aligned} p_1&:g(f(v_1))=v_1\\ p_2&:g(f(v_1))=v_2\\ H_\ell&:\mathsf{tr}(\ell_{12})(p_1)=p_2\\ H_r&:\mathsf{tr}(r_{21})(p_2)=p_1. \end{aligned}\] which simplifies to \[\begin{aligned} p_1&:v_1=v_1\\ p_2&:v_1=v_2\\ H_\ell&:g(f(\ell_{12}))^{-1}\cdot p_1\cdot \ell_{12}=p_2\\ H_r&:=g(f(r_{21}))^{-1}\cdot p_2\cdot r_{21}= p_1 \end{aligned}\] and then to \[\begin{aligned} p_1&:v_1=v_1\\ p_2&:v_1=v_2\\ H_\ell&:(\ell_{12}\cdot r_{21})^{-1}\cdot p_1\cdot \ell_{12}=p_2\\ H_r&:\ensuremath{\mathsf{refl}}_{v_1}\cdot p_2\cdot r_{21}= p_1 \end{aligned}\]

To solve all of these constraints we can choose \(p_1\stackrel{\mathrm{def}}{=}\ensuremath{\mathsf{refl}}_{v_1}\), which by consulting either \(H_\ell\) or \(H_r\) requires that we take \(p_2\stackrel{\mathrm{def}}{=}{r_{21}}^{-1}\).

Now examining \(f\circ g\), we have \[\begin{aligned} f(g(\ensuremath{\mathsf{base}}))&=\ensuremath{\mathsf{base}}&\\ f(g(\ensuremath{\mathsf{loop}}))&=f(\ell_{12}\cdot r_{21})=\ensuremath{\mathsf{loop}} \end{aligned}\] and so we have an easy proof that this is the identity.

The proof of the more general case \(C_n \simeq C_{n-1}\) is very similar. Take the maps \(f:C_n\to C_{n-1}\), \(g:C_{n-1}\to C_n\) to be \[\begin{aligned} f(v_i)=v_i&\quad(i=1,\ldots,n-1) & g(v_i)&=v_i&\quad(i=1,\ldots,n-1)\\ f(v_n)=v_1&\quad& g(e_{i,i+1})&=e_{i,i+1}&\quad(i=1,\ldots,n-2)\\ f(e_{i,i+1})=e_{i,i+1}&\quad(i=1,\ldots,n-1)& g(e_{n-1,1})&=e_{n-1,n}\cdot e_{n,1}&\\ f(e_{n-1,n})=e_{n-1,1}&&&&\\ f(e_{n,1})=\ensuremath{\mathsf{refl}}_{v_1}&&&& \end{aligned}\] where \(f\) should be thought of as shrinking \(e_{n,1}\) so that \(v_n\) coalesces into \(v_1\).

The proof that \(g\circ f\sim\ensuremath{\text{id}}_{C_n}\) proceeds as follows: the composition is definitionally the identity except \[\begin{aligned} g(f(v_n))&=v_1\\ g(f(e_{n-1,n}))&=e_{n-1,n}\cdot e_{n,1}\\ g(f(e_{n,1}))&= \ensuremath{\mathsf{refl}}_{v_1}. \end{aligned}\] Guided by our previous experience we choose \({e_{n,1}}^{-1}:g(f(v_n))=v_n\), and define the pathovers by transport.

The proof that \(f\circ g\sim\ensuremath{\text{id}}_{C_{n-1}}\) requires only noting that \(f(g(e_{n-1,1}))=f(e_{n-1,n}\cdot e_{n,1})=e_{n-1,1}\cdot\ensuremath{\mathsf{refl}}_{v_1}=e_{n-1,1}\). ◻

Proof. We can add \(n-1\) points to \(S^1\) and use Lemma 3. ◻

With \(m_k\) we can start with a collection of pentagons and hexagons and make the collection homogeneous: by applying \(m_6\) to the pentagons and \(m_5\) to the hexagons we obtain a collection of 30-gons. This will be useful when we work more with the link function.

3.5 The higher inductive type \(\ensuremath{\mathbb{O}}\)

We will create our first combinatorial surface, an octahedron. In \(\mathsf{SimpCompSet_n}\) the combinatorial data of the faces can be represented with a Hasse diagram, which shows the poset of inclusions in a graded manner, with a special top and bottom element. We give an octahedron in Figure 7. The names of the vertices are short for white, yellow, blue, red, green, and orange, the colors of the faces of a Rubik’s cube. The octahedron is the dual of the cube, with each vertex corresponding to a face.

Applying the map \(\mathcal{R}\) to \(O_0\to O_1\to O\) gives the presented type \(\ensuremath{\mathbb{O}}_0\to \ensuremath{\mathbb{O}}_1\to \ensuremath{\mathbb{O}}\).

4 Connections and curvature

4.1 The function \(T\)

We will build up a map \(T\) out of \(\ensuremath{\mathbb{O}}\) which is meant to be like the circle bundle of a tangent bundle. And so we will begin with the intrinsic data of the link at each point: taking the link of a vertex gives us a map from vertices to polygons.

To extend \(T_0\) to a function \(T_1\) on the 1-skeleton we have complete freedom. Defining a map by induction makes clear that the action on paths is its own structure. Two functions on the octahedron could agree on points but differ on edges. We are going to identify this 1-dimensional freedom with a connection:

Continuing the example, we will do something “tangent bundley”, imagining how \(T_1\) changes as we slide from point to point in the embedding shown in the figures. Sliding from \(w\) to \(b\) and tipping the link as we go, we see \(r\mapsto r\) and \(o\mapsto o\) because those lie on the axis of rotation. Then \(g\mapsto w\) and \(b\mapsto y\).

It’s very important to be able to visualize what \(T_1\) does to triangular paths such as \(wb\cdot br\cdot rw\) (which circulates around the boundary of face \(wbr\)). You can see it if you imagine Figure 8 as the frames of a short movie. Or you can place your palm over the top of a cube and note where your fingers are pointing, then slide your hand to an equatorial face, then along the equator, then back to the top. The answer is: you come back rotated clockwise by a quarter-turn.

Note by univalence the equivalence \(R\) gives a loop in the universe, a term of \(C_4=_{\mathrm{EM}(\ensuremath{\mathbb{Z}},1)}C_4\).

Now let’s extend \(T_1\) to all of \(\ensuremath{\mathbb{O}}\) by providing values for the eight faces. The face \(wbr\) is a path from \(\ensuremath{\mathsf{refl}}_w\) to the concatenation \(wb\cdot br\cdot rw\), and so the image of \(wbr\) under the extended version of \(T_1\) must be a homotopy from \(\ensuremath{\mathsf{refl}}_{T_1(w)}\) to \(T_1(wb\cdot br\cdot rw)\). Here there is no additional freedom.

4.2 Total holonomy

The purpose of this type is to probe combinatorial manifolds in an organized fashion, by mapping \(L\) into the type \(\ensuremath{\mathbb{M}}\).

Given a face enumerator we can form the compositions \(T\circ\ell_{L,i}\) with the associated loop to obtain transport isomorphisms \(T\circ\ell_{L,i}:Tm=Tm\). We can concatenate all the loops \(\ell_{L,1}\cdot\cdots\cdot\ell_{L,k}\) and obtain a total holonomy \(T\circ(\ell_{L,1}\cdot\cdots\cdot\ell_{L,k}):Tm=Tm\).

4.3 Existence of connections

How confident can we be that we can always define a connection on an arbitrary combinatorial manifold? Two things make the octahedron example special: the link is a 4-gon at every vertex, and every edge extends to a symmetry of the entire octahedron, embedded in 3-dimensional space. This imposed a coherence on the interactions of all the choices we made for the connection, which we can worry may not exist for more complex combinatorial data.

We know as a fact outside of HoTT that any combinatorial surface that has been realized as a triangulated surface embedded in 3-dimensional euclidean space can inherit the parallel transport entailed in the embedding. We could then approximate that data to arbitrary precision with enough subdivision of the fibers of \(T\).

What would a proof inside of HoTT look like? We will leave this as an open question.

5 Vector fields

If \(T:\ensuremath{\mathbb{M}}\to\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\) is a bundle of mere circles, then a vector field should consist of, in part, a choice of a point in each fiber:

On 1-paths \(p:x=_{\ensuremath{\mathbb{M}}_1}y\) \(X\) assigns a choice of pathover \(\pi:\mathsf{tr}(p)(x)=_{Ty}y\), which can also be thought of as a proof of pointedness of the transport map \(\mathsf{tr}(p)\).

The goal now is to recompute the total curvature in the context of some vector field \(X\) and obtain three values:

1. The total curvature, e.g. in the case of \(\ensuremath{\mathbb{O}}\) the value \(R^8\).

2. The total winding of \(X\), which will take the proof of pointedness around all faces in the domain of \(X\). Being a loop in a circle, this is an integer.

3. A pointed version of curvature, which couples the winding of \(X\) to the transport, which is a total function, and which produces a contractible pointed map, i.e. 0.

Once we have these, we will unpack how they provide a proof in HoTT of the Poincaré-Hopf theorem and the Gauss-Bonnet theorem.

5.1 Index of a vector field: subtracting curvature

Index should be an integer that computes a winding number “of the vector field” around a zero. Classically this is done in a local trivialization around a zero of the vector field, with a canonical flat connection associated to the trivialization (an isomorphism with a product bundle). We should therefore first look for a loop in one of our pointed fibers \((Tm, Xm)\). Let \(\pi_1,\ldots,\pi_k:L\to\ensuremath{\mathbb{M}}\) be a face enumerator with basepoint \(m:\ensuremath{\mathbb{M}}\) (Definition 20) and consider the loop \(\ell\stackrel{\mathrm{def}}{=}\ell_{L,1}\).

\(T\ell:Tm=Tm\) is the holonomy isomporphism of the loop, and it has flatness structure \(H\ell:T\ell=\ensuremath{\text{id}}_m\). The vector field assigns a dependent path over the loop (a loopover) \(X\ell:T\ell(Xm)=Xm\) which is not a closed loop in general. (Remember, this is the whole point of curvature: transporting around a loop does not produce a pointed isomorphism of the fiber.)

But notice that the flatness structure tells us exactly how to close the loopover and produce an honest loop in \((Tm,Xm)\), namely by evaluating \(H\ell\) at \(Xm\), giving \(H\ell(Xm):T\ell(Xm)=Xm\), which is of the same type as \(X\ell\). Forming the concatenation \(X\ell\cdot H\ell(Xm)^{-1}:Xm=Xm\) gives a term in the loop space \(\Omega_{Xm}(Tm)\simeq\ensuremath{\mathbb{Z}}\). Conceptually, we have asked how much the vector field swirls as it moves around the loop not counting any swirl of the parallel transport. The concatenation \(-\cdot H\ell(Xm)^{-1}\) is a subtraction of the effect of curvature.

We have constructed a map \(\Omega_m(\ensuremath{\mathbb{M}})\to \Omega_{Xm}(Tm)\):

5.2 Equality of total index and total curvature

Identification with Euler characteristic