### HoTT Cohesion – Exercise II

#### Posted by Urs Schreiber

Following “exercise I” on *Axiomatic Cohesion in Homotopy Type Theory*, where we saw (thanks to Guillaume Brunerie!) the HoTT-Coq code incantation of the Maurer-Cartan form on cohesive ∞-groups, it should now be a small step to conjure up something rather interesting: the definition of differential cohomology and the proof of its characteristic curvature exact sequence.

A writeup of this in the pseudocode formerly known as traditional mathematics is in section 2.3.14, p. 147 of *Differential Cohomology in a Cohesive ∞-Topos*. The following “exercises a) – d)” try to extract from this a core statement that should have a fairly straightforward implementation in HoTT-Coq (I hope!).

As before, this “exercise” is an exercise that I am posing myself. But also as before, it is more than likely that HoTT experts can solve this many orders of magnitudes quicker than I will. Don’t hesitate, there are plenty of further “exercises” along these lines waiting to get attention.

**Exercise II a)** In exericse I you found HoTT encoding of the fiber sequence

$G \stackrel{\theta}{\to} \flat_{dR}\mathbf{B}G \to \flat \mathbf{B}G \to \mathbf{B}G$

exhibiting the Maurer-Cartan form with values in de Rham coefficients inside the moduli ∞-stack of flat ∞-connections for a cohesive ∞-group $G$.

Take now $G = \mathbf{B}^n A$ to be an Eilenberg-MacLane object. Then, as before, the fiber sequence continues further to the left to yield

$\Omega \flat \mathbf{B}^{n+1} A \to \mathbf{B}^n A \stackrel{\theta}{\to} \flat_{dR} \mathbf{B}^{n+1}A \to \cdots \,.$

Show that $\flat$ – being a right adjoint – commutes with forming loop space objects and thus deduce the fiber sequence

$\flat \mathbf{B}^{n} A \to \mathbf{B}^{n} A \stackrel{\theta}{\to} \flat_{dR} \mathbf{B}^{n+1}A \,.$

**Exercise II b)** Consider a morphism into $\flat_{dR} \mathbf{B}^{n+1}A$ out of a 0-truncated object, to be denoted

$\Omega^{n+1}_{cl}(-,A) \to \flat_{dR} \mathbf{B}^{n+1} A \,.$

For later exercises we will demand the morphism thus denoted to be an effective epimorphism. But describing effective epiness will require more work than fits into the present exercise. Since the following parts c) and d) do not yet depend on this morphism being effective epi, we can ignore it for the moment and just assume some morphism out of a 0-truncated object. Extra credit, of course, if you manage to code effective epiness nevertheless!

**Exercise II c)** Define the type $\mathbf{B}^n A_{conn}$ – to be called the *moduli ∞-stack of A-principal n-connections* – as the ∞-pullback

$\array{ \mathbf{B}^n A_{conn} &\stackrel{F}{\to}& \Omega^{n+1}_{cl}(-,A) \\ \downarrow && \downarrow \\ \mathbf{B}^n A &\stackrel{\theta}{\to}& \mathbf{\flat}_{dR} \mathbf{B}^{n+1} A } \,.$

**Exercise II d)** Prove that the type thus defined fits into a fiber sequence of the form

$\flat \mathbf{B}^n A \to \mathbf{B}^n A_{conn} \stackrel{F}{\to} \Omega^{n+1}_{cl}(-,A)$

to be called the *$\infty$-stack refinement of the curvature exact sequence*.

**Remark.** The meat is in a). The rest should be straightforward consequences whose main point is to amplify the relevance of a).

## Re: HoTT Cohesion – Exercise II

I am unutterably amused by that remark. (-:

I wish I could be doing these exercises myself, but I just don’t have the time this month. )-: But I’m excited that they’re happening!