Colimits in HoTT

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 f_0:\ A \rightarrow B we can construct a diagram

picture:iterated-diag1.png

where the HIT \mathbf{KP} 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 f_{n+1} is defined recursively from f_n. We call this diagram the iterated kernel pair of f_0. The result is that the colimit of this diagram is \Sigma_{y:B} \parallel \mathbf{fib}_{f_0}\ y \parallel , the image of f_0 (\mathbf{fib}_{f_0}\ y is \Sigma_{x:A}\ f_0(x) = y the homotopy fiber of f_0 in y).
It generalizes Floris’ result in the following sense: if we consider the unique arrow f_0: A \rightarrow \mathbf{1} (where \mathbf{1} is Unit) then \mathbf{KP}(f_0) is \{ A \} the one-step truncation of A and the colimit is equivalent to \parallel A \parallel the truncation of A.

We then go further. Indeed, this HIT doesn’t respect the homotopy levels at all: even \{\mathbf{1}\} 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 \mathbf{KP'} 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 f and g is \Sigma_{x:A} f(x) = g(x).
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 Q :

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 C:\mathrm{cocone}\ D\ Q be a cocone into Q and f be a function Q \rightarrow Q'. Then we can extend C to a cocone into Q' by postcomposition with f. It gives us a function

\mathrm{postcompose} :\ (\mathrm{cocone}\ D\ Q) \rightarrow (Q': \mathrm{Type}) \rightarrow (Q \rightarrow Q')\rightarrow (\mathrm{cocone}\ D\ Q')

picture:pict-colim.png

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

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

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

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, \mathrm{colimit}\ D is a colimit of D.

Functoriality and Uniqueness

Diagram morphisms

Let D and D' be two diagrams over the same graph G. 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 m is an equivalence of diagrams if all functions m_i are equivalences. In that case, we can define the inverse of m (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 m: D \Rightarrow D' , we can make every cocone over D' into a cocone over D by precomposition by m. It gives us a function

\mathrm{precompose} :\ (D \Rightarrow D') \rightarrow (Q : \mathrm{Type})\rightarrow (\mathrm{cocone}\ D'\ Q) \rightarrow (\mathrm{cocone}\ D\ Q)

picture:pict-precompose.png

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 m: D \Rightarrow D' be a diagram morphism and Q and Q' two colimits of D and D'. Let’s note C and C' the universal cocone into Q and Q'. Then, we can get a function Q \rightarrow Q' given by:

(\mathrm{postcompose}\ C\ Q)^{-1}\ (\mathrm{precompose}\ m\ Q'\ C')

picture:pict-functo.png

We check that if m is an equivalence of diagram then the function Q' \rightarrow Q given by m^{-1} is well an inverse of Q \rightarrow Q' .
As a consequence, we get:

The colimits of two equivalents diagrams are equivalent.

Uniqueness

In particular, if we consider the identity morphism D \Rightarrow D we get:

Let Q_1 and Q_2 be two colimits of the same diagram, then: Q_1~\simeq~Q_2~ .

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

Commutation with sigmas

Let B be a type and, for all y:B , D^y a diagram over a graph G. We can then build a new diagram over G whose objects are the \Sigma_y D_0^y(i)\ and functions \Sigma_y D_0^y(i) \rightarrow \Sigma_y D_0^y(j) are induced by the identity on the first component and by D_1^y(g) : D_0^y(i) \rightarrow D_0^y(j) on the second one. Let’s note \Sigma D this diagram.

Seemingly, from a family of cocone C:\Pi_y\mathrm{cocone}\ D^y\ Q_y , we can make a cocone over \Sigma D into \Sigma_y Q_y.

picture:pict-sigma.png

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

If, for all y:B\ , Q_y is a colimit of D_y, then \Sigma_y Q_y is a colimit of \Sigma D.

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 \{ A \} is not a proposition, the path constructor \mathrm{e} is not strong enough. But we have the following result:

Let A be a type. Let’s consider the following diagram:
A \rightarrow \{A\} \rightarrow \{\{A\}\} \rightarrow \dots
Then, \parallel A \parallel is a colimit of this diagram.

Let’s generalize this result to a function f: A \rightarrow B (we will recover the theorem considering the unique function A \rightarrow \mathbf{1}).
Let f: A \rightarrow B . We note \mathbf{KP}(f) the colimit of the kernel pair of f:

picture:diag-kp.png

where the pullback A \times_B A is given by \Sigma_{x,\, x'}\, f(x) = f(x') .
Hence, \mathbf{KP}(f) 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:

picture:cocone-kp.png

we get a function \mathrm{lift}_f: \mathbf{KP}(f) \rightarrow B by universality (another point of view is to say that \mathrm{lift}_f is defined by \mathbf{KP\_rec}(f, \lambda\ p.\ p)).

Then, iteratively, we can construct the following diagram:

picture:iterated-diag.png

where f_0 := f :\ A \rightarrow B and f_{n+1} := \mathrm{lift}_{f_n} :\ \mathbf{KP}(f_n) \rightarrow B .
The iterated kernel pair of f is the subdiagram

picture:iterated-diag1.png

We proved the following result:

The colimit of this diagram is \Sigma_{y:B}\parallel \mathbf{fib}_f\ y\parallel \ , the image of f.

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.

picture:three-diag2.png

Going from the first line to the second is just apply the equivalence A\ \simeq\ \Sigma_{y:B}\mathbf{fib}_f\ y (for f: A \rightarrow B) at each type. Going from the second to the third is more involved, we don’t detail it here. And \Sigma_{y:B}\parallel \mathbf{fib}_f\ y\parallel \ is well the colimit of the last line: by commutation with sigmas it is sufficient to show that for all y, \parallel \mathbf{fib}_f\ y\parallel \ is the colimit of the diagram

picture:diag-fib1.png

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 \{\mathbf{1}\} is the circle \mathbb{S}^1. Hence, to compute \parallel \mathbf{1}\parallel (which is \mathbf{1} 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 \mathbf{KP} by \mathbf{KP'} 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)

\mathbf{KP'} can be seen as a “colimit with identities” of the following diagram :

picture:diag-kp-id1.png     (♣)

with \pi_i \circ \delta = \mathrm{id}.

In his article, Floris explains that, when p:\ a =_A b then \mathrm{ap}_\alpha(p) and \mathrm{t\_eq}\ a\ b are not equal. But now they become equal: by path induction we bring back to \mathrm{kp\_eq\_1}. 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. \mathbf{KP'}(\mathbf{1} \rightarrow \mathbf{1}) is \mathbf{1} (meaning that the one-step truncation of a contractible type is now \mathbf{1}),
  2. If f: A \rightarrow B is an embedding (in the sense that \mathrm{ap}(f) : x = y \rightarrow f(x) = f(y) is an equivalence for all x, y) then so is \mathrm{lift}_f : \mathbf{KP'}(f) \rightarrow B. In particular, if A is hProp then so is \mathbf{KP'}(A \rightarrow \mathbf{1}) (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 f is a generalization of his kernel pair: it is the simplicial object

picture:diag-cech.png

(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:

picture:diag-cech-trunc.png

(degeneracies still here).

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

We wonder to which extent \mathbf{KP}(f_n) 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 \mathbf{KP'}(f_0) is the colimit of the kernel pair (♣),
  2. and that there is a cocone over the 2-trunated Čech nerve into \mathbf{KP'}(f_1)

(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 C, C must have a certain compatibility with the path concatenation. \mathbf{KP'}(f) doesn’t have such a compatibility: if p:\ f(a) =_A f(b) and q:\ f(b) =_A f(c), in general we do not have

\mathrm{kp\_eq}_f\ (p \centerdot q)\ =\ \mathrm{kp\_eq}_f\ p\ \centerdot\ \mathrm{kp\_eq}_f\ q     in     \mathrm{kp}(a)\ =_{\mathbf{KP'}(f)}\ \mathrm{kp}(c).

On the contrary, \mathbf{KP'}(f_1) have the require compatibility: we can prove that

\mathrm{kp\_eq}_{f_1}\ (p \centerdot q)\ =\ \mathrm{kp\_eq}_{f_1}\ p\ \centerdot\ \mathrm{kp\_eq}_{f_1}\ q     in     \mathrm{kp}(\mathrm{kp}(a))\ =_{\mathbf{KP'}(f_1)}\ \mathrm{kp}(\mathrm{kp}(c)).

(p has indeed the type f_1(\mathrm{kp}(a)) = f_1(\mathrm{kp}(b)) because f_1 is \mathbf{KP\_rec}(f, \lambda\ p.\ p) and then f_1(\mathrm{kp}(x)) \equiv x.)
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 \mathbf{KP}(f_n) 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…

This entry was posted in Code, Higher Inductive Types. Bookmark the permalink.

14 Responses to Colimits in HoTT

  1. Floris van Doorn says:

    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 B 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.)

      • Floris van Doorn says:

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

    • Mike Shulman says:

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

      • Floris van Doorn says:

        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.

        • Mike Shulman says:

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

        • Floris van Doorn says:

          This is the special case where we take a colimit over \mathbb{N}. Suppose we have a diagram over \mathbb{N}, which is a sequence of types A : \mathbb{N} \to U with maps f : \Pi(n : \mathbb{N}), A(n) \to A(n+1). Now suppose we also have a diagram over A, which is a sequence of types P : \Pi(n : \mathbb{N}), A(n) \to U with maps g : \Pi(n : \mathbb{N})(a : A(n)), P_n(a) \to P_{n+1}(f(a)). Then we can form a new diagram over \mathbb{N}, which is the “sigma-diagram” of this data. It consists of sigma types X(n) :\equiv \Sigma(a : A(n)), P_n(a) with corresponding functions (f, g) : X(n) \to X(n+1). With colimit-of-sigmas I mean the colimit of this diagram.

          • Mike Shulman says:

            Great. Now in general we can construct the \mathbb{N}-colimit of a sequence A:\mathbb{N}\to \mathcal{U} with connecting maps f:\prod_{n:\mathbb{N}} A(n) \to A(n+1) as a coequalizer of two endomaps of \sum_{n:\mathbb{N}}A(n), one of which is the identity and the other of which (call it \Sigma f) is built out of f.

            Your P:\prod_{n:\mathbb{N}} A(n) \to \mathcal{U} also induces a family P' : (\sum_{n:\mathbb{N}}A(n)) \to \mathcal{U} defined by P'(n,a) = P_n(a), and your g:\prod_{n:\mathbb{N}}\prod_{a:A(n)} P_n(a) \to P_{n+1}(f_n(a)) induces an endomap \Sigma g of this family lying over \Sigma f.

            If g is a family of equivalences P_n(a) \simeq P_{n+1}(f_n(a)), then we have an equifibered family over a parallel pair, and the flattening lemma applies. The \tilde{W} defined there is the coequalizer of the above two induced endomaps of \sum_{(n,a):\sum_{n:\mathbb{N}} A(n)} P_n(a). But by associativity of sigmas, this is equivalent to the colimit of your X, since the latter can be constructed as a coequalizer of two endomaps of \sum_{n:\mathbb{N}} \sum_{a:A(n)} P_n(a). Therefore, the flattening lemma says that this colimit is equivalent to \sum_{x:C} Q(x), where C is the colimit of (A,f) and Q:C\to \mathcal{U} is defined by C-recursion from (P,g).

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

          • Mike Shulman says:

            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 g does not consist of equivalences, but the type Q is not defined in the naive way but rather by taking a colimit of all the P types.

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

    • Floris van Doorn says:

      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.

  3. 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 A and B). 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'(f_n) 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.

  4. Pingback: Reflexive graph quotients are pushouts | Egbert RIJKE

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s