## Just Kidding: Understanding Identity Elimination in Homotopy Type Theory

Several current proof assistants, such as Agda and Epigram, provide uniqueness of identity proofs (UIP): any two proofs of the same propositional equality are themselves propositionally equal. Homotopy type theory generalizes this picture to account for higher-dimensional types, where UIP does not hold–e.g. a universe (type of types), where equality is taken to be isomorphism, and there can be many different isomorphisms between two types. On the other hand, Coq does not provide uniqueness of identity proofs (but nor does it allow you to define higher-dimensional types that contract it, except by adding axioms).

What determines whether UIP holds? The answer lies in two elimination rules for identity types, called J and K. J is the fundamental elimination rule for identity types, present in all (intensional) dependent type theories. Here is a statement of J, in Agda notation, writing Id x y for the identity (propositional equality) type, and Refl for reflexivity.

    J : (A : Set) (C : (x y : A) -> Id x y -> Set)
-> ((x : A) -> C x x Refl)
-> (M N : A) (P : Id M N) -> C M N P
J A C b M .M Refl = b M


J reads like an induction principle: C is a predicate on on two propositionally equal terms. If you can give a branch b that, for each x, covers the case where the two terms are both x and related by reflexivity, then C holds for any two propositionally equal terms.

J certainly seems to say that the only proof of Id is reflexivity—it reduces a goal that talks about an arbitrary proof to one that just covers the case of reflexivity. So, you would expect UIP to be a consequence, right? After all, by analogy, the induction principle for natural numbers tells you that the only natural numbers are zero and successor of a nat.

Here’s where things get confusing: UIP is not a consequence of J, as shown by the first higher-dimensional interpretation of type theory, Hofmann and Streicher’s groupoid interpretation. This gives a model of type theory that validates J, but in which UIP does not hold. UIP can be added as an extra axiom, such as Streicher’s K:

  K : (A : Set) (M : A) (C : Id M M -> Set)
-> C Refl
-> (loop : Id M M) -> C loop


K says that to prove a predicate about Id M M, it suffices to cover the case for reflexivity. From this, you can prove that any p : Id M M is equal to reflexivity, and from that you can prove that any p q : Id M N are propositionally equal (by reducing one to reflexivity using J). An alternative to adding this axiom is to allow the kind of dependent pattern matching present in Agda and Epigram, which allow you to define K.

So what is J really saying? And why is it valid in homotopy type theory? When there are more proofs of propositional equality than just reflexivity, why can you show something about all of them by just covering the case for reflexivity?

Find out after the cut!

Posted in Foundations | 35 Comments

## An Interval Type Implies Function Extensionality

One of the most important spaces in homotopy theory is the interval (be it the topological interval $[0,1]$ or the simplicial interval $\Delta^1$). Thus, it is natural to ask whether there is, or can be, an “interval type” in homotopy type theory. Of course, the interval is contractible, so up to homotopy equivalence it might as well be a point, but on the “point-set level” it carries additional structure: it is the “universal space containing two points and a path between them.”

With this in mind, it is natural to define an “interval type” to be inductively generated by two elements and a path between them. The usual sort of inductive types do not allow constructors to specify elements of the path-type of the inductive type, rather than elements of the type itself, but we can envision extending the notion of inductive type to allow this. (Of course, there will be semantical and computational issues to deal with.) I think this idea is due to Peter Lumsdaine.

In general, this sort of “higher inductive type” should allow us to build “cell complexes”, including spheres of all dimensions. But right now I just want to describe the interval type I. It comes with three “constructors” zero:I, one:I, and segment: zero $\rightsquigarrow$ one. Its “elimination rule” says that given any type A with points $x,y\colon A$ and a path $p\colon x \rightsquigarrow y$, there is a specified term $i\colon I \vdash \mathrm{Ielim}_{x,y,p}(i)\colon A$ such that $\mathrm{Ielim}_{x,y,p}(\mathrm{zero}) = x$, $\mathrm{Ielim}_{x,y,p}(\mathrm{one}) = y$, and $\mathrm{map}(\mathrm{Ielim}_{x,y,p}, \mathrm{segment}) = p$. (More generally, there should also be a “dependent elimination” property.)

Peter Lumsdaine has “implemented” the interval type in Coq, by asserting I, zero, one, segment, and Ielim as axioms. (See the “Experimental” directory of Andrej’s Github, or Peter’s Github for an older version.) Of course we can’t add new definitional equalities to Coq, but we can assert propositional versions of the computation rules $\mathrm{Ielim}_{x,y,p}(\mathrm{zero}) = x$, $\mathrm{Ielim}_{x,y,p}(\mathrm{one}) = y$, and $\mathrm{map}(\mathrm{Ielim}_{x,y,p}, \mathrm{segment}) = p$. (The same should be possible for any other “higher inductive type.”) This suffices to prove, for instance, that the interval is contractible.

However, if the above rules are actually definitional, then I claim that the interval type (together with the usual eta rule) implies function extensionality. The idea is quite simple: suppose we have a homotopy $p\colon \prod_{x\colon X} (f x \rightsquigarrow g x)$. Then for each $x\colon X$ we have a map $I\to Y$. But by currying and uncurrying, that’s the same as having, for every $a\colon I$, a map $X\to Y$. In particular, applying this to “segment”, we should get a path in the function space $Y^X$ from f to g. More precisely, we get a path from eta(f) to eta(g), due to the effects of the curry-uncurry; thus the eta rule finishes off the proof.

I’ve “implemented” this in Coq, insofar as is possible. The following code uses “admit” to solve two goals that ought to be automatic if the computation rules for the interval held definitionally. (It requires both the base library and Interval.v to be loaded.)

Theorem eta_implies_fe : eta_rule_statement ->
function_extensionality_statement.
Proof.
intros etarule A B f g H.
set (mate := fun (i:Interval) x => interval_path' (H x) i).
path_via (mate zero).
path_via (eta f).
unfold eta, mate.
(* This would be automatic if [interval_path_zero'] were
a definitional equality (computation rule). *)
path_via (mate one).
exact (map mate segment).
path_via (eta g).
unfold mate, eta.
(* Ditto for [interval_path_one']. *)
Defined.

Posted in Foundations | 53 Comments

## A Formal Proof that the Higher Fundamental Groups are Abelian

Homotopy type theory (HoTT) will have applications for both computer science and math. On the computer science side, applications include using homotopy type theory’s more general notion of equality to make formal verification of software easier. On the mathematical side, applications include using type theoretic proof assistants, like Coq and Agda, to give formal, machine-verified, proofs of mathematical theorems. We’d like to show that HoTT is useful for formalizing homotopy theory and higher-dimensional category theory, and then that the ability to work up-to-equivalence is useful for other parts of math as well.

As a first example of the former, we can prove the well-known result that the higher homotopy groups of a topological space are all abelian.

Given a space A and a distiguished base point base, the fundamental group π1 is the group of loops around the base point. π1 has, as elements, the loops at base—paths from the base point to itself—with the group multiplication given by composition, and the identity element by the identity path. However, to satisfy associativity and unit, the paths must be quotiented by homotopy.

However, the homotopies, or deformations of paths, themselves have some structure, and we can look at the second fundamental group π2, which is the same construction “one level up”: take the base point to be the identity loop at the original base point base, and then look at the homotopies from this loop to itself (again quotiented by higher homotopies).

It turns out that the second fundamental group, and all higher ones obtained by iterating this construction, are abelian. The way we’ll prove this is to show that there are two different notions of composition on them, which have the same unit and satisfy an interchange law, so the result follows from the Eckmann-Hilton argument. What are the two notions of compostion? The first is the multiplication from π2, which is just composition/transitivity of homotopies/deformations. The second uses composition of loops one level down (which explains why the fundamental group is not necessarily abelian), and states that composition preserves deformability. Namely, if you have four loops around base, p q p' q' and a deformation from p to p' and a deformation from q to q', then you can compose these to give a deformation from q ∘ p to q' ∘ p'. Now, take all four loops to be the identity, in which case we have an operation that takes two elements of π2 (i.e. two deformations from the identity loop to itself) and gives back a third (by the unit laws, id ∘ id = id).

Next, we are going to formalize this proof in type theory. In particular, I will use Agda, though the proof could easily be translated to Coq.

Here are the basic definitions:


module FundamentalAbelian (A : Set) (base : A) where
π1El : Set
π1El = base ≃ base
π2El : Set
π2El = _≃_{π1El} Refl Refl

_∘_ : π2El → π2El → π2El
p ∘ q = trans q p

_⊙_ : π2El → π2El → π2El
a ⊙ b =  resptrans b a

⊙-unit-l : (p : π2El) → (Refl ⊙ p) ≃ p
⊙-unit-l p = resptrans-unit-r p

⊙-unit-r : (a : π2El) → (a ⊙ Refl) ≃ a
⊙-unit-r a = trans (resptrans-unit-l a) (trans-unit-l a)

interchange : (a b c d : _)
→ ((a ∘ b) ⊙ (c ∘ d)) ≃ ((a ⊙ c)  ∘ (b ⊙ d))
interchange a b c d = trans-resptrans-ichange  _ _ d _ c _ _ b _ a


We define a module parametrized by a set A (Agda uses the word Set for ‘type’) and a term base of that type: the proof works for any space and base point. The type π1El (the elements of π1) is defined to be the loops at base, represented using the identity type M ≃ N, which is defined in a library. Similarly, the elements of π1 are the loops (at type π1El) at reflexivity. The two notions of composition discussed above are defined in the identity type library, with ∘ defined by transitivity, and ⊙ defined by resptrans–the proof that transitivity respects equivalence.

⊙-unit-l proves the left unit law for ⊙. The way to read this declaration is (1) ⊙-unit-l is a term of type (p : π2El) → (Refl ⊙ p) ≃ p (where (x : A) → B is Agda syntax for a Pi-type), and (2) it is defined to be the term λ p → resptrans-unit-r p. That is, it is implemented by a straightforward application of a lemma in the identity type library. ⊙-unit-r is similar, except it takes two lemmas to prove: the general resp-trans-unit-l states that resptrans Refl a is equal to a composed with proofs that cancel trans - Refl (transitivity with reflexivity on this side is propositionally but not definitionally the identity, for the way I have defined transitivity); however, in this case, these transitivities cancel, because the base point is reflexivity.

The middle-four interchange law states an interaction between the two notions of composition, which is key to the proof below. It is proved using an application of a lemma from the library.

Now, we can give a simple formalization of the Eckmann-Hilton argument, which proves that the two compositions are the same, and abelian:

    same : (a b : π2El) → (a ∘ b) ≃ (a ⊙ b)
same a b = (( a ∘ b)              ≃〈 resp (λ x → x ∘ b) (sym (⊙-unit-r a)) 〉
((a ⊙ Refl) ∘ b)         ≃〈 resp (λ x → (a ⊙ Refl) ∘ x) (sym (⊙-unit-l b)) 〉
((a ⊙ Refl) ∘ (Refl ⊙ b)) ≃〈 sym (interchange a Refl Refl b) 〉
((a ∘ Refl) ⊙ (Refl ∘ b))  ≃〈 resp (λ x → x ⊙ (Refl ∘ b)) (trans-unit-l a) 〉
(a ⊙ (Refl ∘ b))         ≃〈 resp (λ x → a ⊙ x) (trans-unit-r b) 〉
(a ⊙ b)
∎)

abelian : (a b : π2El) → (a ∘ b) ≃ (b ∘ a)
abelian a b = (a ∘ b)               ≃〈 resp (λ x → x ∘ b) (sym (⊙-unit-l a)) 〉
((Refl ⊙ a) ∘ b)           ≃〈 resp (λ x → (Refl ⊙ a) ∘ x) (sym (⊙-unit-r b)) 〉
((Refl ⊙ a) ∘ (b ⊙ Refl)) ≃〈 interchange Refl b a Refl 〉
((Refl ∘ b) ⊙ (a ∘ Refl))  ≃〈 resp (λ x → x ⊙ (a ∘ Refl)) (trans-unit-r b) 〉
(b           ⊙ (a ∘ Refl))  ≃〈 resp (λ x → b ⊙ x) (trans-unit-l a) 〉
(b ⊙ a)                     ≃〈 sym (same b a) 〉
(b ∘ a)
∎


The proof is exactly the textbook Eckmann-Hilton argument. We use a notational trick to write the proof as a sequence of steps x ≃〈 p 〉y, which is read x is equivalent to y by p. To prove that the compositions are the same, we expand using the unit laws, apply interchange, and then contract. To prove that they are abelian, we expand using the unit laws, apply interchange, and contract, which swaps the order but also swaps the composition; so same gives the result. In the proofs, resp is a general compatibility lemma, which lifts an equation into a context (given by the function in its first argument).

The thing to take away from this post is that, after developing some libraries for identity types, we were able to use a simple, clean transcription of the Eckmann-Hilton argument to give a formal proof of the result. In the next post, I’ll talk about the lemmas we used from the identity type library.

Technical caveat: following the discussion here (if I have understood it correctly; if not please correct me), what this theorem really states is that composition in the loop space is abelian, up to higher homotopies (because the statement of the theorem itself uses the identity type). This is slightly different than stating that the fundamental group is abelian. The difference is that the loop space is itself a whole higher-dimensional space, with “external” higher-dimensional homotopies, whereas the fundamental group theorem talks about the group whose elements are paths quotiented by homotopy. Our theorem statement is like saying that two numbers are congruent mod k, whereas the theorem about fundamental groups is like saying that two elements of Z/kZ are equal. Of course, it’s easy to go between these, but to state the latter version in type theory, we will need a form of quotient types that lets one quotient by higher dimensional structure to obtain a lower-dimensional type.

The code for this post is here, for now, until I make a GitHub repository. Thierry Coquand and Nils Anders Danielsson have a proof here, but it seems to use a different argument than Eckmann-HIlton.

Posted in Applications | 13 Comments

## Constructive Validity

(This is intended to complement Mike Shulman’s nCat Cafe posting HoTT, II.)

The Propositions-as-Types conception of Martin-Löf type theory leads to a system of logic that is different from both classical and intuitionistic logic with respect to the statements that hold in the fragment of logical language that these three share, namely the quantifiers $\Pi$ , $\Sigma$ , equality $\mathsf{Id}$ , conjunction $\times$ , disjunction $+$ , implication $\rightarrow$ and negation $\neg$ .  For example, it validates the “axiom of choice” but not the “law of excluded middle” — a combination that is impossible classically and intuitionistically.  Let us call this conception “constructive validity” following a paper by Dana Scott in which it was first introduced (Constructive Validity, Symposium on Automated Deduction, LNM 125, Springer (1970), pp. 237-275).

Constructive validity is closely tied to proof theory: as explained by Per Martin-Löf in the monograph Intuitionistic Type Theory (Bibliopolis, 1984), the constructive rules for the logical operations can be justified by associating the terms of a type with the proofs of the corresponding proposition.  To say that a proposition is constructively true or valid means just that it has a proof, and a proof of a conjunction $A\times B$ is a pair of proofs, one for each conjunct $A$ and $B$, and so on.  In the end, a proposition-type $A$ is true iff one has constructed a proof-term $a : A$.  The rules of construction for types are seen to correspond to the usual rules of inference for propositions in a deductive calculus, and so the entire system represents a sort of “theory of proofs”, rather than the more usual logical “theory of provability”. Keyword: Curry-Howard correspondence.

The system of constructive type theory has two variants: extensional and intensional.  This is a topic for another day, but don’t confuse it with the distinct  issue of function extensionality, which can hold or fail in the intensional type theory, but is usually assumed to hold in the extensional theory.  We can model extensional constructive type theory in a now well-known way in locally cartesian closed categories.  In particular, this theory is deductively complete with respect to both topological models (i.e. sheaves on a space, see S. Awodey, Topological representation of the lambda-calculus. Math. Stru. Comp. Sci. (2000), vol. 10, pp. 81–96.) and Kripke models (i.e. presheaves on a poset, see S. Awodey and F. Rabe, Kripke Semantics for Martin-Löf’s Extensional Type Theory. TLCA 2009: 249-263).  The topological and order-theoretic interpretation of this system is a straighforward extension of the same for the simply typed $\lambda$-calculus, which is the basis of Dana Scott’s domain theory. The basic insight of domain theory is that logically definable maps are always continuous, and logical constructions (with their associated structure maps, like product projections) should not lead outside the category of spaces.  This leads to the development of synthetic domain theory, which like Lawvere’s synthetic differential geometry builds the continuity, respectively smooth structure, in from the start and seeks to axiomatize the logical-categorical structure of such a category of domains, respectively smooth spaces, directly (rather than modelling them as structured sets).

Still talking about the extensional system, we can compare and relate constructive to classical and intuitionistic validity by extending the system in several different ways: logic-enriched type theory of Aczel and Gambino (Collection principles in dependent type theory, in: Vol. 2277 of LNCS, Springer-Verlag, 2002, pp. 1-23.), the [bracket] types of Awodey and Bauer (Journal of Logic and Computation. Volume 14, Issue 4, August 2004, pp. 447-471), a type Prop of proof-irrelevant propositions as in Coq, and others.  In such a hybrid system, one may consider the constructive (proof-relevant) operations $\Pi, \Sigma, \mathsf{Id}, \times, + , \rightarrow, \neg$  as “type-theoretic” and the corresponding “predicate logical” ones $\forall, \exists, =, \wedge, \vee, \Rightarrow, \neg$ as “logic”.  These new predicate logical operations are “proof irrelevant”, since they produce or apply to formulas which do not preserve all the information about proofs (e.g., from a proof of $\exists x:A. P(x)$ one does not always have a way to find a term $a:A$ and a proof of $P(a)$).  Such extended systems are useful both for relating constructive and other kinds of validity, and also for reasoning about their natural models in categories like toposes that have the required structure (an lcc pretopos is more than sufficient).  However, one does not need to include such extended predicate or proof-irrelevant logical operations in a system of constructive logic, which is perfectly sensible without them. (Semantically, the proof-irrelevant operations are modeled in the fibration of subobjects or monos over the category of types, rather than in the entire codomain fibration as in the lccc semantics.)

Now what about the intensional system?  Here the notion of constructive validity is even further from classical and intuitionistic validity, since the proof-relevant identity relation also behaves in a logically unfamiliar way (but one that is familiar from the standpoint of higher-dimensional categories!).  Despite its better proof-theoretic and computational character, even many type-theorists with constructive inclinations have had a hard time learning to live with this system, and prefer instead systems with additional rules that imply not only Function Extensionality, but also Uniquenes of Identity Proofs.  As a system of logic, however, intensional type theory without such additions still represents a perfectly coherent conception — just one that is very different from the intuition of (classical or intuitionistic) sets, classes, relations, functions, etc.

And now the fascinating new fact is that this conception of intensional constructive type theory does have a natural model in the world of homotopy — with the identity relation interpreted as the fibration of paths, and the quantifiers interpreted constructively as before.  This model expands the topological one of extensional type theory by replacing the diagonal relation by the fibration of paths, which aligns better with the constructive point of view, since it’s now a proof-relevant relation.  (From an order-theoretic point of view, we pass from posets to (higher-dimensional) categories, and use the (higher) groupoid of isos in place of the diagonal relation.)

This is the leading idea of Homotopy Type Theory: we still regard the operations of quantification, identity, etc. as constructively logical — and we can use the system of type theory to reason formally as before — but the interpretation is now intrinsically homotopical: the types are spaces (or homotopy types), the terms are continuous mappings, identity between terms (as expressible in the system) is homotopy, isomorphism of types is homotopy equivalence, etc.  Combining this with the constructive interpretation of the other logical operations (quantification, implication, conjunction, etc.) still makes good sense, given the topological interpretation that we already had of constructive validity — in fact, it makes even better sense than before, since now identity is handled constructively, too (as opposed to extensionally), and is modelled topologically.  The approach might also be called synthetic homotopy theory, since it has the same methodology of taking homotopy, continuity, etc., as built-in, rather than modelled in structured sets.

Finally, what happens if — as in the extensional case — we try to add a [bracket]-type constructor, or logic-enriched type theory, or a proof-irrelevant type Prop into the mix?  There does seem to be a natural “proof irrelevant logic” in the homotopical model, say in simplicial sets.  One can identify some types as “propositions” — i.e. types of H-level 1, using Voevodsky’s IsProp construction — and one can imagine using $\pi_{-1}$ as a logical operation like the [bracket]  to “squash all the proofs together”.  In that case, one would again have a “hybrid” system in which there are both $\Sigma$ and $\exists$, etc. — both “type-theoretic” and “logical” operations, as we termed them above.  This is much like (a part of) the Calculus of Constructions implemented in the current Coq system — but it is not (yet) used in homotopy type theory, nor is it used in Voevodky’s Coq development of Univalent Foundations.  That’s not to say that HoTT couldn’t profitably be extended in this way — very likely it could.  But one would first need to pick an extended type theory and then carefully investigate the homotopical interpretation of that extended system, and this has yet to be done.  Even then, however, the original constructive interpretation remains a perfectly coherent conception of constructive validity; we don’t want to be forced to always read the identity relation as a space of paths, and the quantifiers as disjoint sums and dependent products — those are constructions on structured sets rather than primitive logical operations of identity and quantification.  We want a system of logic representing constructive validity, employing the propositions-as-types paradigm — perhaps extended by some further device for erasing proof-relevance — interpreted homotopically in a way that also makes geometric sense.  Understanding both the logical and homotopical sides, and their interaction, is what this project is about.

Posted in Foundations | 17 Comments

## Homotopy Type Theory, II | The n-Category Café

Mike Shulman has another great posting on HoTT over at the n-Cat Cafe’. It starts out like this:

Homotopy Type Theory, II — Posted by Mike Shulman

Last time we talked about the correspondence between the syntax of intensional type theory, and in particular of identity types, and the semantics of homotopy theory, and in particular that of a nicely-behaved weak factorization system. This time we’re going to start developing mathematics in homotopy type theory, mostly following Vladimir Voevodsky’s recent work.

## Function Extensionality from Univalence

Andrej Bauer and Peter Lumsdaine have worked out a proof of Function Extensionality from Univalence that is somewhat different from Vladimir Voevodsky’s original.  In it, they identify and employ a very useful consequence of Univalence: induction along weak-equivalences.  Andrej has written it up using CoqDoc, which produces a very readable pdf available from his GitHub repository or directly here.  Peter has a neatly organized Coq treatment in his repository here.

Here is the Introduction from Andrej’s CoqDoc:

This is a self-contained presentation of the proof that the Univalence Axiom implies Functional Extensionality. It was developed by Peter LeFanu Lumsdaine and Andrej Bauer, following a suggestion by Steve Awodey. Peter has his own Coq file with essentially the same proof.

Our proof contains a number of ideas from Voevodsky’s proof. Perhaps the most important difference is our use of the induction principle for weak equivalences, see weq induction below. We outline the proof in human language at the end of the file, just before the proof of extensionality.

This file is an adaptation of a small part of Vladimir Voevodsky’s Coq files on homotopy theory and univalent foundations, see https://github.com/vladimirias/Foundations/.

The main difference with Voevodsky’s file is rather liberal use of standard Coq tricks, such as notation, implicit arguments and tactics. Also, we are lucky enough to avoid universe inconsistencies. Coq is touchy-feely about universes and one unfortunate definition seems to be enough to cause it to encounter a universe inconsistency. In fact, an early version of this file encountered a universe inconsistency in the last line of the main proof. By removing some auxiliary definitions, we managed to make it go away.

This file also contains extensive comments about Coq. This is meant to increase its instructional value.

Posted in Univalence | 6 Comments