\(\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.4 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 Polytopes and combinatorial manifolds

We will use two types of classical combinatorial structures: abstract polytopes and combinatorial manifolds. The latter is a subtype of the former. Abstract polytopes (or just “polytopes” in this note) encompass polygons, polyhedra, and higher-dimensional versions. They exclude certain undesirable shapes such as two triangles that meet at one vertex. But they aren’t necessarily simplicial either:

Minimal HITs:

def S1:
base: S1
loop: base=base

def S2:
N: S2
surf: refl_N = refl_N

def torus:
b:torus
p,q:b=b
donut:p.q=q.p


the map R (realization) R(S2):U lossy map

R(C_4) has an equivalence to R(S1)
perhaps this is R(the map C_4->S1, the strict one)
C_4->S1 is a strict map
S1->C_4 is non-strict, uses generated data, uses data from R(C_4)

def OO:
6 vertices
12 edges
8 faces

f:S2->OO 
T:OO->EM(Z,1)

def OO_w:
5 vertices
8 edges
5 faces: four bottom triangles, and a square refl_b=loop "brgob"

g:S2->OO_w

compose f and g^{-1} to give OO equiv OO_w

Tof(base) is (C_4, is_equiv_s1)
inside this is a twice rotation around C_4 and a homotopy to id(C_4)

"strict morphism of HITs": ctors to ctors

Imagine only having X:U, or X:*-> U

Claim: we cannot see the one-notch "90 degree" rotation of C_4 at the level of types.

-- Connections --
Type X w/ 1-skel X_1
HIT gives skeletal filtration
functions naturally given as per-skeleton steps
there are constraints/obstructions:
obstruction to extend map T from vertices a, b to path e:a=b is that T(a) and T(b) are in same connected component
say 2-cell F contracts a loop L: F:L=refl_v some vertex v
we have a choice of v for each face F
then T(F) must be in same component as refl_v (refl_v:\pi_1 X with basepoint v)
T(F) is merely refl, and holonomy is merely refl, and connection on this face F is merely flat
curvature is a function from 2-cells to \pi_1(X,v)
T(v):U
T(L):T(v)=T(v)

T(F):refl_{T(v)}=T(L)
the class ||T(L)||:\pi_1(U,T(v)) is an obstruction to having T(F), to extending T to F

The hierarchy of maps extending to higher skeletons, which we call connections of dimension 1, 2, etc.
This works for ANY HIT.
The combinatorial manifold structure is just one special case that gives me a specific map T.

3.1 Polytopes

The diamond condition captures that two edges meet at a vertex, two faces meet at one edge, and so on. See the Hasse diagram (a graph of the poset with rank represented on the \(y\)-axis) of a tetrahedron in Figure 2 and the square pyramid (which will arise later as an octahedron minus its south pole) in Figure 3.

Next we will map abstract polytopes to higher inductive types. The poset structure will generate the paths, so the rank will correspond to the dimension. But as usual in a HIT we will need to make a choice of direction for each path constructor, which wasn’t necessary in the polytope setting. We will restrict to dimension at most 2.

If \(Z:\mathcal{U}\) is a type then to define a map

3.2 Combinatorial manifolds

We will adapt to higher inductive types in a straightforward manner the classical construction of combinatorial manifolds. See for example the classic book by Kirby and Siebenmann (Kirby & Siebenmann, 1977). These are a subclass of simplicial complexes.

Note that we don’t require all subsets of \(M_0\) to be included – that would make \(M\) an individual simplex. A simplicial complex is a family of simplices that are identified along various faces.

The link is all the neighboring vertices of \(v\) and the codimension 1 faces joining those to each other. See for example Figure 4.

In a 2-dimensional combinatorial manifold the link is a polygon. See Figures 5, 6, and 7 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.

3.3 Higher inductive combinatorial manifolds

We will convert a simplicial complex \(M\) of dimension at most 2 to a higher inductive type, in two steps.

We will assume there is a formal theory of such HITs, and that at least up to dimension 2 there are no obstructions to simply copying over the combinatorial data to the HIT constructors. For recent work on HITs see for example David Wärn’s discussion of pushouts (Wärn, 2024).

We’re making the distinction between \(\mathcal{H}\) and \(\mathcal{R}\) because we will mostly study functions and phenomena on \(\mathcal{H}(M)\) for some simplicial complex \(M\).

3.4 Polygons

We will now start looking at some examples, first by defining a type that is important both for the domain and the codomain of mere circles: a square.

The standard HoTT circle itself is a non-example of a combinatorial manifold since it lacks the second vertex of the edge:

Nonetheless, all polygons are equivalent to each other and to \(S^1\).

Proof. First we need to construct a term \(4e:\prod_{x:C_4}s_1(\ell(x))=x\) by induction on \(C_4\), by defining terms

1. \(4ei:s_1(\ell(c_i))=c_i\)

2. \(4eij:\mathsf{apd}(c_ic_j)(4ei)=4ej\), i.e. \(4eij: s_1(\ell(c_ic_j))^{-1}\cdot 4ei\cdot c_ic_j=4ej\).

where in the second goal we used a result about \(\mathsf{apd}\) on transport (HoTT Book (Univalent Foundations Program, 2013) Theorem 2.11.3). These goals are fulfilled by

• \(4e1=\ensuremath{\mathsf{refl}}_{c_1}\)

• \(4e2={c_1c_2}\)

• \(4e3={c_1c_2\cdot c_2c_3}\)

• \(4e4={c_1c_2\cdot c_2c_3\cdot c_3c_4}\)

• \(4e12=(c_1c_2\cdot c_2c_3\cdot c_3c_4\cdot c_4c_1)^{-1}\cdot(-)\)

• \(4e23=\ensuremath{\mathsf{refl}}_{c_1c_2\cdot c_2c_3}\)

• \(4e34=\ensuremath{\mathsf{refl}}_{c_1c_2\cdot c_2c_3\cdot c_3c_4}\)

• \(4e41=4e12\).

Next we need a term \(e4:\prod_{y:S^1}\ell(s_1(y))=y\) by induction on \(S^1\), by defining.

1. \(e4b:\ell(s_1(\mathsf{base}))=\mathsf{base}\)

2. \(e4l:\mathsf{apd}(\mathsf{loop})(e4b)=e4b\), i.e. \(e4l:\ell(s_1(\mathsf{loop}))^{-1}\cdot e4b\cdot e4b\).

These goals are fulfilled by

• \(e4b=\ensuremath{\mathsf{refl}}_{\mathsf{base}}\)

• \(e4l=\ensuremath{\mathsf{refl}}_{\mathsf{loop}}\).

 ◻

A different approach might be to prove that \(C_n\simeq C_{n-1}\) by removing just one vertex, and seeing that the argument generates equivalences between any polygon, or a polygon and \(S^1\).

Recalling that terms of \(\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\) are pairs: a type, and a mere equivalence with \(S^1\), we have:

Given some other square \(abcd\) and an equivalence with \(C_4\), we get via univalence a path in \(\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\). This includes automorphisms of \(C_4\), for example \(R\). Furthermore there is a homotopy from \(R\) to the identity, which give a 2-path \(\ensuremath{\mathsf{refl}}_{C_4}=R\) in the universe.

Real-world triangulations of surfaces will often have links whose number of vertices varies across the surface. For example we can see hexagons and pentagons in Figure 5. This presumably introduces only a minor practical inconvenience and doesn’t materially affect the discussion to come.

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

We will create our first combinatorial surface, a 2-sphere. We will adopt the convention that a subscript indicates the dimension of a subskeleton of a complex. For instance, we have \(\mathsf{base}:S^1_0\).

We have obvious maps \(\ensuremath{\mathbb{O}}_0\xrightarrow[]{i_0} \ensuremath{\mathbb{O}}_1\xrightarrow[]{i_1} \ensuremath{\mathbb{O}}\) that include each skeleton into the next-higher-dimensional skeleton.

3.6 Groupoid operations on higher inductive combinatorial manifolds

Let \(M:\mathsf{SimpCompSet_2}\) be a combinatorial 2-manifold and \(\ensuremath{\mathbb{M}}\stackrel{\mathrm{def}}{=}\mathcal{H}(M):\mathsf{CombMfd_2}\) the corresponding higher inductive type. \(\ensuremath{\mathbb{M}}\) has triangular 2-faces just as \(M\) does, except they are 2-paths in the HoTT sense. If two faces \(bca\) and \(bdc\) share the edge \(bc\) (see Figure 8), then we can define an operation that combines the combinatorics of simplices with the higher groupoid operations generated by our HIT.

Consider Figure 8 and the 2-paths \(bac: ba\cdot ac=bc\) and \(bdc: bd\cdot dc = bc\). The 2-path concatenation \(bac\cdot bdc^{-1}\) is a path in \(ba\cdot ac = bd\cdot dc\). And from there we see we have a 4-gon \(abdc:\ensuremath{\mathsf{refl}}_b=\ensuremath{\mathsf{refl}}_b\). In this way we can concatenate faces across common boundaries once we choose a common vertex (in this case \(b\)).

We will have two use cases for this operation. The first is to consider the concatenation of all the faces of \(\ensuremath{\mathbb{M}}\), i.e. a term \(f_\ensuremath{\mathbb{M}}:\ensuremath{\mathsf{refl}}_a=\ensuremath{\mathsf{refl}}_a\) corresponding to \(\ensuremath{\mathbb{M}}\) itself. This will play the role of the “fundamental homology class” from classical topology, which is an object on which 2-forms can be evaluated to compute their value on the whole manifold.

Of course there are many choices in this definition of total face!

The second use case for concatenating faces is to create a HIT related to \(\ensuremath{\mathbb{M}}\) but without some of the point constructors. Figure 9 illustrates the equivalence.

Proof. We will prove that concatenating two faces of \(\ensuremath{\mathbb{M}}\) as in Figure 8 produces an equivalent type. Let \(A\) be the constructor given on the left that includes the edge \(bc\), and \(B\) the constructor on the right. We will define functions on constructors. Let \(f:A\to B\) be

• \(f(a:A)=a:B, f(b)=b, f(c)=c, f(d)=d\)

• \(f(ab)=ab, f(bd)=bd, f(dc)=dc, f(ca)=ca\)

• \(f(bc)=bdc\)

• \(f(abc)=abcd\)

• \(f(bdc)=\ensuremath{\mathsf{refl}}_{bd\cdot dc}\)

which “squishes the right face onto its right >-shaped boundary.” In the other direction let \(g:B\to A\) be the inclusion of all the constructors of dimension 1 and 2, and set \(g(abdc)=abc*bdc\), which denotes the concatenation operation across the shared edge.

We must provide a term \(gf:\prod_{x:A}g(f(x))=x\) which requires supplying four paths, five pathovers, and two faceovers. The four paths are \(\ensuremath{\mathsf{refl}}_a\), \(\ensuremath{\mathsf{refl}}_b\), \(\ensuremath{\mathsf{refl}}_c\) and \(\ensuremath{\mathsf{refl}}_c\). Four of the pathovers are \(\ensuremath{\mathsf{refl}}_{ab}\), \(\ensuremath{\mathsf{refl}}_{bd}\), \(\ensuremath{\mathsf{refl}}_{dc}\), \(\ensuremath{\mathsf{refl}}_{ca}\). It remains to find terms

1. \(\mathit{gfbc}:\mathsf{apd}(bc)(\ensuremath{\mathsf{refl}}_b)=\ensuremath{\mathsf{refl}}_c\)

2. \(\mathit{gfabc}:\mathsf{apd}(abc)(\ensuremath{\mathsf{refl}}_{ab}\cdot \mathit{gfbc}\cdot \ensuremath{\mathsf{refl}}_{ca})=\ensuremath{\mathsf{refl}}_{\ensuremath{\mathsf{refl}}_a}\), i.e. \(\mathit{gfabc}:g(f(abc))^{-1}\cdot (\ensuremath{\mathsf{refl}}_{ab}\cdot \mathit{gfbc}\cdot \ensuremath{\mathsf{refl}}_{ca})\cdot abc = \ensuremath{\mathsf{refl}}_{\ensuremath{\mathsf{refl}}_a}\)

3. \(\mathit{gfbdc}:\mathsf{apd}(bdc)(\ensuremath{\mathsf{refl}}_{bd}\cdot \ensuremath{\mathsf{refl}}_{dc}\cdot \mathit{gfbc}^{-1})=\ensuremath{\mathsf{refl}}_{\ensuremath{\mathsf{refl}}_b}\), i.e. \(\mathit{gfbdc}:g(f(bdc))^{-1}\cdot (\ensuremath{\mathsf{refl}}_{bd}\cdot \ensuremath{\mathsf{refl}}_{dc}\cdot \mathit{gfbc}^{-1})\cdot bdc\)

which are supplied by

1. \(cbd:cb\cdot bd\cdot dc=\ensuremath{\mathsf{refl}}_c\)

2. \(\ensuremath{\mathsf{refl}}_{\ensuremath{\mathsf{refl}}_{\ensuremath{\mathsf{refl}}_a}}\)

3. \(\ensuremath{\mathsf{refl}}_{\ensuremath{\mathsf{refl}}_{\ensuremath{\mathsf{refl}}_b}}\).

We must also provide a term \(\mathit{fg}:\prod_{x:B}f(g(x))=x\) which is \(\ensuremath{\mathsf{refl}}\) on all constructors. ◻

4 Connections and vector fields

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 10 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 \(T\) on concatenations of faces

Continuing with the classical analogies, we should seek a way to concatenate the curvature on two or more faces. This would correspond to integrating the curvature 2-form over a larger 2-cell, including integrating over a total face to compute total curvature. Look again at Figure 8 where we concatenated two faces that share an edge. HoTT maps respect groupoid operations, so we have \(T_2(abc\cdot bdc) = T_2(abdc)\). We can double-check this by comparing transport around a 4-gon like \(wbyr\) to a path that traverses each face.

Proof. Both are equal to \(R^2\) acting to permute \(\{b, r, g, o\}\) to \(\{g, o, b, r\}\). ◻

Similarly transport around the other vertical wedges \(wryg\), \(wgyo\) and \(woyb\) are each \(R^2\), and the four wedges can be composed to obtain \(R^8:\mathop{\mathrm{\mathsf{link}}}(w)=\mathop{\mathrm{\mathsf{link}}}(w)\). This implies that the total face given by concatenating all 8 faces (in this order) maps by \(T_2\) to \(R^8\) together with the homotopy that unwinds \(R^8\) to the identity.

What if we chose another strategy for concatenating the faces of \(\ensuremath{\mathbb{O}}\)? Suppose we concatenate all four triangles in the upper hemisphere with \(w\) as the basepoint, then move to \(y\) and compose the four southern triangles, then move back up to \(w\)?

Proof. Both are equal to \(R^4\). ◻

And therefore by concatenating the path on the left with the path on the right we see that this different ordering of the faces gives the same value of \(T_2\) as before, namely \(R^8\).

4.3 The torus

We can define a combinatorial torus as a similar HIT. This time each vertex will have six neighbors. So all the links will be merely equal to \(C_6\) which is a hexagonal version of \(C_4\). See Figure 11.

To help parse this figure, imagine instead Figure 12. We take this simple alternating-triangle pattern, then glue the left and right edges, then bend into Figure 11. The fact that each column in Figure 12 has four dots corresponds to the torus in Figure 11 having a square in front, diamonds in the middle, and a square in back.

This somewhat arbitrary and unfamiliar model of a torus has the helpful property that it is a combinatorial manifold that is somewhat minimal while still being representable by a donut shape. But the donut-shaped version suggests a very different connection than the flat model! Starting with the flat model, we can easily see how to define \(T_1\) by sliding a link rigidly along the page to the link of some adjacent vertex. Then we can see that transport around any loop is the identity and so \(T_2\) is always the identity (together with the homotopy \(\ensuremath{\mathsf{refl}}_\ensuremath{\text{id}}\) from the identity to itself). So if we imagine a way to visit every face like we did for the octahedron, starting and ending at some basepoint \(v\), we expect to see no net rotation at all of \(Tv\). Later we will call this “total curvature 0.”

The donut-shaped torus suggests a different connection, one determined by the embedding in 3-space that we have represented. But the easiest way to think about that bundle and its connection and curvature is to wait until we have a proof of the Poincaré-Hopf theorem, so that we can instead compute with a vector field.

4.4 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 be a partial function \(T_\bullet:\ensuremath{\mathbb{M}}\to\mathrm{EM_{\bullet}}(\ensuremath{\mathbb{Z}},1)\) that lifts \(T\). In other words, a pointing of some of the fibers. This aligns with the classical picture of a choice of nonzero vector at each point, except for some points where the vector field vanishes. So instead of having a notion corresponding to the full tangent vector space (one candidate for which would be the disk at each point, i.e. \(\mathop{\mathrm{\mathsf{link}}}\) plus its spokes and filler triangles) we are mapping some vertices to their circular fibers, and others to \(\star\). This lets us continue to work with \(\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\) instead of a type of tangent spaces.

Figure 13 illustrates what removing the preimage of \(\star\) looks like. The resulting type is no longer a combinatorial manifold, since it fails the condition about every point having a circular link.

where \(T_\bullet=\overline{T}\circ X\). Note that \(\exp\) is different from \(\ensuremath{\mathrm{pr}}_1\) since it spreads a fiber out onto the manifold. The composition \(\exp\circ X\) is a map \(\ensuremath{\mathbb{M}}\setminus Z\to \ensuremath{\mathbb{M}}\), and can be thought of as the flow of the vector field.

Let’s see a few examples.

4.5 Index of a vector field

Index should be an integer that computes a winding number “of the vector field” around a zero. We can compute an integer from a map by taking its degree, which is a construction we will assume that we have, for example using (Buchholtz & (Favonia), 2018), where they indeed require that degree agrees with winding number for maps \(S^1\to S^1\).

Proof. \(\mathsf{apd}(X_{\mathrm{spin}})(br) = \ensuremath{\mathsf{refl}}_{X_{\mathrm{spin}}(r)}\) and similarly for the other edges and for \(X_{\mathrm{down}}\). So \(\mathsf{apd}\) on the loop around the equator is the identity, which has index 1. ◻

If these vector fields both have index +1, what does index –1 look like? We can see an example on the torus with its downward vector field.

On the torus we can also consider both a spinning vector field and a downward vector field. Figure 16 shows one way to spin the torus, and in this case there are no zeros so the index is the degree of a map from the empty set, which is 0 (as it factors through a constant map).

Figure 17 shows a downward flow with four zeros. Although this is a picture of the flat torus, the vector field is derived from the shape of Figure 11 where we actually have a notion of up and down. We see at the position labeled (outer, top of diamonds), i.e. the top of the torus, an everywhere outward pointing vector field. At (outer, bottom of diamonds) we see an inward pointing vector field. But at (hole, top of diamonds), i.e. the top of the hole, we see something else. Imagine transport from the neighbor to the lower right to the neighbor below, then continuing clockwise around the link. If we assume that we define \(\mathsf{apd}\) on these edges to be counterclockwise rotation, then transport around the whole link has degree –1. Similarly for the zero at (hole, bottom of diamonds). Adding these four indexes we again get 0.

Summarizing what we’ve seen in our examples, vector fields with isolated zeros have an index, and this index tracks with the total curvature, and the Euler characteristic.

4.6 Equality of total index and total curvature

Here we are inspired by the classical proof of Hopf (Hopf, 1983), presented in detail in Needham (Needham, 2021).

Proof. The algorithm that visits each face in order always starts and ends at \(a\) and so we can skip any faces we wish, to obtain an ordering of face constructors for the remaining union of faces. ◻

Note that on \(\ensuremath{\mathbb{M}}\setminus Z\) the vector field \(X\) trivializes the bundle by mapping into the contractible type of pointed types over \(\mathrm{K}(\ensuremath{\mathbb{Z}},2)\). So \(X\simeq Y:\ensuremath{\mathbb{M}}\setminus Z\to (Ta,a)\), the fixed pointed circle in the fiber of the basepoint \(a\).

Proof. The ordering of faces \(\{f_i\}-\{f_{zk}\}\) provides an ordering of all the edges, say \(\{e_l\}\). Each edge appears an even number of times in this list, traversed in opposite directions, except those bounding a replacement face. These replacement-bounding edges are traversed an odd number of times and can be concatenated to traverse the boundary counterclockwise. Concatenation of paths in \(S^1\) is abelian, so \(Y(\{e_l\})\) cancels except on the boundary of the replacement faces, which gives a map from the disjoint union of boundary circles to \(Ta\), with each boundary circle traversed in the counterclockwise direction. The orientation gives the minus sign. ◻

Consider now the total face \(f_{\ensuremath{\mathbb{M}}_Z}\) of \(\ensuremath{\mathbb{M}}_Z\) and its ordering of faces \(\{f_i\}\). \(Y\) is only defined on some of these faces. We will define a new function on all the \(\{f_i\}\).

Because \(\mathsf{apd}\) uses both transport and the value of the vector field, it couples the connection with the vector field, hence the name. Of course in HoTT this coupling is built into the definition of \(\mathsf{apd}\), so that’s another reminder that we aren’t straying far from the foundations to find these geometrical concepts.

The fact that \(C\) is defined on all the faces, by using the value of the vector field only on the 1-skeleton of \(\ensuremath{\mathbb{M}}_Z\) where it was always defined, lets us make the final part of the argument.

Proof. The data of the total face provides an ordering of all the edges. Each edge appears an even number of times, traversed in opposite directions, including the edges in the replacement faces. Concatenation of paths in the polygon \(Ta\) is abelian, so the paths all cancel. ◻

\(C\) is similar to \(X\) and \(Y\) except that it is a total function. On any given edge it computes a path, that is, a homotopy from the function \(\mathsf{tr}\) to the function \(X\), which we can call “the difference between transport and the vector field on that edge.” We have found a way to add all these homotopies together to get 0. We can call this total “the difference between the total index and the total curvature.”

Recall now that we made some arbitrary choices in Definition 31 of an enumeration, and hence the function \(C\). But since \(C\) is unconditionally constant, the space of extra data is contractible.

The last step is to link this value to the Euler characteristic.

4.7 Identification with Euler characteristic

Here we only point the way. Combinatorial manifolds are intuitive objects that connect directly to the classical definition of Euler characteristic. We can argue using Morse theory, the study of smooth real-valued functions on smooth manifolds and their singularities. Classically the gradient of a Morse function is a vector field that can be used to decompose the manifold into its handlebody decomposition. This would be an excellent story to pursue in future work.

Imagine starting with a classical 2-manifold of genus \(g\) that has been triangulated. Stand it upright with the holes forming a vertical sequence. Now install a vector field that points downward whenever possible. This vector field will have a zero at the top and bottom, and one at the top and bottom of each hole. The top and bottom will have zeros of (classical) index 1, and zeros in the holes will have index –1. We include some sketches in the case of a torus (Figure 18). This illustrates how we obtain the formula for genus \(g\): \(\chi(M)=2-2g\). If we choose the triangulation so that the zeros are at vertices, we should be able to import that data into \(\mathsf{CombMfd_2}\) and reproduce the computation using the tools in this note.

5 Why this works

The arguments in this note flowed from a simple hypothesis: that \(\ensuremath{\mathsf{ap}}\) is analogous to \(d\), the exterior derivative. For example:

1. The derivative of a function is its action on tangent vectors, and this is an infinitesimal limit of its action on paths (though these classical “paths” consist of points, which is why \(df\) is entailed in the data of \(f\) on points).

2. Connections are not entailed in the data of a classical principal bundle. But they do answer the question: what does the bundle do on paths, i.e. how do we transport along a path? In this sense a connection might be the derivative of a bundle (and curvature the derivative of the connection).

3. In HoTT the transport function on fibers along a path is part of the type family. But of course if we are working inductively on a HIT, there is a moment after we define the family on points and before we define it on paths. In this sense connections are also extra structure.

4. de Rham complexes and cohomology are graded by dimension, but in HoTT this data is unified into a higher groupoid. Is a complex an infinitesimal limit of a groupoid?

5. The Leibniz rule (product rule) for real-valued smooth functions \(f,g:M\to\ensuremath{\mathbb{R}}\) is \(d(fg)=fdg + gdf\). In HoTT given functions \(f,g:M\to H\) for any type \(M\) and H-space \(H\) with multiplication \(*\), and path \(p:x=_M y\), we have \(f(p)* g(p) = (f(x)* g(p))\cdot (f(p)*g(y))\), where we say \(f(p)\) instead of \(\ensuremath{\mathsf{ap}}(p)(f)\). The Leibniz formula is so often treated as an axiom that it was surprising to the author to see this relationship with whiskering.

We will end with some discussion of classical connections and how to find more analogies with what we defined in previous sections.

5.1 Classical connections

Physicists call principal bundle automorphisms “gauge transformations”:

\(VP\) can be visualized as the collection of tangent vectors that point along the fibers. It should be clear that at each point of \(M\) the group \(G\) acts on \(VP\), sending vertical vectors to vertical vectors. In other words, \(\mathop{\mathrm{Aut}}P\) acts on \(VP\).

Being preserved by the action of \(G\) implies that the complementary horizontal subspaces in a given fiber of \(\pi:P\to M\) are determined by the splitting at any single point in the fiber. The action of \(G\) on this fiber can then push the splitting around to all the other points.

The utility and parsimony of this definition relates to the solvability of ordinary differential equations. We now have an isomorphism \(T_p\pi:H_pP\simeq T_{\pi(p)}M\) between each horizontal space and the tangent space below it in \(M\). This means that given a tangent vector at \(x:M\) and a point \(p\) in \(\pi^{-1}(x)\) we can uniquely lift the tangent vector to a horizontal vector at \(p\). We can also lift vector fields and paths in this way. To lift a path \(\gamma:[0,1]\to M\) you must specify a lift for \(\gamma(0)\) and then lift the tangent vectors of \(\gamma\) and prove that you can integrate the lift of that vector field upstairs in \(HP\).

Armed with the lifting of paths one immediately obtains isomorphisms between the fibers of \(P\): given a path in \(M\) we can map the starting point of a lift to the ending point. So the three constructions: the Ehresmann connection, the lifting of paths, and transport isomorphisms between fibers are all recapitulations of the structure that the connection adds to the bundle.

Moving now to HoTT, fix a combinatorial manifold \(\ensuremath{\mathbb{M}}:\mathsf{CombMfd_2}\) and a principal bundle \(T:\ensuremath{\mathbb{M}}\to\mathrm{K}(\ensuremath{\mathbb{Z}},2)\) with pullback \(P\). HoTT immediately provides a transport isomorphism of fibers from a path in \(\ensuremath{\mathbb{M}}\). Recall the theory of pathovers from Section 2.2. Does HoTT provide a lifting of paths in \(\ensuremath{\mathbb{M}}\) to paths in \(P\)? Given a path \(p:a=_\ensuremath{\mathbb{M}}b\) and a point \(\alpha:Ta\) above \(a\), we obtain a slightly constrained type of paths over \(p\) that begin at \(\alpha\) and end at \(\mathsf{tr}(p)(\alpha\). This is the type \(\mathsf{tr}(p)(\alpha)=\mathsf{tr}(p)(\alpha)\) which has the canonical term \(\ensuremath{\mathsf{refl}}\). In this sense HoTT has split the type of paths over \(p\) into pairs given by \(p\) itself and loops in \(\mathsf{tr}(p)(\alpha)=\mathsf{tr}(p)(\alpha)\) in \(Tb\). The term \(\ensuremath{\mathsf{refl}}\) could be called the horizontal lift of the path.

5.1.1 Gauge theory

Classically, given a bundle \(\pi:P\to M\) there is a space of connections \(\mathscr{A}(P)\). The group \(\mathop{\mathrm{Aut}}P\) acts on this space. For example, a gauge transformation that is constant in the neighborhood of a point (i.e. is given by multiplication by a fixed \(g:G\)) will not change the splitting, it will just shift the splitting rigidly along the fiber. But at the other extreme, a gauge transformation that is changing rapidly near a point will tilt the horizontal subspaces. The field of gauge theory begins with a study of this action, and of the quotient space \(\mathscr{A}(P)/\mathop{\mathrm{Aut}}P\).

In HoTT the gauge transformations are the type \(T\sim T\stackrel{\mathrm{def}}{=}\prod_{a:\ensuremath{\mathbb{M}}}Ta=Ta\), and rather than taking a quotient we have this group already emergent as paths in the space \(\ensuremath{\mathbb{M}}\to\mathrm{K}(\ensuremath{\mathbb{Z}},2)\).

Atiyah and Bott ( (Atiyah & Bott, 1983) equation 3.4) noted that the horizontal lift of two vector fields may have a vertical component when taking their Lie bracket, and identified this vertical component with the curvature. This forms an obstruction to splitting the Atiyah sequence of Lie algebras \[\text{vertical vector fields on }P \hookrightarrow \text{vector fields on }P \xrightarrow[]{\mathrm{lift}\circ\pi} \text{horizontal vector fields on }P.\] despite the splitting at the level of vector spaces.

In HoTT the analogue of bracketing two vector fields is (presumably) composing two paths \(p,q:a=_\ensuremath{\mathbb{M}}b\) to form a loop \(p\cdot q^{-1}\). The curvature can be seen by noting that the transport automorphism around the loop can be nontrivial, as discussed earlier in the note.

In this century mathematicians in HoTT and HoTT-adjacent fields sought an integrated Atiyah sequence, including Urs Schreiber (nLab authors, 2024) (Schreiber, 2006). This would be a Lie groupoidal version of the Atiyah sequence of Lie algebras. If a groupoid extension could be examined, the thinking went, a link could be sought to Schreier theory. Tying everything together we see that the desired groupoid is just the type \(P\) itself! To tie this with Schreier theory, we’ll recall that David Jaz Myers showed that we have an equivalence between the type of extensions of a group \(G\) by a group \(F\) and the actions of \(G\) on a delooping \(BF\): \[\mathrm{Ext}(G; F) \simeq (BG \,\cdot\!\to\mathop{\mathrm{BAut}}(BF))\] (see (Myers, 2022) Theorem 2.5.7). Our type of classifying maps \(\ensuremath{\mathbb{M}}\to\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\) can be seen as extensions of \(\pi_1(\ensuremath{\mathbb{M}})\) by the group \(\mathop{\mathrm{Aut}}S^1\). Such extensions that are furthermore principal fibrations are the oriented ones, as we showed before. What a lovely reframing of principal bundles.