Type theoretic replacement & the n-truncation

Posted on 31 January 2017 by Egbert Rijke

This post is to announce a new article that I recently uploaded to the arxiv:

The main result of that article is a type theoretic replacement construction in a univalent universe that is closed under pushouts. Recall that in set theory, the replacement axiom asserts that if $F$ is a class function, assigning to any set $X$ a new set $F(X)$ , then the image of any set $A$ , i.e. the set $\{F(X)\mid X\in A\}$ is again a set. In homotopy type theory we consider instead a map $f : A\to X$ from a small type $A:U$ into a locally small type $X$ , and our main result is the construction of a small type $\mathrm{im}(f)$ with the universal property of the image of $f$ .

We say that a type is small if it is in $U$ , and for the purpose of this blog post smallness and locally smallness will always be with respect to $U$ . Before we define local smallness, let us recall the following rephrasing of the `encode-decode method’, which we might also call the Licata-Shulman theorem:

Theorem. Let $A$ be a type with $a:A$ , and let $P: A\to U$ be a type with $p:P(a)$ . Then the following are equivalent.

The total space $\Sigma_{(b:A)} P(b)$ is contractible.
The canonical map $\Pi_{(b:A)} (a=b)\to P(b)$ defined by path induction, mapping $\mathrm{refl}_a$ to $p$ , is a fiberwise equivalence.

Note that this theorem follows from the fact that a fiberwise map is a fiberwise equivalence if and only if it induces an equivalence on total spaces. Since for path spaces the total space will be contractible, we observe that any fiberwise equivalence establishes contractibility of the total space, i.e. we might add the following equivalent statement to the theorem.

There (merely) exists a family of equivalences $e:\Pi_{(b:B)} (a=b)\simeq P(b)$ . In other words, $P$ is in the connected component of the type family $b\mapsto (a=b)$ .

There are at least two equivalent ways of saying that a (possibly large) type $X$ is locally small:

For each $x,y:X$ there is a type $(x='y):U$ and an equivalence $e_{x,y}:(x=y)\simeq (x='y)$ .
For each $x,y:X$ there is a type $(x='y):U$ ; for each $x:X$ there is a term $r_X:x='x$ , and the canonical dependent function $\Pi_{(y:X)} (x=y)\to (x='y)$ defined by path induction by sending $\mathrm{refl}_x$ to $r_x$ is an equivalence.

Note that the data in the first structure is clearly a (large) mere proposition, because there can be at most one such a type family $(x='y)$ , while the equivalences in the second structure are canonical with respect to the choice of reflexivity $r_x$ . To see that these are indeed equivalent, note that the family of equivalences in the first structure is a fiberwise equivalence, hence it induces an equivalence on total spaces. Therefore it follows that the total space $\Sigma_{(y:X)} (x='y)$ is contractible. Thus we see by Licata’s theorem that the canoncial fiberwise map is a fiberwise equivalence. Furthermore, it is not hard to see that the family of equivalences $e_{x,y}$ is equal to the canonical family of equivalences. There is slightly more to show, but let us keep up the pace and go on.

Examples of locally small types include any small type, any mere proposition regardless of their size, the universe is locally small by the univalence axiom, and if $A$ is small and $X$ is locally small then the type $A\to X$ is locally small. Observe also that the univalence axiom follows if we assume the `uncanonical univalence axiom’, namely that there merely exists a family of equivalences $e_{A,B} : (A=B)\simeq (A\simeq B)$ . Thus we see that the slogan ‘identity of the universe is equivalent to equivalence’ actually implies univalence.

Main Theorem. Let $U$ be a univalent universe that is closed under pushouts. Suppose that $A:U$ , that $X$ is a locally small type, and let $f:A\to X$ . Then we can construct

a small type $\mathrm{im}(f):U$ ,
a factorization
such that $i_f$ is an embedding that satisfies the universal property of the image inclusion, namely that for any embedding $g$ , of which the domain is possibly large, if $f$ factors through $g$ , then so does $i_f$ .

Recall that $f$ factors through an embedding $g$ in at most one way. Writing $\mathrm{Hom}_X(f,g)$ for the mere proposition that $f$ factors through $g$ , we see that $i_f$ satisfies the universal property of the image inclusion precisely when the canonical map

$\mathrm{Hom}_X(i_f,g)\to\mathrm{Hom}_X(f,g)$

is an equivalence.

Most of the paper is concerned with the construction with which we prove this theorem: the join construction. By repeatedly joining a map with itself, one eventually arrives at an embedding. The join of two maps $f:A\to X$ and $g:B\to X$ is defined by first pulling back, and then taking the pushout, as indicated in the following diagram

join_maps

In the case $X \equiv \mathbf{1}$ , the type $A \ast_X B$ is equivalent to the usual join of types $A \ast B$ . Just like the join of types, the join of maps with a common codomain is associative, commutative, and it has a unit: the unique map from the empty type into $X$ . The join of two embeddings is again an embedding. We show that the last statement can be strengthened: the maps $f:A\to X$ that are idempotent in a canonical way (i.e. the canonical morphism $f \to f \ast f$ in the slice category over $X$ is an equivalence) are precisely the embeddings.

Below, I will indicate how we can use the above theorem to construct the n-truncations for any $n\geq -2$ on any univalent universe that is closed under pushouts. Other applications include the construction of set-quotients and of Rezk-completion, since these are both constructed as the image of the Yoneda-embedding, and it also follows that the univalent completion of any dependent type $P:A\to U$ can be constructed as a type in $U$ , namely $\mathrm{im}(P)$ , without needing to resort to more exotic higher inductive types. In particular, any connected component of the universe is equivalent to a small type.

Theorem. Let $U$ be a univalent universe that is closed under pushouts. Then we can define for any $n\geq -2$

an n-truncation operation $\|{-}\|_n:U\to U$ ,
a map $|{-}|:\Pi_{(A:U)} A\to \|A\|_n$
such that for any $A:U$ , the type $\|A\|_n$ is n-truncated and satisfies the (dependent) universal property of n-truncation, namely that for every type family $P:\|A\|_n\to\mathrm{Type}$ of possibly large types such that each $P(x)$ is n-truncated, the canonical map
$(\Pi_{(x:\|A\|_n)} P(x))\to (\Pi_{(a:A)} P(|a|_n))$
given by precomposition by $|{-}|_n$ is an equivalence.

Construction. The proof is by induction on $n\geq -2$ . The case $n\equiv -2$ is trivial (take $A\mapsto \mathbf{1}$ ). For the induction hypothesis we assume an n-truncation operation with structure described in the statement of the theorem.

First, we define $\mathcal{Y}_n:A\to (A\to U)$ by $\mathcal{Y}_n(a,b):\equiv \|a=b\|_n$ . As we have seen, the universe is locally small, and therefore the type $A\to U$ is locally small. Therefore we can define

$\|A\|_{n+1} :\equiv \mathrm{im}(\mathcal{Y}_n)$
$|{-}|_{n+1} :\equiv q_{\mathcal{Y}_n}$ .

For the proof that $\|A\|_{n+1}$ is indeed $(n+1)$ -truncated, and satisfies the universal property of the n-truncation we refer to the article.

Posted in Uncategorized | Leave a comment

Parametricity, automorphisms of the universe, and excluded middle

Posted on 26 January 2017 by Auke Booij

Specific violations of parametricity, or existence of non-identity automorphisms of the universe, can be used to prove classical axioms. The former was previously featured on this blog, and the latter is part of a discussion on the HoTT mailing list. In a cooperation between Martín Escardó, Peter Lumsdaine, Mike Shulman, and myself, we have strengthened these results and recorded them in a paper that is now on arXiv.

In this blog post, we work with the full repertoire of HoTT axioms, including univalence, propositional truncations, and pushouts. For the paper, we have carefully analysed which assumptions are used in which theorem, if any.

Parametricity

Parametricity is a property of terms of a language. If your language only has parametric terms, then polymorphic functions have to be invariant under the type parameter. So in MLTT, the only term inhabiting the type $\prod_{X:\mathcal{U}}X \to X$ of polymorphic endomaps is the polymorphic identity $\lambda (X:\mathcal{U}). \mathsf{id}_X$ .

In univalent foundations, we cannot prove internally that every term is parametric. This is because excluded middle is not parametric (exercise 6.9 of the HoTT book tells us that, assuming LEM, we can define a polymorphic endomap that flips the booleans), but there exist classical models of univalent foundations. So if we could prove this internally, excluded middle would be false, and thus the classical models would be invalid.

In the abovementioned blog post, we observed that exercise 6.9 of the HoTT book has a converse: if $f:\prod_{X:\mathcal{U}}X\to X$ is the flip map on the type of booleans, then excluded middle holds. In the paper on arXiv, we have a stronger result:

Theorem. There exist $f:\prod_{X:\mathcal{U}}X\to X$ and a type $X$ and a point $x:X$ with $f_X(x)\neq x$ if and only if excluded middle holds.

Notice that there are no requirements on the type $X$ or the point $x$ . We have also applied the technique used for this theorem in other scenarios, for example:

Theorem. There exist $f:\prod_{X:\mathcal{U}}X\to \mathbf{2}$ and types $X, Y$ and points $x:X, y:Y$ with $f_X(x)\neq f_Y(y)$ if and only if weak excluded middle holds.

The results in the paper illustrate that different violations of parametricity have different proof-theoretic strength: some violations are impossible, while others imply varying amounts of excluded middle.

Automorphisms of the universe

In contrast to parametricity, which proves that terms of some language necessarily have some properties, it is currently unknown if non-identity automorphisms of the universe are definable in univalent foundations. But some believe that this may not be the case.

In the presence of excluded middle, we can define non-identity automorphisms of the universe. Given a type $X$ , we use excluded middle to decide if $X$ is a proposition. If it is, we map $X$ to $\neg X$ , and otherwise we map $X$ to itself. Assuming excluded middle, we have $\neg\neg X=X$ for any proposition, so this is an automorphism.

The above automorphism swaps the empty type $\mathbf{0}$ with the unit type $\mathbf{1}$ and leaves all other types unchanged. More generally, assuming excluded middle we can swap any two types with equivalent automorphism ∞-groups, since in that case the corresponding connected components of the universe are equivalent. Still more generally, we can permute arbitrarily any family of types all having the same automorphism ∞-group.

The simplest case of this is when all the types are rigid, i.e. have trivial automorphism ∞-group. The types $\mathbf{0}$ and $\mathbf{1}$ are both rigid, and at least with excluded middle no other sets are; but there can be rigid higher types. For instance, if $G$ is a group that is a set (i.e. a 1-group), then its Eilenberg-Mac Lane space $B G$ is a 1-type, and its automorphism ∞-group is a 1-type whose $\pi_0$ is the outer automorphisms of $G$ and whose $\pi_1$ is the center of $G$ . Thus, if $G$ has trivial outer automorphism group and trivial center, then $BG$ is rigid. Such groups are not uncommon, including for instance the symmetric group $S_n$ for any $n\neq 2,6$ . Thus, assuming excluded middle we can permute these $BS_n$ arbitrarily, producing uncountably many automorphisms of the universe.

In the converse direction, we recorded the following.

Theorem. If there is an automorphism of the universe that maps some inhabited type to the empty type, then excluded middle holds.

Corollary. If there is an automorphism $g:\mathcal{U}\to\mathcal{U}$ of the universe with $g(\mathbf{0})\neq\mathbf{0}$ , then the double negation

$\neg\neg\prod_{P:\mathcal{U}}\mathsf{isProp}(P)\to P+\neg P$

of the law of excluded middle holds.

This corollary relates to an unclaimed prize: if from an arbitrary equivalence $f:\mathcal{U}\to\mathcal{U}$ such that $f(X) \neq X$ for a particular $X:\mathcal{U}$ you get a non-provable consequence of excluded middle, then you get $X$ -many beers. So this corollary wins you 0 beers. Although perhaps sober, we think this is an achievement worth recording.

Using this corollary, in turn, we can win $\mathsf{LEM}_\mathcal{U}$ -many beers, where $\mathsf{LEM}_\mathcal{U}$ is excluded middle for propositions in the universe $\mathcal{U}$ . If $\mathcal{U} :\mathcal{V}$ we have $\mathsf{LEM}_\mathcal{U}:\mathcal{V}$ . Suppose $g$ is an automorphism of $\mathcal{V}$ with $g(\mathsf{LEM}_\mathcal{U})\neq\mathsf{LEM}_\mathcal{U}$ , then $\neg\neg\mathsf{LEM}_\mathcal{U}$ . For suppose that $\neg\mathsf{LEM}_\mathcal{U}$ , and hence $\mathsf{LEM}_\mathcal{U}=\mathbf{0}$ . So by the corollary, we obtain $\neg\neg\mathsf{LEM}_\mathcal{V}$ . But $\mathsf{LEM}_\mathcal{V}$ implies $\mathsf{LEM}_\mathcal{U}$ by cumulativity, so $\neg\neg\mathsf{LEM}_\mathcal{U}$ also holds, contradicting our assumption that $\neg\mathsf{LEM}_\mathcal{U}$ .

To date no one has been able to win 1 beer.

Posted in Foundations | 7 Comments

HoTT MRC

Posted on 4 October 2016 by Mike Shulman

From June 4 — 10, 2017, there will be a workshop on homotopy type theory as one of the AMS’s Mathematical Research Communities (MRCs).

Continue reading →

Posted in News, Publicity, Uncategorized | 1 Comment

HoTTSQL: Proving Query Rewrites with Univalent SQL Semantics

Posted on 26 September 2016 by konstantinweitz

SQL is the lingua franca for retrieving structured data. Existing semantics for SQL, however, either do not model crucial features of the language (e.g., relational algebra lacks bag semantics, correlated subqueries, and aggregation), or make it hard to formally reason about SQL query rewrites (e.g., the SQL standard’s English is too informal). This post focuses on the ways that HoTT concepts (e.g., Homotopy Types, the Univalence Axiom, and Truncation) enabled us to develop HoTTSQL — a new SQL semantics that makes it easy to formally reason about SQL query rewrites. Our paper also details the rich set of SQL features supported by HoTTSQL.

You can download this blog post’s source (implemented in Coq using the HoTT library). Learn more about HoTTSQL by visiting our website.

Continue reading →

Posted in Applications | 5 Comments

Combinatorial Species and Finite Sets in HoTT

Posted on 20 July 2016 by Brent

(Post by Brent Yorgey)

My dissertation was on the topic of combinatorial species, and specifically on the idea of using species as a foundation for thinking about generalized notions of algebraic data types. (Species are sort of dual to containers; I think both have intereseting and complementary things to offer in this space.) I didn’t really end up getting very far into practicalities, instead getting sucked into a bunch of more foundational issues.

To use species as a basis for computational things, I wanted to first “port” the definition from traditional, set-theory-based, classical mathematics into a constructive type theory. HoTT came along at just the right time, and seems to provide exactly the right framework for thinking about a constructive encoding of combinatorial species.

For those who are familiar with HoTT, this post will contain nothing all that new. But I hope it can serve as a nice example of an “application” of HoTT. (At least, it’s more applied than research in HoTT itself.)

Combinatorial Species

Traditionally, a species is defined as a functor $F : \mathbb{B} \to \mathbf{FinSet}$ , where $\mathbb{B}$ is the groupoid of finite sets and bijections, and $\mathbf{FinSet}$ is the category of finite sets and (total) functions. Intuitively, we can think of a species as mapping finite sets of “labels” to finite sets of “structures” built from those labels. For example, the species of linear orderings (i.e. lists) maps the finite set of labels $\{1,2, \dots, n\}$ to the size- $n!$ set of all possible linear orderings of those labels. Functoriality ensures that the specific identity of the labels does not matter—we can always coherently relabel things.

Constructive Finiteness

So what happens when we try to define species inside a constructive type theory? The crucial piece is $\mathbb{B}$ : the thing that makes species interesting is that they have built into them a notion of bijective relabelling, and this is encoded by the groupoid $\mathbb{B}$ . The first problem we run into is how to encode the notion of a finite set, since the notion of finiteness is nontrivial in a constructive setting.

One might well ask why we even care about finiteness in the first place. Why not just use the groupoid of all sets and bijections? To be honest, I have asked myself this question many times, and I still don’t feel as though I have an entirely satisfactory answer. But what it seems to come down to is the fact that species can be seen as a categorification of generating functions. Generating functions over the semiring $R$ can be represented by functions $\mathbb{N} \to R$ , that is, each natural number maps to some coefficient in $R$ ; each natural number, categorified, corresponds to (an equivalence class of) finite sets. Finite label sets are also important insofar as our goal is to actually use species as a basis for computation. In a computational setting, one often wants to be able to do things like enumerate all labels (e.g. in order to iterate through them, to do something like a map or fold). It will therefore be important that our encoding of finiteness actually has some computational content that we can use to enumerate labels.

Our first attempt might be to say that a finite set will be encoded as a type $A$ together with a bijection between $A$ and a canonical finite set of a particular natural number size. That is, assuming standard inductively defined types $\mathbb{N}$ and $\mathsf{Fin}$ ,

$\displaystyle \Sigma (A:U). \Sigma (n : \mathbb{N}). A \cong \mathsf{Fin}(n).$

However, this is unsatisfactory, since defining a suitable notion of bijections/isomorphisms between such finite sets is tricky. Since $\mathbb{B}$ is supposed to be a groupoid, we are naturally led to try using equalities (i.e. paths) as morphisms—but this does not work with the above definition of finite sets. In $\mathbb{B}$ , there are supposed to be $n!$ different morphisms between any two sets of size $n$ . However, given any two same-size inhabitants of the above type, there is only one path between them—intuitively, this is because paths between $\Sigma$ -types correspond to tuples of paths relating the components pointwise, and such paths must therefore preserve the particular relation to $\mathsf{Fin}(n)$ . The only bijection which is allowed is the one which sends each element related to $i$ to the other element related to $i$ , for each $i \in \mathsf{Fin}(n)$ .

So elements of the above type are not just finite sets, they are finite sets with a total order, and paths between them must be order-preserving; this is too restrictive. (However, this type is not without interest, and can be used to build a counterpart to L-species. In fact, I think this is exactly the right setting in which to understand the relationship between species and L-species, and more generally the difference between isomorphism and equipotence of species; there is more on this in my dissertation.)

Truncation to the Rescue

We can fix things using propositional truncation. In particular, we define

$\displaystyle U_F := \Sigma (A:U). \|\Sigma (n : \mathbb{N}). A \cong \mathsf{Fin}(n)\|.$

That is, a “finite set” is a type $A$ together with some hidden evidence that $A$ is equivalent to $\mathsf{Fin}(n)$ for some $n$ . (I will sometimes abuse notation and write $A : U_F$ instead of $(A, p) : U_F$ .) A few observations:

First, we can pull the size $n$ out of the propositional truncation, that is, $U_F \cong \Sigma (A:U). \Sigma (n: \mathbb{N}). \|A \cong \mathsf{Fin}(n)\|$ . Intuitively, this is because if a set is finite, there is only one possible size it can have, so the evidence that it has that size is actually a mere proposition.
More generally, I mentioned previously that we sometimes want to use the computational evidence for the finiteness of a set of labels, e.g. enumerating the labels in order to do things like maps and folds. It may seem at first glance that we cannot do this, since the computational evidence is now hidden inside a propositional truncation. But actually, things are exactly the way they should be: the point is that we can use the bijection hidden in the propositional truncation as long as the result does not depend on the particular bijection we find there. For example, we cannot write a function which returns the value of type $A$ corresponding to $0 : \mathsf{Fin}(n)$ , since this reveals something about the underlying bijection; but we can write a function which finds the smallest value of $A$ (with respect to some linear ordering), by iterating through all the values of $A$ and taking the minimum.
It is not hard to show that if $A : U_F$ , then $A$ is a set (i.e. a 0-type) with decidable equality, since $A$ is equivalent to the 0-type $\mathsf{Fin}(n)$ . Likewise, $U_F$ itself is a 1-type.
Finally, note that paths between inhabitants of $U_F$ now do exactly what we want: a path $(A,p) = (B,q)$ is really just a path $A = B$ between 0-types, that is, a bijection, since $p = q$ trivially.

Constructive Species

We can now define species in HoTT as functions of type $U_F \to U$ . The main reason I think this is the Right Definition ™ of species in HoTT is that functoriality comes for free! When defining species in set theory, one must say “a species is a functor, i.e. a pair of mappings satisfying such-and-such properties”. When constructing a particular species one must explicitly demonstrate the functoriality properties; since the mappings are just functions on sets, it is quite possible to write down mappings which are not functorial. But in HoTT, all functions are functorial with respect to paths, and we are using paths to represent the morphisms in $U_F$ , so any function of type $U_F \to U$ automatically has the right functoriality properties—it is literally impossible to write down an invalid species. Actually, in my dissertation I define species as functors between certain categories built from $U_F$ and $U$ , but the point is that any function $U_F \to U$ can be automatically lifted to such a functor.

Here’s another nice thing about the theory of species in HoTT. In HoTT, coends whose index category are groupoids are just plain $\Sigma$ -types. That is, if $\mathbb{C}$ is a groupoid, $\mathbb{D}$ a category, and $T : \mathbb{C}^{\mathrm{op}} \times \mathbb{C} \to \mathbb{D}$ , then $\int^C T(C,C) \cong \Sigma (C : \mathbb{C}). T(C,C)$ . In set theory, this coend would be a quotient of the corresponding $\Sigma$ -type, but in HoTT the isomorphisms of $\mathbb{C}$ are required to correspond to paths, which automatically induce paths over the $\Sigma$ -type which correspond to the necessary quotient. Put another way, we can define coends in HoTT as a certain HIT, but in the case that $\mathbb{C}$ is a groupoid we already get all the paths given by the higher path constructor anyway, so it is redundant. So, what does this have to do with species, I hear you ask? Well, several species constructions involve coends (most notably partitional product); since species are functors from a groupoid, the definitions of these constructions in HoTT are particularly simple. We again get the right thing essentially “for free”.

There’s lots more in my dissertation, of course, but these are a few of the key ideas specifically relating species and HoTT. I am far from being an expert on either, but am happy to entertain comments, questions, etc. I can also point you to the right section of my dissertation if you’re interested in more detail about anything I mentioned above.

Posted in Applications, Higher Inductive Types, Programming | Tagged combinatorial species, finite, species | 5 Comments

Parametricity and excluded middle

Posted on 24 February 2016 by Auke Booij

Exercise 6.9 of the HoTT book tells us that, and assuming LEM, we can exhibit a function $f:\Pi_{X:\mathcal{U}}(X\to X)$ such that $f_\mathbf{2}$ is a non-identity function $\mathbf{2}\to\mathbf{2}.$ I have proved the converse of this. Like in exercise 6.9, we assume univalence.

Parametricity

In a typical functional programming career, at some point one encounters the notions of parametricity and free theorems.

Parametricity can be used to answer questions such as: is every function

f : forall x. x -> x

equal to the identity function? Parametricity tells us that this is true for System F.

However, this is a metatheoretical statement. Parametricity gives properties about the terms of a language, rather than proving internally that certain elements satisfy some properties.

So what can we prove internally about a polymorphic function $f:\Pi_{X:\mathcal{U}}X\to X$ ?

In particular, we can see that internal proofs (claiming that $f$ must be the identity function for every type $X$ ) cannot exist: exercise 6.9 of the HoTT book tells us that, assuming LEM, we can exhibit a function $f:\Pi_{X:\mathcal{U}}(X\to X)$ such that $f_\mathbf{2}$ is $\mathsf{flip}:\mathbf{2}\to\mathbf{2}.$ (Notice that the proof of this is not quite as trivial as it may seem: LEM only gives us $P+\neg P$ if $P$ is a (mere) proposition (a.k.a. subsingleton). Hence, simple case analysis on $X\simeq\mathbf{2}$ does not work, because this is not necessarily a proposition.)

And given the fact that LEM is consistent with univalent foundations, this means that a proof that $f$ is the identity function cannot exist.

I have proved that LEM is exactly what is needed to get a polymorphic function that is not the identity on the booleans.

Theorem. If there is a function $f:\Pi_{X:\mathcal U}X\to X$ with $f_\mathbf2\neq\mathsf{id}_\mathbf2,$ then LEM holds.

Proof idea

If $f_\mathbf2\neq\mathsf{id}_\mathbf2,$ then by simply trying both elements $0_\mathbf2,1_\mathbf2:\mathbf2,$ we can find an explicit boolean $b:\mathbf2$ such that $f_\mathbf2(b)\neq b.$ Without loss of generality, we can assume $f_\mathbf2(0_\mathbf2)\neq 0_\mathbf2.$

For the remainder of this analysis, let $P$ be an arbitrary proposition. Then we want to achieve $P+\neg P,$ to prove LEM.

We will consider a type with three points, where we identify two points depending on whether $P$ holds. In other words, we consider the quotient of a three-element type, where the relation between two of those points is the proposition $P.$

I will call this space $\mathbf{3}_P,$ and it can be defined as $\Sigma P+\mathbf{1},$ where $\Sigma P$ is the suspension of $P.$ This particular way of defining the quotient, which is equivalent to a quotient of a three-point set, will make case analysis simpler to set up. (Note that suspensions are not generally quotients: we use the fact that $P$ is a proposition here.)

Notice that if $P$ holds, then $\mathbf{3}_P\simeq\mathbf{2},$ and also $(\mathbf{3}_P\simeq\mathbf{3}_P)\simeq\mathbf{2}.$

We will consider $f$ at the type $(\mathbf{3}_P\simeq\mathbf{3}_P)$ (not $\mathbf{3}_P$ itself!). Now the proof continues by defining

$g:=f_{\mathbf{3}_P\simeq\mathbf{3}_P}(\mathsf{ide}_{\mathbf{3}_P}):\mathbf{3}_P\simeq\mathbf{3}_P$

(where $\mathsf{ide_{\mathbf3_P}}$ is the equivalence given by the identity function on $\mathbf3_P$ ) and doing case analysis on $g(\mathsf{inr}(*)),$ and if necessary also on $g(\mathsf{inl}(x))$ for some elements $x:\Sigma P.$ I do not believe it is very instructive to spell out all cases explicitly here. I wrote a more detailed note containing an explicit proof.

Notice that doing case analysis here is simply an instance of the induction principle for $+.$ In particular, we do not require decidable equality of $\mathbf3_P$ (which would already give us $P+\neg P,$ which is exactly what we are trying to prove).

For the sake of illustration, here is one case:

$g(\mathsf{inr}(*))= \mathsf{inr}(*):$ Assume $P$ holds. Then since $(\mathbf{3}_P\simeq\mathbf{3}_P)\simeq\mathbf{2},$ then by transporting along an appropriate equivalence (namely the one that identifies $0_\mathbf2$ with $\mathsf{ide}_{\mathbf3_P}),$ we get $f_{\mathbf{3}_P\simeq\mathbf{3}_P}(\mathsf{ide}_{\mathbf{3}_P})\neq\mathsf{ide}_{\mathbf{3}_P}.$ But since $g$ is an equivalence for which $\mathsf{inr}(*)$ is a fixed point, $g$ must be the identity everywhere, that is, $g=\mathsf{ide}_{\mathbf{3}_P},$ which is a contradiction.

I formalized this proof in Agda using the HoTT-Agda library

Acknowledgements

Thanks to Martín Escardó, my supervisor, for his support. Thanks to Uday Reddy for giving the talk on parametricity that inspired me to think about this.

Posted in Foundations | 13 Comments

Colimits in HoTT

Posted on 8 January 2016 by Simon Boulier

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

$\mathbf{KP'}(\mathbf{1} \rightarrow \mathbf{1})$ is $\mathbf{1}$ (meaning that the one-step truncation of a contractible type is now $\mathbf{1}$ ),
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 :

That $\mathbf{KP'}(f_0)$ is the colimit of the kernel pair (♣),
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

Homotopy Type Theory

Type theoretic replacement & the n-truncation

Parametricity, automorphisms of the universe, and excluded middle

Parametricity

Automorphisms of the universe

HoTT MRC

HoTTSQL: Proving Query Rewrites with Univalent SQL Semantics

Combinatorial Species and Finite Sets in HoTT

Combinatorial Species

Constructive Finiteness

Truncation to the Rescue

Constructive Species

Parametricity and excluded middle

Parametricity

Proof idea

Acknowledgements

Colimits in HoTT

Colimits in HoTT

Existence

Functoriality and Uniqueness

Diagram morphisms

Precomposition

Functoriality of colimits

Uniqueness

Commutation with sigmas

Iterated Kernel Pair

First construction

Second construction

Toward a link with the Čech nerve

Questions

Recent Posts

Categories

Archives

Blogroll

Meta