\(\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 Combinatorial manifolds

3.1 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 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.

3.2 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.3 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:

3.4 New in 2025: Adding and removing points from polygons

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_{ij}:v_i=v_j\) where \(j=i+1\) except for \(e_{n1}\).

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.

In general, given functions \(\phi,\psi:A\to B\) between two arbitrary types, and the type family of paths \(\alpha:A\to\mathcal{U}, a:A\mapsto \phi(a)=\psi(a)\), transport is given by concatenating the three obvious paths: \[\mathsf{tr}(p:a=a')(q:\phi(a)=\psi(a)) = \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')\).

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}\). ◻

With the lemma we can prove that all the polygons are merely equal to \(S^1\) and hence are in \(\mathrm{EM}(\ensuremath{\mathbb{Z}},1)\).

With the lemma we can define a function on polygons that inserts \(k\) vertices between each original vertex, providing us a map \(m_k:C_n\to C_{kn}\).

With \(m_k\) we can start with a surface that has pentagonal plus hexagonal links, and apply \(m_6\) to the pentagons and \(m_5\) to the hexagons, and have a type family that is the tangent bundle (because it comes from the link) but where every fiber has 30 vertices.

3.5 New in 2025: The classical adding of angles is given by horizontal composition

Let me start a new discussion of composing faces. Consider Figure 6 and the diamond on the left. Denote the clockwise triangular path around the left triangle by \(bcab\), and around the right by \(bdcb\). These are loops at \(b\). Say that the tangent map \(T\) satisfies \(T(bcab)=R\) where \(R\) is rotation by 1 notch in the 4-sided polygon \(Tb\), and similarly \(T(bdcb)=R\) as well.

Since \(bcab\) has a filler 2-cell, which we will call \(f_1\), we know that \(T(f_1)=H\) where \(H:R=\ensuremath{\text{id}}\) is a path in \(\mathop{\mathrm{Aut}}(Tb)\) from \(R\) to the identity. Similarly for \(f_2\), the filler for \(bdcb\).

The two faces can be horizontally composed giving \(f_1\star f_2\), which fills the diamond \(bdcab\). It also gives us a way to combine the two homotopies into a single homotopy \(H\star H:R^2=\ensuremath{\text{id}}\).

In this way, given an explicit ordering of the faces (a “plan” for visiting all faces of the manifold), we can “sum” the curvature. For our ocatahedron where each triangle produces a rotation of \(R\), we’d get \(R^8\).

This sum will be very similar to concatenating edges that circulate once around each face.

3.6 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.7 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 7), then we can define an operation that combines the combinatorics of simplices with the higher groupoid operations generated by our HIT.

Consider Figure 7 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 8 illustrates the equivalence.

Proof. We will prove that concatenating two faces of \(\ensuremath{\mathbb{M}}\) as in Figure 7 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. ◻