UF IAS 2012 Archive Open Problems

Here are some open problems that have come up.

Mathematics

Here are problems related to type theory and univalent foundations which are not just re-proofs of theorems from classical mathematics.

1. Define the notion of a (semi-) simplicial type in type theory. Here is a description.
2. Without using HITs, but with a sequence of univalent universes, show that for any $n>0$ there are types strictly of h-level $n$ (i.e. of h-level $n$ but not of h-level $n$-1). (Didn’t Nicolai do this?)
3. Let TT^+ be the intensional type theory with a sequence of universes + for each n>0, an axiom asserting that there are types strictly of h-level n. Show that the addition of axioms asserting that each universe is univalent does not increase the logical strength (in the proof theoretic sense) or perhaps show that it does.
4. Is there a Quillen model structure on semi-simplicial sets (with semi-simplicial Kan fibrations) making it Quillen equivalent to simplicial sets (with Kan fibrations)?
5. Define a weak omega-category in type theory.

Formalization

Here are theorems which are true in classical homotopy theory, which we should try to prove in type theory and formalize in Coq in order to learn more about how to use proof assistants and what we want of them. The problems are listed in the order of anticipated difficulty. Some of the problems need careful formulation.

1. Prove that the torus (with the HIT definition involving a 2-dimensional path) is equivalent to a product of two circles.
2. Study the fundamental group / loop space of a wedge of circles indexed by an arbitrary set A. If A has decidable equality, then you can prove that the loop space is equivalent to the free group on A (see here). If A does not have decidable equality, it is most likely still true that the fundamental group of the wedge of circles is equivalent to the free group (I haven’t formalized it yet), but the loop space seems more complicated and does not even seem to be a set.
3. Show that the homotopy groups of spheres are all finite except for those of the form π_n(S^n) or π_{4n−1}(S^(2n)) (for positive n), when the group is the product of Z with a finite abelian group.

Closed formalization problems :)

See also the page on Formalized Homotopy Theory.

1. Using higher inductive types, show that π_1(S^2) is trivial. (solved by Guillaume, then by Dan)
2. Prove that the $k$-th homotopy group of S^n is trivial if $k$ < $n$. (solved by Guillaume, then by Dan)
3. Prove that the n-th homotopy group of S^n is $Z$. (solved by Dan and Guillaume)
4. Use higher-inductive types to define arbitrary truncations (solved by Guillaume; see here)
5. Prove the Seifert–van Kampen theorem. (done by Mike Shulman)
6. For $G$ a group (with a set of elements) construct a $K($G$,1)$ space. (solved by Dan)
7. For some definition of the spheres, define a fibration over S^2 whose fiber is S^1 and whose total space is S^3 (Hopf fibration). (solved by Guillaume)
8. For G an abelian group and $n$ > 1, construct a $K($G$,n)$ space (n-truncated space whose n-fold loop space is G) (solved by Dan)
9. Prove that if a function A -> B induces a bijection on connected components and for any base point induces an equivalence between loop spaces, then it is an equivalence (solved by Dan)
10. Prove the Freudenthal suspension theorem (solved by Peter L. and Dan).
11. Prove that every precategory is equivalent (in some sense) to a category (where equality on objects is equivalent to isomorphism in the category). (solved by Benedikt and Chris K.)