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…

Posted in Code, Higher Inductive Types | 14 Comments

The Lean Theorem Prover

Lean is a new player in the field of proof assistants for Homotopy Type Theory. It is being developed by Leonardo de Moura working at Microsoft Research, and it is still under active development for the foreseeable future. The code is open source, and available on Github.

You can install it on Windows, OS X or Linux. It will come with a useful mode for Emacs, with syntax highlighting, on-the-fly syntax checking, autocompletion and many other features. There is also an online version of Lean which you can try in your browser. The on-line version is quite a bit slower than the native version and it takes a little while to load, but it is still useful to try out small code snippets. You are invited to test the code snippets in this post in the on-line version. You can run code by pressing shift+enter.

In this post I’ll first say more about the Lean proof assistant, and then talk about the considerations for the HoTT library of Lean (Lean has two libraries, the standard library and the HoTT library). I will also cover our approach to higher inductive types. Since Lean is not mature yet, things mentioned below can change in the future.

Update January 2017: the newest version of Lean currently doesn’t support HoTT, but there is a frozen version which does support HoTT. The newest version is available here, and the frozen version is available here. To use the frozen version, you will have to compile it from the source code yourself.

Continue reading

Posted in Code, Higher Inductive Types, Programming | 47 Comments

Real-cohesive homotopy type theory

Two new papers have recently appeared online:

Both of them have fairly chatty introductions, so I’ll try to restrain myself from pontificating at length here about their contents. Just go read the introductions. Instead I’ll say a few words about how these papers came about and how they are related to each other.

Continue reading

Posted in Applications, Foundations, Paper | 12 Comments

A new class of models for the univalence axiom

First of all, in case anyone missed it, Chris Kapulkin recently wrote a guest post at the n-category cafe summarizing the current state of the art regarding “homotopy type theory as the internal language of higher categories”.

I’ve just posted a preprint which improves that state a bit, providing a version of “Lang(C)” containing univalent strict universes for a wider class of (∞,1)-toposes C:

Continue reading

Posted in Models, Paper, Univalence | 4 Comments

Constructing the Propositional Truncation using Nonrecursive HITs

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

Posted in Code, Higher Inductive Types | 25 Comments

Universal Properties of Truncations

Some days ago at the HoTT/UF workshop in Warsaw (which was a great event!), I have talked about functions out of truncations. I have focussed on the propositional truncation \Vert - \Vert, and I want to write this blog post in case someone could not attend the talk but is interested nevertheless. There are also my slides and the arXiv paper.
The topic of my talk can be summarised as

Question: What is the type \Vert A \Vert \to B ?

This question is very easy if B is propositional, because then we have

Partial answer (1): If B is propositional, then (\Vert A \Vert \to B) \simeq (A \to B)

by the usual universal property, with the equivalence given by the canonical map. Without an assumption on B, it is much harder.

The rest of this post contains a special case which already contains some of the important ideas. It is a bit lengthy, and in case you don’t have time to read everything, here is the

Main result (general universal property of the propositional truncation).
In a dependent type theory with at least \mathbf{1}, \Sigma-, \Pi-, and identity types, which furthermore has Reedy \omega^{\mathsf{op}}-limits (“infinite \Sigma-types”), we can define the type of coherently constant functions A \xrightarrow {\omega} B as the type of natural transformations between type-valued presheaves. If the type theory has propositional truncations, we can construct a canonical map from \Vert A \Vert \to B to A \xrightarrow {\omega} B. If the type theory further has function extensionality, then this canonical map is an equivalence.
If B is known to be n-truncated for some fixed n, we can drop the assumption of Reedy \omega^{\mathsf{op}}-limits and perform the whole construction in “standard syntactical” HoTT. This describes how functions \Vert A \Vert \to B can be defined if B is not known to be propositional, and it streamlines the usual approach of finding a propositional Q with A \to Q and Q \to B.


Here comes the long version of this blog post. So, what is a function g : \Vert A \Vert \to B? If we think of elements of \Vert A \Vert as anonymous inhabitants of A, we could expect that such a g is “the same” as a function f : A \to B which “cannot look at its input”. But then, how can we specify what it means to “not look at its input” internally? A first attempt could be requesting that f is weakly constant, \mathsf{wconst}_f :\equiv \Pi_{x,y:A} f(x) = f(y). Indeed, it has been shown:

Partial answer (2): If B is a set (h-set, 0-truncated), then (\Vert A \Vert \to B) \simeq (\Sigma (f : A \to B). \mathsf{wconst}_f), where the function from left to right is the canonical one.

It is not surprising that we still need this strong condition on B if we want weak constancy to be a sufficient answer: just throwing in a bunch of paths, which might or might not “fit together” (we just don’t know anything) seems wrong. Indeed, from Mike’s recent construction, we know that the statement does become false (contradicts univalence) without this requirement.

Given a function f : A \to B and a proof c : \mathsf{wconst}_f, we can try to fix the problem that the paths given by c “do not fit together” by throwing in a coherence proof, i.e. an element of \mathsf{coh}_{f,c} :\equiv \Pi_{x,y,z:A} c(x,y) \cdot c(y,z) = c(x,z). We should already know that this will introduce its own problems and thus not fix everything, but at least, we get:

Partial answer (3): If B is 1-truncated, then (\Vert A \Vert \to B) \simeq (\Sigma (f : A \to B). \Sigma (c:\mathsf{wconst}_f). \mathsf{coh}_{f,c}), again given by a canonical map from left to right.

In my talk, I have given a proof of “partial answer (3)” via “reasoning with equivalences” (slides p. 5 ff). I start by assuming a point a_0 : A. The type B is then equivalent to the following (explanation below):

\Sigma (f_1 : B).
\Sigma (f : A \to B). \Sigma (c_1 : \Pi_{a:A} f(a) = f_1).
\Sigma (c : \mathsf{const}_f). \Sigma(d_1 : \Pi_{a^1, a^2:A} c(a^1,a^2) \cdot c_1(a^2) = c_1(a^1)
\Sigma (c_2 : f(a_0) = f_1). \Sigma (d_3 : c(a_0,a_0) \cdot c_1(a_0) = c_2).
\Sigma (d : \mathsf{coh}_{f,c_0}).
\Sigma (d_2 : \Pi_{a:A} c(a_0,a) \cdot c_1(a) = c_2).
\mathbf{1}

In the above long nested \Sigma-type, the first line is just the B that we start with. The second line adds two factors/\Sigma-components which, by function extensionality, cancel each other out (they form a singleton). The same is true for the pair in the third line, and for the pair in the fourth line. Lines five and six look different, but they are not really; it’s just that their “partners” (which would complete them to singletons) are hard to write down and, at the same time, contractible; thus, they are omitted. As B is assumed to be a 1-type, it is easy to see that the \Sigma-components in lines five and six are both propositional, and it’s also easy to see that the other \Sigma-components imply that they are both inhabited. Of course, the seventh line does nothing.

Simply by re-ordering the \Sigma-components in the above type, and not doing anything else, we get:

\Sigma (f : A \to B). \Sigma(c : \mathsf{const}_f). \Sigma(d : \mathsf{coh}_{f,c}).
\Sigma (f_1 : B) \Sigma(c_2 : f(a_0) = f_1).
\Sigma (c_1 : \Pi_{a:A} f(a) = f_1). \Sigma(d_2 : \Pi_{a:A} c(a_0,a) \cdot c_1(a) = c_2).
\Sigma (d_1 : \Pi_{a^1, a^2:A} c(a^1,a^2) \cdot c_1(a^2) = c_1(a^1)).
\Sigma (d_3 : c(a_0,a_0) \cdot c_1(a_0) = c_2).
\mathbf{1}

By the same argument as before, the components in the pair in line two cancel each other out (i.e. the pair is contractible). The same is true for line three. Line four and five are propositional as B is 1-truncated, but easily seen to be inhabited. Thus, the whole nested \Sigma-type is equivalent to \Sigma (f : A \to B). \Sigma(c : \mathsf{const}_f). \mathsf{coh}_{f,c}.
In summary, we have constructed an equivalence B \simeq \Sigma (f : A \to B). \Sigma(c : \mathsf{const}_f). \mathsf{coh}_{f,c}. By going through the construction step-by-step, we see that the function part of the equivalence (map from left to right) is the canonical one (let’s write \mathsf{canon}_1), mapping b : B to the triple (\lambda \_. b, \lambda \_ \_ . \mathsf{refl}_b , \lambda \_ \_ \_ . \mathsf{refl}_{\mathsf{refl}_b}). Before we have started the construction, we have assumed a point a_0 : A. But, and this is the crucial observation, the function \mathsf{canon}_1 does not depend on a_0! So, if the assumption A implies that \mathsf{canon}_1 is an equivalence, then \Vert A \Vert is already enough. Thus, we have \Vert A \Vert \to \big(B \simeq \Sigma (f : A \to B). \Sigma(c : \mathsf{const}_f). \mathsf{coh}_{f,c}\big). We can move the \Vert A \Vert \to-part to both sides of the equivalence, and on the right-hand side, we can apply the usual “distributivity of \Sigma and \Pi (or \to)”, to move the \Vert A \Vert \to into each \Sigma-component; but in each \Sigma-component, the \Vert A \Vert gets eaten by an A (we have that \Vert A \Vert \to \Pi_{a : A}\ldots and \Pi_{a:A} \ldots are equivalent), which gives us the claimed result.

The strategy we have used is very minimalistic. It does not need any “technology”: we just add and remove contractible pairs. For this “expanding and contracting” strategy, we have really only used very basic components of type theory (\Sigma, \Pi, identity types with function extensionality, propositional truncation, but even that only in the very end). If we want to weaken the requirement on B by one more level (i.e. if we want to derive a “universal property” which characterises \Vert A \Vert \to B if B is 2-truncated), we have to add one more coherence condition (which ensures that the \mathsf{coh}_{f,c}-component is well-behaved). The core idea is that this expanding and contracting strategy can be done for any truncation level of B, even if B is not known to be n-truncated at all, where the tower of conditions becomes infinite. I call an element of this “infinite \Sigma-type” a coherently constant function from A to B.

The idea is that the \Sigma-components (f : A \to B) and (c : \mathsf{const}_f) and (d : \mathsf{coh}_{f,c}) we used in the special case can be seen as components of a natural transformation between [2]-truncated semi-simplicial types. By semi-simplicial type, I mean a Reedy fibrant diagram \Delta_+^{\mathsf{op}} \to \mathcal{C}. By [2]-truncated semi-simplicial types, I mean the “initial segments” of semi-simplicial types, the first three components X_0, X_1, X_2 as described here.
The first diagram we need is what I call the “trivial semi-simplicial type” over A, written T \! A, and its initial part is given by T \! A_{[0]} :\equiv A, T \! A_{[1]} :\equiv A \times A, and T \! A_{[2]} :\equiv A \times A \times A. If we use the “fibred” notation (i.e. give the fibres over the matching objects), this would be T \! A_{[0]} :\equiv A, T \! A_{[1]}(a_1,a_2) :\equiv \mathbf{1}, T \! A_{[2]}(a_1,a_2,a_3,\_,\_,\_) :\equiv \mathbf{1}. In the terminology of simplicial sets, this is the [0]-coskeleton of [the diagram that is constantly] A.
The second important diagram, I call it the equality semi-simplicial type over B, is written E \! B. One potential definition for the lowest levels would be given by (I only give the fibres this time): E \! B_{[0]} :\equiv B, E \! B_{[1]}(b_1,b_2) :\equiv b_1 = b_2, E \! B_{[2]}(b_1,b_2,b_3,p_{12},p_{23},p_{13}) :\equiv p_{12} \cdot p_{23} = p_{13}. This is a fibrant replacement of B. (We are lucky because T \! A is already fibrant; otherwise, we should have constructed a fibrant replacement as well.)
If we now check what a (strict) natural transformation between T \! A and E \! B (viewed as diagrams over the full subcategory of \Delta_+^{\mathsf{op}} with objects [0],[1],[2]) is, it is easy to see that the [0]-component is exactly a map f : A \to B, the [1]-component is exactly a proof c : \mathsf{const}_f, and the [2]-component is just a proof d : \mathsf{coh}_{f,c}. (The type of such natural transformations is given by the limit of the exponential of T \! A and E \! B.)

However, even with this idea, and with the above proof for the case that B is 1-truncated, generalising this proof to the infinite case with infinitely many coherence conditions requires some ideas and a couple of technical steps which, for me, have been quite difficult. Therefore, it has taken me a very long time to write this up cleanly in an article. I am very grateful to the reviewers (this work is going to appear in the post-proceedings of TYPES’14) and to Steve (my thesis examiner) for many suggestions and interesting connections they have pointed out. In particular, one reviewer has remarked that the main result (the equivalence of coherently constant functions A \xrightarrow{\omega} B and maps out of the truncation \Vert A \Vert \to B) is a type-theoretic version of Proposition 6.2.3.4 in Lurie’s Higher Topos Theory; and Vladimir has pointed out the connection to the work of his former student Alexander Vishik. Unfortunately, both are among the many things that I have yet to understand, but there is certainly a lot to explore. If you can see further connections which I have not mentioned here or in the paper, then this is very likely because I am not aware of them, and I’d be happy to hear about it!

Posted in Foundations, Homotopy Theory, Models, Paper, Talk | 3 Comments

Modules for Modalities

As defined in chapter 7 of the book, a modality is an operation on types that behaves somewhat like the n-truncation. Specifically, it consists of a collection of types, called the modal ones, together with a way to turn any type A into a modal one \bigcirc A, with a universal property making the modal types a reflective subcategory (or more precisely, sub-(∞,1)-category) of the category of all types. Moreover, the modal types are assumed to be closed under Σs (closure under some other type formers like Π is automatic).

We called them “modalities” because under propositions-as-(some)-types, they look like the classical notion of a modal operator in logic: a unary operation on propositions. Since these are “monadic” modalities — in particular, we have A \to \bigcirc A rather than the other way around — they are most closely analogous to the “possibility” modality of classical modal logic. But since they act on all types, not just mere-propositions, for emphasis we might call them higher modalities.

The example of n-truncation shows that there are interesting new modalities in a homotopy world; some other examples are mentioned in the exercises of chapter 7. Moreover, most of the basic theory of n-truncation — essentially, any aspect of it that involves only one value of n — is actually true for any modality.

Over the last year, I’ve implemented this basic theory of modalities in the HoTT Coq library. In the process, I found one minor error in the book, and learned a lot about modalities and about Coq. For instance, my post about universal properties grew out of looking for the best way to define modalities.

In this post, I want to talk about something else I learned about while formalizing modalities: Coq’s modules, and in particular their universe-polymorphic nature. (This post is somewhat overdue in that everything I’ll be talking about has been implemented for several months; I just haven’t had time to blog about it until now.)

Continue reading

Posted in Code, Programming | 19 Comments