### HoTT Cohesion – Exercise I

#### Posted by Urs Schreiber

In the discussion of a previous entry finally the Coq-formulation of the axioms of cohesion in homotopy type theory (HoTT) materialized (thanks to prodding by David Corfield and expertise by Mike Shulman). See

With these axioms in hand, I would now enjoy to see the machinery put to work. I’ll try to take this as an occasion to learn HoTT and its coding as we go along. Currently I still know next to nothing, and so I am hoping that by stating in public the exercises that I pose to myself, I might get some hints from the experts and some help from whoever likes to join in.

The following should be a very basic and nevertheless interesting first exercise to warm up.

**Exercise I a)** Give the Coq-code that describes from a connected type – to be denoted

```
BG : Type
```

the homotopy fiber type of

```
map_from_flat BG : flat BG -> BG
```

to be denoted

```
flat_dR BG : Type
```

(The de Rham coefficient object.)

**Exercise I b)** Give the Coq-code that describes the canonical term

```
theta : G -> flat_dR BG
```

where `G`

is the identity type

```
Id_BG pt pt : Type
```

(This $\theta$ formalizes the notion of the Maurer-Cartan form on $G$.)

**Hint:** use uuo.v.

**Warning:** I assume that comprehensive code for the notion of connected objects is more involved than the rest of the exercise, so probably it is helpful to first adopt a more ad hoc treatment.

## Re: HoTT Cohesion – Exercise I

Here is my code :-) (and the

`Cohesive_Topos`

module I’m using is here)Note that I needed to use univalence in order to prove that the point is discrete (and I needed this to build a base point of $\flat BG$ from a base point of $BG$). Perhaps this is not necessary.

By the way, what do you mean by a connected object? Your link only defines a $n$-connected object. Do you mean $0$-connected? (in my code I just assumed that $BG$ is (constructively) inhabited).