In this post, I would want to present you two things:

- the small library about colimits that I formalized in Coq,
- a construction of the image of a function as a colimit, which is essentially a sliced version of the result that Floris van Doorn talked in this blog recently, and further improvements.

I present my hott-colimits library in the first part. This part is quite easy but I hope that the library could be useful to some people. The second part is more original. Lets sketch it.

Given a function we can construct a diagram

where the HIT is defined by:

HIT KP f := | kp : A -> KP f | kp_eq : forall x x', f(x) = f(x') -> kp(x) = kp(x').

and where is defined recursively from . We call this diagram the iterated kernel pair of . The result is that the colimit of this diagram is , the image of ( is the homotopy fiber of in ).

It generalizes Floris’ result in the following sense: if we consider the unique arrow (where is Unit) then is the one-step truncation of and the colimit is equivalent to the truncation of .

We then go further. Indeed, this HIT doesn’t respect the homotopy levels at all: even is the circle. We try to address this issue considering an HIT that take care of already existing paths:

HIT KP' f := | kp : A -> KP' f | kp_eq : forall x x', f(x) = f(x') -> kp(x) = kp(x'). | kp_eq_1 : forall x, kp_eq (refl (f x)) = refl (kp x)

This HIT avoid adding new paths when some elements are already equals, and turns out to better respect homotopy level: it at least respects hProps. See below for the details.

Besides, there is another interesting thing considering this HIT: we can sketch a link between the iterated kernel pair using and the Čech nerve of a function. We outline this in the last paragraph.

All the following is joint work with Kevin Quirin and Nicolas Tabareau (from the CoqHoTT project), but also with Egbert Rijke, who visited us.

All our results are formalized in Coq. The library is available here:

https://github.com/SimonBoulier/hott-colimits

# Colimits in HoTT

In homotopy type theory, Type, the type of all types can be seen as an ∞-category. We seek to calculate some homotopy limits and colimits in this category. The article of Jeremy Avigad, Krzysztof Kapulkin and Peter LeFanu Lumsdaine explain how to calculate the limits over graphs using sigma types. For instance an equalizer of two function and is .

The colimits over graphs are computed in same way with Higher Inductive Types instead of sigma types. For instance, the coequalizer of two functions is

HIT Coeq (f g: A -> B) : Type := | coeq : B -> Coeq f g | cp : forall x, coeq (f x) = coeq (g x).

In both case there is a severe restriction: we don’t know how two compute limits and colimits over diagrams which are much more complicated than those generated by some graphs (below we use an extension to “graphs with compositions” which is proposed in the exercise 7.16 of the HoTT book, but those diagrams remain quite poor).

We first define the type of graphs and diagrams, as in the HoTT book (exercise 7.2) or in hott-limits library of Lumsdaine *et al.*:

Record graph := { G_0 :> Type ; G_1 :> G_0 -> G_0 - Type }.

Record diagram (G : graph) := { D_0 :> G -> Type ; D_1 : forall {i j : G}, G i j -> (D_0 i -> D_0 j) }.

And then, a cocone over a diagram into a type :

Record cocone {G: graph} (D: diagram G) (Q: Type) := { q : forall (i: G), D i - X ; qq : forall (i j: G) (g: G i j) (x: D i), q j (D_1 g x) = q i x }.

Let be a cocone into and be a function . Then we can extend to a cocone into by postcomposition with . It gives us a function

A cocone is said to be universal if, for all other cocone over the same diagram, can be obtained uniquely by extension of , that we translate by:

Definition is_universal (C: cocone D Q) := forall (Q': Type), IsEquiv (postcompose_cocone C Q').

Last, a type is said to be a colimit of the diagram if there exists a universal cocone over into .

## Existence

The existence of the colimit over a diagram is given by the HIT:

HIT colimit (D: diagram G) : Type := | colim : forall (i: G), D i - colimit D | eq : forall (i j: G) (g: G i j) (x: D i), colim j (D_1 g x) = colim i x

Of course, is a colimit of .

## Functoriality and Uniqueness

### Diagram morphisms

Let and be two diagrams over the same graph . A morphism of diagrams is defined by:

Record diagram_map (D1 D2 : diagram G) := { map_0: forall i, D1 i - D2 i ; map_1: forall i j (g: G i j) x, D_1 D2 g (map_0 i x) = map_0 j (D_1 D1 g x) }.

We can compose diagram morphisms and there is an identity morphism. We say that a morphism is an equivalence of diagrams if all functions are equivalences. In that case, we can define the inverse of (reversing the proofs of commutation), and check that it is indeed an inverse for the composition of diagram morphisms.

### Precomposition

We yet defined forward extension of a cocone by postcomposition, we now define backward extension. Given a diagram morphism , we can make every cocone over into a cocone over by precomposition by . It gives us a function

We check that precomposition and postcomposition respect the identity and the composition of morphism. And then, we can show that the notions of universality and colimits are stable by equivalence.

### Functoriality of colimits

Let be a diagram morphism and and two colimits of and . Let’s note and the universal cocone into and . Then, we can get a function given by:

We check that if is an equivalence of diagram then the function given by is well an inverse of .

As a consequence, we get:

The colimits of two equivalents diagrams are equivalent.

### Uniqueness

In particular, if we consider the identity morphism we get:

Let and be two colimits of the same diagram, then: .

So, if we assume univalence, the colimit of a diagram is truly unique!

## Commutation with sigmas

Let be a type and, for all , a diagram over a graph . We can then build a new diagram over whose objects are the and functions are induced by the identity on the first component and by on the second one. Let’s note this diagram.

Seemingly, from a family of cocone , we can make a cocone over into .

We proved the following result, which we believed to be quite nice:

If, for all , is a colimit of , then is a colimit of .

# Iterated Kernel Pair

## First construction

Let’s first recall the result of Floris. An attempt to define the propositional truncation is the following:

HIT {_} (A: Type) := | α : A -> {A} | e : forall (x x': A), α x = α x'.

Unfortunately, in general is not a proposition, the path constructor is not strong enough. But we have the following result:

Let be a type. Let’s consider the following diagram:

Then, is a colimit of this diagram.

Let’s generalize this result to a function (we will recover the theorem considering the unique function ).

Let . We note the colimit of the kernel pair of :

where the pullback is given by .

Hence, is the following HIT:

Inductive KP f := | kp : A -> KP f | kp_eq : forall x x', f(x) = f(x') -> kp(x) = kp(x').

Let’s consider the following cocone:

we get a function by universality (another point of view is to say that is defined by ).

Then, iteratively, we can construct the following diagram:

where and .

The iterated kernel pair of is the subdiagram

We proved the following result:

The colimit of this diagram is , the image of .

The proof is a slicing argument to come down to Floris’ result. It uses all properties of colimits that we talked above. The idea is to show that those three diagrams are equivalent.

Going from the first line to the second is just apply the equivalence (for ) at each type. Going from the second to the third is more involved, we don’t detail it here. And is well the colimit of the last line: by commutation with sigmas it is sufficient to show that for all , is the colimit of the diagram

which is exactly Floris’ result!

The details are available here.

## Second construction

The previous construction has a small defect: it did not respect the homotopy level at all. For instance is the circle . Hence, to compute (which is of course), we go through very complex types.

We found a way to improve this: adding identities!

Indeed, the proof keeps working if we replace by which is defined by:

Inductive KP' f := | kp : A -> KP' f | kp_eq : forall x x', f(x) = f(x') -> kp(x) = kp(x'). | kp_eq_1 : forall x, kp_eq (refl (f x)) = refl (kp x)

can be seen as a “colimit with identities” of the following diagram :

(♣)

with .

In his article, Floris explains that, when then and are not equal. But now they become equal: by path induction we bring back to . That is, if two elements are already equal, we don’t add any path between them.

And indeed, this new HIT respects the homotopy level better, at least in the following sense:

- is (meaning that the one-step truncation of a contractible type is now ),
- If is an embedding (in the sense that is an equivalence for all ) then so is . In particular, if is hProp then so is (meaning that the one-step truncation of an hProp is now itself).

## Toward a link with the Čech nerve

Although we don’t succeed in making it precise, there are several hints which suggest a link between the iterated kernel pair and the Čech nerve of a function.

The Čech nerve of a function is a generalization of his kernel pair: it is the simplicial object

(the degeneracies are not dawn but they are present).

We will call n-truncated Čech nerve the diagram restricted to the n+1 first objects:

(degeneracies still here).

The kernel pair (♣) is then the 1-truncated Čech nerve.

We wonder to which extent could be the colimit of the (n+1)-truncated Čech nerve. We are far from having such a proof but we succeeded in proving :

- That is the colimit of the kernel pair (♣),
- and that there is a cocone over the 2-trunated Čech nerve into

(both in the sense of “graphs with compositions”, see exercise 7.16 of the HoTT book).

The second point is quite interesting because it makes the path concatenation appear. We don’t detail exactly how, but to build a cocone over the 2-trunated Čech nerve into a type , must have a certain compatibility with the path concatenation. doesn’t have such a compatibility: if and , in general we do **not** have

in .

On the contrary, **have** the require compatibility: we can prove that

in .

( has indeed the type because is and then .)

This fact is quite surprising. The proof is basically getting an equation with a transport with apD and then making the transport into a path concatenation (see the file *link_KPv2_CechNerve.v* of the library for more details).

## Questions

Many questions are left opened. To what extent is linked with the (n+1)-truncated diagram? Could we use the idea of the iterated kernel pair to define a groupoid object internally? Indeed, in an ∞-topos every groupoid object is effective (by Giraud’s axioms) an then is the Čech nerve of his colimit…

Sorry for my late response, I’ve only had time to read it now.

This is very nice. I like the result about commutation of sigma and colimits. Egbert and I worked on a similar problem, and we were stumped by it. The problem we worked on was also commutation of sigma’s and colimits, but a more general case, where the type is also a colimit, and you want to commute the sigma with both these colimits. Have you tried that problem with any success?

Another question: If you define the propositional truncation with KP’ instead of KP, do you get a new result for eliminating out of a propositional truncation (for example an easier universal property if you eliminate from the propositional truncation to a set)?

There is a morphism from your diagram to the

`KP'`

-diagram (ok, this could become confusing. Let’s say “Floris-diagram” for yours with {}, and “Simon-diagram” for the one with`KP'`

but where the codomain of`f`

is the unit type). So, there is a morphism from the Floris-diagram to the Simon-diagram, which means that cocones for the Simon-diagram are at least as hard to define as cocones for the Floris-diagram. It’s also quite intuitive that the Simon-diagram gives probably an elimination principle that is harder to apply, simply because you need to construct more stuff.But I *do* think that, with the Simon-diagram, you get the simplified elimination principle when you eliminate from the propositional truncation into a 1-type. This is just because, if

`B`

is a 1-type, then maps from`KP'(A->1)`

already correspond to maps`‖A‖ -> B`

. This is a re-formulation of Proposition 2.3 in my paper. But I’m afraid for general n-types it again does not work in this way. (It works with the sequence that I have constructed here, but that’s another story.)Thanks for the observations. Nice to see your construction in a paper. I have to read it more carefully. So if I understand correctly, you’ve also fully formalized your construction? Can you point to the universal property you get in the Agda formalization?

I have formalized the main results, but I didn’t formulate the universal property explicitly. I have added an explicit proof that the colimit of the sequence is equivalent to the truncation – see the end of this file, maybe easier to read here (end) in the html version. From that, you get that the truncation has the same universal property as the colimit, but I didn’t make this a lemma in the formalization. (Btw, in the beginning of the last section in the pdf, p18, there is a paragraph “Consequences for the van Doorn sequence”. This is a cleaner write-up of the argument that I sketched for you in some email.)

Is your first question related to the flattening lemma (section 6.12 in the book)?

Yes, it is definitely related, in that the flattening lemma tells that the sigma-of-a-colimit is equivalent to *something*, but it doesn’t tell you that it is equivalent to a colimit-of-sigmas. It is not clear whether it is easier to prove whether *something* is equivalent to a colimit-of-sigmas or whether it is easier to do it directly without using the flattening lemma.

I guess I don’t know what you mean by a colimit-of-sigmas. The is the flattening lemma is basically the coequalizer of a couple of maps between sigmas, isn’t it?

This is the special case where we take a colimit over . Suppose we have a diagram over , which is a sequence of types with maps . Now suppose we also have a diagram over , which is a sequence of types with maps . Then we can form a new diagram over , which is the “sigma-diagram” of this data. It consists of sigma types with corresponding functions . With colimit-of-sigmas I mean the colimit of this diagram.

Great. Now in general we can construct the -colimit of a sequence with connecting maps as a coequalizer of two endomaps of , one of which is the identity and the other of which (call it ) is built out of .

Your also induces a family defined by , and your induces an endomap of this family lying over .

If is a family of equivalences , then we have an equifibered family over a parallel pair, and the flattening lemma applies. The defined there is the coequalizer of the above two induced endomaps of . But by associativity of sigmas, this is equivalent to the colimit of your , since the latter can be constructed as a coequalizer of two endomaps of . Therefore, the flattening lemma says that this colimit is equivalent to , where is the colimit of and is defined by -recursion from .

If does not conist of equivalences, then I don’t see how to define , so I don’t know what you would want to show the colimit of to be equivalent to.

Adding a comment here for the sake of passers-by: Egbert and Floris explained to me off-line that the question is indeed about the case when

gdoesnotconsist of equivalences, but the typeQis not defined in the naive way but rather by taking a colimit of all thePtypes.Thank you Floris.

I am afraid I will answer negatively to both of your questions…

For the first: In the non dependent case, is your problem the following?

Given two diagrams D1(i) and D2(i) (let’s say on the same graph), find another diagram D1xD2(i) such that colim D1xD2 = (colim D1) x (colim D2).

I believe that I tried to find something life that but was unable to do it…

For the second question: It would be nice! But we didn’t succeed… In particular, we didn’t succeed in proving any other property of truncation or connectedness than those that I presented.

I think that in the non-dependent case it indeed reduces to that problem. We’re doing it in the special case for diagrams over the natural numbers, but it is indeed very tricky.

Thanks for the nice post. I would like to add some thoughts, connections with other work, and also some guesses about your open questions.

As you say,

`KP`

is the sliced version of Floris’ one-step truncation. This is because`kp_eq`

is [the sliced version of] a weak-constancy-constructor. In the same way, your`kp_eq_1`

corresponds to [the sliced version of] what I call “first coherence condition” of a weakly constant function.Some background: In this article, I construct the type of coherently constant functions (between two types, say and ). This type of coherently constant functions consists of an infinite tower of coherence data (see also this post). Intuitively, each datum ensures that the proceeding one is well-behaved. A drawback is that this type of coherently constant functions basically requires semi-simplicial types (i.e. you cannot just write it down in HoTT). But you can consider the finite approximations.

The HIT-version of this would say that the (hypothetical) HIT with an infinite number of constructors is a non-recursive version of the propositional truncation (but we cannot really write down this HIT).

The finite approximations of this HIT (which, as you say, “preserve homotopy levels a bit better”) have also been discussed in this thread, started by Gershom.

Now, in Floris’ construction, you don’t need any of the higher coherence data; instead, you only use a very low approximation and then iterate it. This low approximation is Floris’ one-step truncation (which has a couple of other names as well, e.g. it is Martin and Thierry’s “generalised circle S). Gershom called this

`UMP_-1`

. You can then go on and consider`UMP_n`

for whatever number`n`

you like. Your`KP'`

is really the sliced version of`UMP_0`

! This is because the constructor`kp_eq_1 : forall x, kp_eq (refl (f x)) = refl (kp x)`

could also be written in its expanded form, i.e. as

`kp_eq_1 : forall x y z, forall p : f(x) = f(y), forall q : f(y) = f(z), kp_eq (p) . kp_eq(q) = kp_eq(p.q)`

I think the expanded form is nicer because it’s easier to see what the next levels are, but if you stop here, then you can of course just use the shorter contracted form.

I would not view this constructor

`kp_eq_1`

as “adding identities”, because these identities are not well-behaved, unfortunately. From my point of view, it’s really simply “one more coherence level”. I say they are not well-behaved because you don’t have the next coherence level (this next level is exactly the “compatibility” that you talk about in your post, but I think it’s really easier to understand it in the expanded version). It’s nice that you get this next coherence level if you iterate, but I don’t find it surprising because we have seen in Floris’ construction that you can derive coherence levels by iterating even if we start from the “even lower” approximation “{-}”.The sections “First construction” and “Second construction” of your post could be extended: you could consider a “Third construction” with

`KP''`

, “fourth construction” with`KP'''`

and so on, adding one more coherence in every step (i.e`KP''`

is`KP'`

where the next coherence level, i.e. your “compatibility”, is added as a constructor). In other words, you would use the sliced versions of`UMP_n`

. The thing with all of these is that finite iterations are not very well-behaved, it just all becomes right if you iterate infinitely often – at least, that’s my current understanding. If you add more coherences, then the finite cases become a bit better in the sense that they preserve low truncation levels, but without restriction of the homotopy level, they are still not well-behaved.So, my guess is that

`KP'`

is not the colimit of the truncated Čech nerve because it’s not coherent, while the “real” colimit should be coherent. I would expect that you could get the colimit if you do the whole construction with`KP''''`

, where the number of`'''`

corresponds to the size of the diagram that you want to consider.Pingback: Reflexive graph quotients are pushouts | Egbert RIJKE