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

1. the small library about colimits that I formalized in Coq,
2. 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:

1. is (meaning that the one-step truncation of a contractible type is now ),
2. 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 :

1. That is the colimit of the kernel pair (♣),
2. 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…

In this post, I want to talk about a construction of the propositional truncation of an arbitrary type using only non-recursive HITs. The whole construction is formalized in the new proof assistant Lean, and available on Github. I’ll write another blog post explaining more about Lean in August.

Continue reading →