# 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 :)

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)
6. For $G$ a group (with a set of elements) construct a $K($G$,1)$ space. (solved by Dan)
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)