HoTTSQL: Proving Query Rewrites with Univalent SQL Semantics

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.

Relations

 

The basic datatype in SQL is a relation, which is a bag (i.e., multiset) of tuples with the same given schema. You can think of a tuple’s schema as being like a variable’s type in a programming language. We formalize a bag of some type A as a function that maps every element of A to a type. The type’s cardinality indicates how many times the element appears in the bag.

Definition Bag A := A -> Type.

For example, the bag numbers = {| 7, 42, 7 |} can be represented as:

Definition numbers : Bag nat :=
fun n => match n with
| 7 => Bool
| 42 => Unit
| _ => Empty
end.

A SQL query maps one or more input relations to an output relation. We can implement SQL queries as operations on bags. For example, a disjoint union query in SQL can be implemented as a function that takes two input bags r1 and r2, and returns a bag in which every tuple a appears r1 a + r2 a times. Note that the cardinality of the sum type r1 a + r2 a is equal to the sum of the cardinalities of r1 a and r2 a.

Definition bagUnion {A} (r1 r2:Bag A) : Bag A :=
fun (a:A) => r1 a + r2 a.

Most database systems contain a query optimizer that applies SQL rewrite rules to improve query performance. We can verify SQL rewrite rules by proving the equality of two bags. For example, we can show that the union of r1 and r2 is equal to the union of r2 and r1, using functional extensionality (by_extensionality), the univalence axiom (path_universe_uncurried), and symmetry of the sum type (equiv_sum_symm).

Lemma bag_union_symm {A} (r1 r2 : Bag A) :
bagUnion r1 r2 = bagUnion r2 r1.
Proof.
unfold bagUnion.
by_extensionality a.
(* r1 a + r1 a = r2 a + r2 a *)
apply path_universe_uncurried.
(* r1 a + r1 a <~> r2 a + r2 a *)
apply equiv_sum_symm.
Qed.

Note that + and * on homotopy types are like the operations of a commutative semi-ring, Empty and Unit are like the identity elements of a commutative semi-ring, and there are paths witnessing the commutative semi-ring axioms for these operations and identity elements. We use the terminology like here, because algebraic structures over higher-dimensional types in HoTT are usually defined using coherence conditions between the equalities witnessing the structure’s axioms, which we have not yet attempted to prove. 

Many SQL rewrite rules simplify to an expressions built using the operators of this semi-ring (e.g. r1 a + r1 a = r2 a + r2 a above), and could thus be potentially solved or simplified using a ring tactic (see). Unfortunately, Coq’s ring tactic is not yet ported to the HoTT library. Porting ring may dramatically simplify many of our proofs (Anyone interested in porting the ring tactic? Let us know).

 

It is reasonable to assume that SQL relations are bags that map tuples only to 0-truncated types (types with no higher homotopical information), because real-world databases’ input relations only contain tuples with finite multiplicity (Fin n is 0-truncated), and because SQL queries only use type operators that preserve 0-truncation. However, HoTTSQL does not requires this assumption, and as future work, it may be interesting to understand what the “cardinality” of a type with higher homotopical information means.

How to model bags is a fundamental design decision for mechanizing formal proofs of SQL query equivalences. Our formalization of bags is unconventional but effective for reasoning about SQL query rewrites, as we will see. 

Previous work has modeled bags as lists (e.g., as done by Malecha et al.), where SQL queries are recursive functions over input lists, and two bags are equal iff their underlying lists are equal up to element reordering. Proving two queries equal thus requires induction on input lists (including coming up with induction hypothesis) and reasoning about list permutations. In contrast, by modeling bags as functions from tuples to types, proving two queries equal just requires proving the equality of two HoTT types.

 

In the database research community, prior work has modeled bags as functions to natural numbers (e.g., as done by Green et al.). Using this approach, one cannot define the potentially infinite sum a, r a that counts the number of elements in a bag r. This is important since a basic operation in SQL, projection, requires counting all tuples in a bag that match a certain predicate. In contrast, by modeling bags as functions from tuples to types, we can count the number of elements in a bag using the sigma type , where the cardinality of the sigma type a, r a is equal to the sum of the cardinalities of r a for all a.

 

Schemas

 

Traditionally, a relation is modeled as a bag of n-ary tuples, and a relation’s schema both describes how many elements there are in each tuple (i.e., n), and the the type of each element. Thus, a schema is formalized as a list of types.

 

In HoTTSQL, a relation is modeled as a bag of nested pairs (nested binary-tuples), and a relation’s schema both describes the nesting of the pairs and the types of the leaf pairs. In HoTTSQL, a schema is thus formalized as a binary tree, where each node stores only its child nodes, and each leaf stores a type. Our formalization of schemas as trees and tuples as nested pairs is unconventional. We will see later how this choice simplifies reasoning.

Inductive Schema :=
| node (s1 s2 : Schema)
| leaf (T:Type)
.

For example, a schema for people (with a name, age, and employment status) can be expressed as Person : Schema := node (leaf Name) (node (leaf Nat) (leaf Bool))

We formalize a tuple as a function Tuple that takes a schema s and returns a nested pair which matches the tree structure and types of s.

Fixpoint Tuple (s:Schema) : Type :=
match s with
| node s1 s2 => Tuple s1 * Tuple s2
| leaf T => T
end.

For example, Tuple Person = Name * (Nat * Bool) and (Alice, (23, false)) : Tuple Person

Finally, we formalize a relation as a bag of tuples that match a given schema s.

Definition Relation (s:Schema) := Bag (Tuple s).

 

Queries

 

Recall that a SQL query maps one or more input relations to an output relation, and that we can implement SQL queries with operations on bags. In this section, we incrementally introduce various SQL queries, and describe their semantics in terms of bags.

 

Union and Selection

 

The following subset of the SQL language supports unioning relations, and selecting (i.e., filtering) tuples in a relation.

Inductive SQL : Schema -> Type :=
| union {s} : SQL s -> SQL s -> SQL s
| select {s} : Pred s -> SQL s -> SQL s
(* … *)
.

Fixpoint denoteSQL {s} (q : SQL s) : Relation s :=
match q with
| union _ q1 q2 => fun t => denoteSQL q1 t + denoteSQL q2 t
| select _ b q => fun t => denotePred b t * denoteSQL q t
(* … *)
end.

 

The query select b q removes all the tuples from the relation returned by the query q where the predicate b does not hold. We denote the predicate as a function denotePred(b) : Tuple s -> Type that maps a tuple to a (-1)-truncated type. denotePred(b) t is Unit if the predicate holds for t, and Empty otherwise. The query multiplies the relation with the predicate to implement the semantics of the query (i.e., n * Unit = n and n * Empty = Empty, where n is the multiplicity of the input tuple t). 

To syntactically resemble SQL, we write q1 UNION ALL q2 for union q1 q2, q WHERE b for select b q, and SELECT * FROM q for q. We write q for the denotation of a query denoteQuery q, and b for the denotation of a predicate denotePred b.

 

To prove that two SQL queries are equal, one has to prove that their two denotations are equal, i.e., that two bags returned by the two queries are equal, given any input relation(s). The following example shows how we can prove that selection distributes over union, by reducing it to showing the distributivity of * over + (lemma sum_distrib_l).

Lemma proj_union_distr s (q1 q2 : SQL s) (p:Pred s) :
SELECT * FROM (q1 UNION ALL q2) WHERE p ⟧ =
⟦ (SELECT * FROM q1 WHERE p) UNION ALL
(SELECT * FROM q2 WHERE p) ⟧.
Proof.
simpl.
by_extensionality t.
(* ⟦p⟧ t * (⟦q1⟧ t + ⟦q2⟧ t) = ⟦p⟧ t * ⟦q1⟧ t + ⟦p⟧ t * ⟦q2⟧ t *)
apply path_universe_uncurried.
apply sum_distrib_l.
Qed.

 

 

Duplicate Elimination, Products, and Projections

 

So far, we have seen the use of homotopy types to model SQL relations, and have seen the use of the univalence axiom to prove SQL rewrite rules. We now show the use of truncation to model the removal of duplicates in SQL relations. To show an example of duplicate removal in SQL, we first have to extend our semantics of the SQL language with more features.

Inductive Proj : Schema -> Schema -> Type :=
| left {s s’} : Proj (node s s’) s
| right {s s’} : Proj (node s’ s) s
(* … *)
.

Inductive SQL : Schema -> Type :=
(* … *)
| distinct {s} : SQL s -> SQL s
| product {s1 s2} : SQL s1 -> SQL s2 -> SQL (node s1 s2)
| project {s s’} : Proj s s’ -> SQL s -> SQL s’
(* … *)
.

Fixpoint denoteProj {s s’} (p : Proj s s’) : Tuple s ->
Tuple s’ :=
match p with
| left _ _ => fst
| right _ _ => snd
(* … *)
end.

Fixpoint denoteSQL {s} (q : SQL s) : Relation s :=
match q with
(* … *)
| distinct _ q => fun t => ║ denoteSQL q t
| product _ _ q1 q2 => fun t => denoteSQL q1 (fst t) *
denoteSQL q2 (snd t)
| project _ _ p q => fun t’ => ∑ t, denoteSQL q t *
(denoteProj p t = t’)
(* … *)
end.

The query distinct q removes duplicate tuples in the relation returned by the query q using the (-1)-truncation function q (see HoTT book, chapter 3.7). 

The query product q1 q2 creates the cartesian product of q1 and q2, i.e., it returns a bag that maps every tuple consisting of two tuples t1 and t2 to the number of times t1 appears in q1 multiplied by the number of times t2 appears in q2.

 

The query project p q projects elements from each tuple contained in the query q. The projection is defined by p, and is denoted as a function that takes a tuple of some schema s and returns a new tuple of some schema s’. For example, left is the projection that takes a tuple and returns the tuple’s first element. We assume that tuples have no higher homotopical information, and that equality between tuples is thus (-1)-truncated.

 

Like before, we write DISTINCT q for distinct q, FROM q1, q2 for product q1 q2, and SELECT p q for project p q. We write p for the denotation of a projection denoteProj p.

 

Projection of products is the reason HoTTSQL must model schemas as nested pairs. If schemas were flat n-ary tuples, the left projection would not know which elements of the tuple formerly belonged to the left input relation of the product, and could thus not project them (feel free to contact us if you have ideas on how to better represent schemas)

 

Projection requires summing over all tuples in a bag, as multiple tuples may be merged into one. This sum is over an infinite domain (all tuples) and thus cannot generally be implemented with natural numbers. Implementing it using the (sigma) type is however trivial.

 

Equipped with these additional features, we can now prove the following rewrite rule.

Lemma self_join s (q : SQL s) :
DISTINCT SELECT left FROM q, q ⟧ =
DISTINCT SELECT * FROM q ⟧.

The two queries are equal, because the left query performs a redundant self-join. Powerful database query optimizations, such as magic sets rewrites and conjunctive query equivalences are based on redundant self-joins elimination. 

To prove the equivalence of any two (-1)-truncated types q1 and q2 , it suffices to prove the bi-implication q1 <-> q2 (lemma equiv_iff_trunc). This is one of the cases where concepts from HoTT simplify formal reasoning in a big way. Instead of having to apply a series of equational rewriting rules (which is complicated by the fact that they need to be applied under the variable bindings of Σ), we can prove the goal using deductive reasoning.

Proof.
simpl.
by_extensionality t.
(* ║ ∑ t’, ⟦q⟧ (fst t’) * ⟦q⟧ (snd t’) * (fst t’ = t) ║ =
║ ⟦q⟧ t ║ *)

apply equiv_iff_trunc.
split.
(* ∃ t’, ⟦q⟧ (fst t’) ∧ ⟦q⟧ (snd t’) ∧ (fst t’ = t) →
⟦q⟧ t *)

intros [[t1 t2] [[h1 h2] eq]].
destruct eq.
apply h1.
(* ⟦q⟧ t →
∃ t’, ⟦q⟧ (fst t’) ∧ ⟦q⟧ (snd t’) ∧ (fst t’ = t) *)

intros h.
exists (t, t).
(* ⟦q⟧ t ∧ ⟦q⟧ t ∧ (t = t) *)
split; [split|].
+ apply h.
+ apply h.
+ reflexivity.

The queries in the above rewrite rule fall in the well-studied category of conjunctive queries where equality is decidable (while equality between arbitrary SQL queries is undecidable). Using Coq’s support for automating deductive reasoning (with Ltac), we have implemented a decision procedure for the equality of conjunctive queries (it’s only 40 lines of code; see this posts source for details), the aforementioned rewrite rule can thus be proven in one line of Coq code.

Restart.
conjuctiveQueryProof.
Qed.

Conclusion

 

We have shown how concepts from HoTT have enabled us to develop HoTTSQL, a SQL semantics that makes it easy to formally reason about SQL query rewrites.

 

We model bags of type A as a function A -> Type. Bags can be proven equal using the univalence axiom. In contrast to models of bags as list A, we require no inductive or permutation proofs. In contrast to models of bags as A -> nat, we can count the number of elements in any bag.

 

Duplicate elimination in SQL is implemented using (-1)-truncation, which leads to clean and easily automatable deductive proofs. Many of our proofs could be further simplified with a ring tactic for the 0-trucated type semi-ring.

 

Visit our website to access our source code, learn how we denote other advanced SQL features such as correlated subqueries, aggregation, advanced projections, etc, and how we proved complex rewrite rules (e.g., magic set rewrites).

 

Contact us if you have any question, feedback, or know how to improve HoTTSQL (e.g., you know how to use more concepts from HoTT to extend HoTTSQL).

Posted in Applications | Leave a comment

Combinatorial Species and Finite Sets in HoTT

(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 , , | 5 Comments

Parametricity and excluded middle

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 Xcannot 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 | 12 Comments

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

Continue reading

Posted in Code, Higher Inductive Types, Programming | 45 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